프로그래밍 언어 및 도구 연구소

IMM: 완화된 메모리 모델에 대한 컴파일 정확성

IMM 프레임워크는 Promising 및 Weakestmo와 같은 프로그래밍 언어 메모리 모델에서 x86, Power, Arm 및 RISC-V와 같은 하드웨어 메모리 모델에 이르기까지 컴파일의 정확성을 보다 간단하게 증명할 수 있게 해줍니다.프레임워크는 Coq에서 기계화됩니다.

약한 메모리 일관성 의미론을 가진 동시 프로그래밍 언어부터 POWER 및 ARM과 같은 주류 멀티 코어 아키텍처에 이르기까지 컴파일의 정확성 증명을 모듈화하는 방법으로서 중간 약한 메모리 모델인 IMM을 개발하고 있습니다.IMM을 사용하여 여러 가지 새로운 프로그래밍 언어 메모리 모델(주로 out-of-thin-air 문제 해결을 목표로 함)부터 POWER, ARMv7, ARMv8, RISC-V 및 x86-TSO와 같은 하드웨어 메모리 모델까지 컴파일의 정확성을 증명합니다.Coq에서 결과가 기계화되었으며, 우리가 아는 한 이것은 x86-TSO보다 약한 모델에 대해 기계로 검증된 최초의 컴파일 정확성 결과입니다.

참가자

Anton Podkopaev
Evgenii Moiseenko