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