프로그램 논리와 의미론은 순차 구성이라는 유쾌한 모습을 보여줍니다. 즉, (𝑆1; 𝑆2)를 실행할 때 먼저 𝑆1을 실행한 다음 𝑆2를 실행합니다.그러나 성능을 향상시키기 위해 프로세서는 명령을 잘못된 순서로 실행하고 컴파일러는 프로그램 순서를 더 크게 재배열합니다.설계상 단일 스레드 시스템은 이러한 재정렬을 관찰할 수 없습니다. 그러나 다중 스레드 시스템은 그럴 수 있기 때문에 유쾌함이 크게 퇴색됩니다.이로 인한 혼란을 이해하기 위한 공식적인 시도로 "완화된 메모리 모델"이라는 것이 알려져 있습니다.

이전 모델은 순차적 구성을 직접 처리하지 못하거나, 프로세서 및 컴파일러를 지나치게 제한하거나, 실제로 관찰할 수 없는 터무니없는 thin-air 동작을 허용합니다.최신 하드웨어를 대상으로 하면서 순차 구성을 지원하기 위해 우리는 전제 조건 및 술어 변환기 세트를 사용하여 표준 이벤트 기반 접근 방식을 강화하고 있습니다.(𝑆1; 𝑆2)의 의미를 계산할 때 𝑒가 의존하는 𝑆1의 이벤트 집합에 따라 𝑆2에서 이벤트 𝑒의 전제 조건에 적용되는 술어 변환기가 선택됩니다.

• 프로젝트 저장소