기술 요약: 고수준 합성에서의 메모리 충돌 탐지를 위한 분리 논리 (Separation Logic)

문제 정의

고수준 합성(High-Level Synthesis, HLS)은 루프 언롤링(loop unrolling)과 배열 파티셔닝(array partitioning)을 활용하여 병렬성을 극대화함으로써, C/C++ 코드를 레지스터 전송 레벨(RTL) 설계로 변환하여 하드웨어 개발을 가속화한다. 그러나 비-아핀 산술(non-affine arithmetic)(예: 심볼릭 곱셈, 나눗셈 또는 나머지 연산)을 포함하는 동시 메모리 접근을 스케줄링할 때 결정적인 병목 현상이 발생한다.

전통적인 HLS 프레임워크는 의존성 분석을 위해 **폴리헤드 모델(polyhedral model)**에 의존한다. 이 기하학적 접근 방식은 루프 경계와 배열 접근 함수가 아핀(선형 조합)이어야 한다는 제약을 가진다. 비-아핀 인덱스를 마주할 때, 폴리헤드 솔버는 안전성을 보장하기 위해 의존성을 체계적으로 과잉 근사(over-approximate)한다. 이는 모든 메모리 문장이 서로 의존한다고 가정하는 보수적인 폴백(fallback)을 강제하며, 결과적으로 **모놀리식 힙 할당(monolithic heap allocation)**과 운영 가능한 작업들의 직렬화를 초래한다. 이러한 인위적인 직렬화는 하드웨어 처리량과 효율성을 저하시킨다. 또한, 기존의 동적 기법들은 런타임 체크나 특수한 컨트롤러를 필요로 하여 오버헤드를 발생시킨다.

방법론

본 논문은 비-아핀 기하학적 제약에 의존하지 않고 메모리 충돌을 탐지하기 위해, **LLVM 중간 표현(Intermediate Representation, IR)**에서 직접 작동하는 **공간 검증 프레임워크(spatial verification framework)**를 제안한다. 핵심 방법론은 **분리 논리(Separation Logic, SL)**를 SMT(Satisfiability Modulo Theories) 솔빙과 결합하는 것이다.

1. LLVM IR 레벨에서의 공간 모델링

C/C++ 추상 구문 트리(AST)를 분석하는 이전 방식들과 달리, 본 프레임워크는 LLVM IR 상에서 동작한다. 이는 컴파일러가 다차원 배열 인덱스를 1차원 산술식으로 기계적으로 평탄화(flattening)할 때 사용하는 getelementptr (GEP) 명령어를 활용한다.

• 이중 상태 구조 (Dual-State Architecture): 프레임워크는 시스템 상태를 두 가지 별개의 구성 요소로 모델링한다:
  • 단조 저장소 (Monotonic Store, $s$): 불변의 정적 단일 할당(SSA) 가상 레지스터를 값에 매핑한다. SSA 덕분에 레지스터는 덮어쓰이지 않으므로 상태 추적이 단순하다.
  • 공간 힙 (Spatial Heap, $h$): 물리적 메모리 주소(값의 부분 집합)를 데이터에 매핑하며, 이는 온칩(on-chip) SRAM 뱅크를 나타낸다.
• 다형적 뱅크 술어 (Polymorphic Bank Predicates): 프레임워크는 $N$개의 뱅크로 분할된 배열 $A$에 대해 $k$번째 메모리 뱅크의 독점적 소유권을 단언하는 공간 술어 bank(k, A, N)를 정의한다. 이 술어들은 LLVM 메타데이터에서 추출된 파티셔닝 전략(Cyclic, Block, 또는 Complete)에 따라 동적으로 적응한다.

2. 충돌 없는 언롤링 (Conflict-Free Unrolling, CFU) 조건

$U$번 언롤링된 루프 반복이 구조적 해저드 없이 동시에 실행될 수 있는지 검증하기 위해, 프레임워크는 충돌 없는 언롤링(CFU) 조건을 공식화한다.

• 분리 결합 (Separating Conjunction, $\ast$): 검증의 핵심은 반복되는 분리 결합이다:
  $$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$$
  이는 $U$개의 동시 메모리 접근이 $U$개의 엄격히 서로 소인(strictly disjoint) 물리적 메모리 영역을 소유해야 함을 단언한다.
• 공간적 붕괴 (Spatial Collapse): 분리 논리의 근본적인 공리는 자원이 자기 자신에 의해 분리되어 소유될 수 없다는 것이다 ($P \ast P \implies \bot$). 만약 두 개의 동시 반복이 동일한 물리적 뱅크 $k$를 대상으로 하면, 공간 공식은 $bank(k) \ast bank(k)$를 평가하려고 시도하며, 이는 논리적으로 **모순($\bot$)**으로 붕괴된다. 이 붕패는 메모리 충돌의 수학적 탐지 역할을 한다.

3. SMT로의 변환 및 폴백

공간 논리를 계산 가능하게 만들기 위해, 프레임워크는 변환 함수 $T$를 사용하여 공간적 소외 요구사항을 SSA 변수들에 대한 쌍별 부등식(pairwise inequalities) 행렬로 축소한다.

• 검증 조건 (Verification Condition, VC): 공간적 요구사항은 다음과 같은 1차 논리 공식으로 변환된다:
  $$\pi \implies \bigende_{1 \le i < j \le U} (k_i \neq k_j)$$
  여기서 $\pi$는 경로 조건이고 $k_i$는 심볼릭 뱅크 인덱스이다.
• SMT 오라클 (SMT Oracle): SMT 솔버(예: Z3)는 VC를 증명하려고 시도한다:
  • Sat (Satisfiable): 인덱스들이 증명 가능하게 구별됨; 병렬 합성이 진행된다.
  • Unsat/Unknown/Timeout: 솔버가 (비선형 산술으로 인해) 결정 불가능한 경우 인덱스의 구별을 증명할 수 없다면, 프레임워크는 **결정론적 순차 폴백(deterministic sequential fallback)**을 트리거한다. 이는 해저드가 존재한다고 가정하고, 물리적 안전을 보장하기 위해 멀티플렉서 기반의 스톨(stall) 로직을 통해 연산을 직렬화한다.

주요 기여

1. 공식 하드웨어 메모리 모델: 본 논문은 다차원 배열 인덱스를 GEP 명령어를 통해 추상화하고, 이를 Cyclic, Block, Complete 파티셔닝을 처리하는 다형적 공간 술어에 바인딩하는 LLVM IR 기반의 정적 메모리 프레임워크를 구축한다.
2. 충돌 없는 언롤링 (CFU) 조건: 반복되는 분리 결합을 사용하여 결정적인 공간 실행 요구사항을 공식화한다. 이는 기하학적 과잉 근사가 아닌 자동화된 공간 논리 붕괴($cfu \implies \bot$)를 통해 물리적 뱅크 해저드를 탐지한다.
3. 자동화된 SMT 변환 및 폴백: 변환 함수는 공간적 명제를 불변의 SSA 레지스터에 대한 쌍별 부등식으로 축소한다. 결정적으로, 비선형 정수 산술이 결정 불가능할 때를 대비하여 절대적 안전을 보장하는 보수적인 순차 폴백 모델을 포함한다.
4. 건전성 정리 (Theorem of Soundness): 대수적 검증 조건이 SMT 솔버에 의해 유효함이 입증되면, 생성된 RTL이 구조적으로 메모리 뱅크 충돌로부터 면역이 있음을 증명한다.

결과 및 의의

본 논문은 형식적 분리 논리 이론과 실제 하드웨어 합성 사이의 간극을 메운다고 주장한다. 기하학적 폴리헤드 모델에서 LLVM IR 상의 대수적 SMT 솔빙으로 검증 부담을 전환함으로써, 프레임워크는 다음과 같은 효과를 얻는다:

• 보수적 직렬화 최소화: 비-아핀 인덱스를 만났을 때 전통적인 도구들이 취하는 "안전하지만 느린" 폴백을 피한다(단, SMT 솔버가 대수적 제약을 해결할 수 있는 경우).
• 구조적 안전성 보장: "공간적 붕괴" 메커니즘과 보수적인 폴백을 통해, 결정 불가능한 산술이 존재하는 경우에도 생성된 하드웨어가 구조적 메모리 충돌을 겪지 않음을 보장한다.
• 아핀 제한 우회: 선형 기하학적 경계나 추가적인 런타임 상태 머신 오버헤드 없이 복잡한 뱅크 매핑 의존성을 해결한다.

이 연구의 의의는 HLS 스케줄링을 위한 엄격한 대수적 대안을 제공함으로써, 비-아핀 메모리 접근 패턴을 가진 설계에서 더 높은 병렬성을 가능하게 하는 동시에 하드웨어 생성에 필요한 절대적 안전 보장을 유지하는 데 있다. 저자들은 향-연구로서 이를 커스텀 LLVM 패스로 구현하고, 읽기 전용 동시 접근 최적화를 위한 분할 권한(fractional permissions)을 탐구할 것이라고 언급하였다.