TENSURE: 희소 텐서 컴파일러 (STC) 를 위한 퍼징 도구 기술 요약

본 논문은 TENSURE라는 새로운 확장 가능한 블랙박스 퍼징 (Fuzzing) 프레임워크를 제안합니다. 이는 고차원 데이터 분석 및 머신러닝 워크로드를 최적화하는 핵심 인프라인 **희소 텐서 컴파일러 (Sparse Tensor Compilers, STC)**의 기능적 정확성을 검증하기 위해 설계된 최초의 도구입니다.

1. 문제 정의 (Problem)

희소 텐서 컴파일러 (STC) 는 압축된 저장 포맷 (CSR, CSC, COO 등) 에서 작동하는 복잡한 비정형 제어 흐름을 고수준 선언적 명세 (예: Einsum) 에서 직접 합성해야 합니다. 이로 인해 다음과 같은 심각한 검증의 어려움이 존재합니다.

• 기존 테스트 프레임워크의 한계: 기존 텐서 컴파일러 테스트 도구 (NNSmith, PolyJuice 등) 는 고정된 연산자 (MatMul, Conv2d 등) 집합으로 구성된 계산 그래프를 기반으로 합니다. 이는 임의의 루프 합성 능력을 테스트하지 못하며, 희소 저장 포맷의 복잡한 제약 조건을 반영하지 못합니다.
• 일반 퍼징의 비효율성: 문법 기반 퍼저 (Grammar-based Fuzzers) 는 문법적으로 유효한 입력을 생성할 수 있지만, Einsum 표기법의 엄격한 의미론적 제약 (예: 인덱스 재사용 규칙, 차원 일관성) 을 이해하지 못해 생성된 입력의 96% 이상이 컴파일러에 의해 거부됩니다.
• 검증의 어려움: STC 는 고수준 선언적 명세를 기반으로 하므로, 기존 명령형 제어 흐름 변형 (dead-code injection 등) 이 적용 불가능합니다. 또한, 다양한 STC (TACO, Finch, MLIR 등) 간 문법과 시맨틱이 파편화되어 있어 통합 테스트 프레임워크 구축이 어렵습니다.

2. 방법론 (Methodology)

TENSURE 는 기존 접근법과 달리 Einsum (Einstein Summation) 표기법을 일반적인 입력 추상화 단위로 사용하여 다음과 같은 핵심 메커니즘을 구현했습니다.

가. 제약 기반 생성 알고리즘 (Constraint-Based Generation)

• 문제: Einsum 표현식은 문맥 의존적 (Context-Sensitive) 인 제약 조건을 가지므로, 일반 문맥 자유 문법 (CFG) 으로 생성 시 유효성이 떨어집니다.
• 해결: TENSURE 는 생성 과정을 **제약 충족 문제 (Constraint Satisfaction Problem)**로 모델링합니다.
  • 입력 텐서의 인덱스 집합을 전역 인덱스 풀에서 샘플링하되, 최대 랭크 (Rank) 를 제한합니다.
  • 출력 인덱스와 축소 (Contraction) 인덱스를 분리하고, 축소 인덱스가 적어도 두 개의 입력 텐서에 존재하도록 **연결성 (Connectivity)**을 강제합니다.
  • 각 인덱스에 구체적인 차원 크기를 할당하여 텐서 모양 (Shape) 의 호환성을 보장합니다.
  • 결과: 생성된 모든 커널이 **100% 의미론적 유효성 (Semantic Validity)**을 가지며, 기존 문법 퍼저의 약 3.3% 유효율 대비 압도적인 효율성을 보입니다.

나. 의미 보존 변형 연산자 (Semantic-Preserving Mutation Operators)

참조 컴파일러 없이 메타모픽 테스트 (Metamorphic Testing) 를 수행하기 위해 두 가지 변형 전략을 도입했습니다.

1. 대수적 교환 법칙 (Algebraic Commutativity): 텐서 연산의 교환 법칙을 활용하여 피연산자의 순서를 변경합니다 (예: $A = B \times C$ vs $A = C \times B$). 이는 동일한 수학 연산에 대해 컴파일러가 생성하는 루프 스케줄이 달라지도록 강제합니다.
2. 저장 포맷 이질성 (Storage Format Heterogeneity): 입력 및 출력 텐서에 서로 다른 압축 저장 포맷 (CSR, CSC, COO 등) 을 무작위로 할당합니다. 수학적으로 동일한 커널이라도 데이터 레이아웃에 따라 생성되는 루프 중첩 구조가 달라지므로, 특정 포맷 처리 로직의 결함을 발견할 수 있습니다.

다. 언어 중립 아키텍처

TACO(C++ 기반) 와 Finch(Julia 기반) 등 다양한 STC 를 지원하기 위해 JSON 기반의 추상화 계층을 도입했습니다. 퍼징 엔진은 추상화된 JSON 스키마를 생성하고, 각 컴파일러에 맞는 경량 변환기 (Translator) 가 이를 해당 도메인별 DSL 로 변환하여 실행합니다.

3. 주요 기여 (Key Contributions)

1. 최초의 STC 전용 퍼저: 언어에 구애받지 않는 블랙박스 퍼징 프레임워크인 TENSURE 를 최초로 제안했습니다.
2. 도메인 특화 변형 연산자: 저장 포맷의 이질성과 대수적 교환 법칙을 활용한 새로운 변형 연산자 세트를 정의하여 의미론적으로 동등한 프로그램을 생성합니다.
3. 100% 유효성 보장 생성 알고리즘: 문맥 민감적 차원 제약을 해결하는 알고리즘을 구현하여, 기존 퍼징 대비 유효한 테스트 케이스 생성 효율을 극대화했습니다.

4. 평가 결과 (Evaluation Results)

최신 STC 두 가지 (TACO, Finch) 를 대상으로 6 시간 동안 퍼징을 수행한 결과는 다음과 같습니다.

• 생성 효율성: TENSURE 의 제약 기반 생성기는 100% 유효율을 기록한 반면, 기존 문법 기반 퍼저 (Grammarinator) 는 약 **3.3%**의 유효율만 보였습니다.
• TACO 평가:
  • 267,000 회 이상의 반복 테스트 수행.
  • 유효한 입력 중 약 **65.2%**에서 결함 발견.
  • 5,758 건의 버그 발견 (크래시 14,400 건 중 일부, 오류 코드 (Silent Miscompilation) 5,758 건 포함).
  • 특히, 컴파일러가 실행은 성공하지만 잘못된 결과를 출력하는 '침묵하는 오류'가 다수 발견되었습니다.
• Finch 평가:
  • 1,619 회 반복 테스트 (컴파일 오버헤드로 인해 TACO 대비 처리량이 낮음).
  • 57 건의 크래시 버그 발견.
  • TACO 와는 달리 침묵하는 오류는 발견되지 않았으나, 프레임워크의 확장성을 입증했습니다.

5. 의의 및 결론 (Significance)

• 희소 컴파일러 생태계의 취약성 폭로: TENSURE 를 통해 현재 STC 인프라 (특히 TACO) 가 심각한 취약점을 가지고 있으며, 단순한 커널에서도 루프 초기화 오류 등으로 인해 심각한 오류가 발생할 수 있음을 증명했습니다.
• 검증 도구의 필요성 강조: 기존 밀집 (Dense) 텐서 컴파일러 테스트 기법이 희소 컴파일러에는 적용되지 않으며, Einsum 의 복잡한 제약 조건을 이해하는 전용 테스트 도구가 필수적임을 보여줍니다.
• 향후 방향: 부동소수점 연산의 비결정성 문제를 해결하기 위해 정수 전용 테스트 모드 도입, 텐서 전치 (Transpose) 를 활용한 추가 변형 연산자 개발, MLIR Sparse Dialect 등 최신 플랫폼으로의 확장 등을 계획하고 있습니다.

결론적으로, TENSURE 는 차세대 머신러닝 및 과학 컴퓨팅 인프라의 신뢰성을 확보하기 위해 필수적인 자동화된 검증 도구로서, 희소 텐서 컴파일러의 기능적 결함을 효과적으로 탐지할 수 있음을 입증했습니다.