OpenMP 병렬성을 포함한 C 언어의 형식적 의미론 (A Formal Semantics of C with OpenMP Parallelism)

OpenMP는 사용자가 몇 가지 간단한 어노테이션 (annotations)을 통해 순차적 코드 (sequential code)를 병렬 코드 (parallel code)로 변환할 수 있게 해주는 대중적인 병렬화 프레임워크 (parallelization framework)입니다. 불행히도, 기존에 올바른 프로그램에 OpenMP 프라그마 (pragmas)를 추가함으로써 논리적 오류 (logic errors)와 레이스 컨디션 (race conditions)을 모두 포함하여 의도치 않게 오류를 유발하기 쉽습니다. 본 논문에서는 검증된 컴파일러인 CompCert의 C 의미론 (C semantics)과 이를 동시성 (concurrency)으로 확장한 연구를 바탕으로, OpenMP 지시어 (directives)가 포함된 C 코드에 대한 형식적 의미론 (formal semantics)을 제시합니다. 우리의 의미론은 이전의 OpenMP 의미론에서 모호하게 처리되었던 OpenMP 지시어와 변수 상태 (variable state) 사이의 미묘한 상호작용을 포착하며, 잘못된 어노테이션으로 인해 발생하는 원치 않는 동작을 탐지할 수 있는 기반을 제공합니다. 특히, 모든 성공적인 실행은 데이터 레이스 (data races)가 없음을 보장합니다.