WarpDRF: Warp 레벨 프로그래밍을 위한 데이터 레이스 자유성

텐서 코어 연산(tensor core operations), 셔플(shuffles), 리덕션(reductions), 배리어(barriers)와 같은 Warp 기본 요소들은 고성능 GPU 커널에 매우 중요하며, 모든 주요 GPU 언어가 이들 중 일부 세트를 지원합니다. 기본 요소를 수행하는 스레드들이 참여하고 따라서 동기화되는 방식은 스레드가 분기하고 재수렴하는 방식, 그리고 독립적인 스레드 스케줄링과 같은 워프 내부 스케줄링에 의해 동적으로 결정됩니다. 실제로 많은 고성능 커널들은 이러한 기본 요소들을 사용하며 예상대로 작동하는데, 이는 명시적으로 정의되거나 경험적으로 테스트된 적이 없는 직관적이지만 불문율의 데이터 레이스 자유성(data-race-freedom) 계약을 따르기 때문입니다. 우리는 이 계약을 정확하게 만드는 최초의 추상 워프 프로그래밍 모델인 WarpDRF를 제시합니다. 이는 재수렴 보장과 기본 요소별 요구 사항에 의해 매개변수화된 참여 규칙을 통해, 다양한 GPU 언어에 맞는 인스턴스화를 가능하게 합니다. 우리는 (Rocq에 형식화되어) WarpDRF를 만족하는 커널이 참조 의미론(reference semantics)이 할당하는 참여자들과 모든 워프 기본 요소를 실행하고 동일한 결과를 생성함을 증명합니다. 따라서 프로그래머는 참조 의미론만으로 추론할 수 있습니다. 우리는 MLIR에 이 모델을 구현하여 참조 인터프리터와 함께, 16개의 장치 및 백엔드 쌍에 걸쳐 CUDA, HIP, HLSL, Metal, SPIR-V의 세 가지 구성 각각에 대해 10K 개의 준수 테스트(conformance tests)를 퍼즈했습니다. 적어도 하나의 WarpDRF 구성이 각 경우를 설명하며, 이 중 CUDA는 가장 약한 구성을 엄격하게 따릅니다. 마지막으로, 우리는 CUDA용 정적 데이터 레이스 분석기인 Faial을 최초의 경험적으로 검증된 워프 모델에 대한 DRF(Data-Race Freedom) 체커로 확장하고 이를 llama.cpp에 적용했습니다. 그 결과, 대부분의 워프 기본 요소를 사용하는 커널들은 이미 이 계약을 만족했지만, 세 개의 커널에서 이전에 알려지지 않은 데이터 레이스들이 발견되어 이러한 검사 도구의 필요성을 보여주었습니다.