WarpDRF: GPU Warp 프로그래밍의 암묵적인 계약

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