Programming Languages
누수 세미콜론
Author
Venue
ACM 프로그래밍 언어 학술대회 2021 논문집
Abstract
프로그램 논리와 의미론은 순차적 조합에 대해 유쾌한 이야기를 들려줍니다. (S1; S2)를 실행할 때, 우리는 먼저 S1을 실행한 다음 S2를 실행합니다. 그러나 성능을 향상시키기 위해 프로세서는 명령어를 순서대로 실행하지 않으며, 컴파일러는 프로그램을 훨씬 더 극적으로 재배열합니다. 설계상 단일 스레드 시스템은 이러한 재배열을 관찰할 수 없지만, 다중 스레드 시스템은 이를 관찰할 수 있어 이야기가 상당히 덜 유쾌해집니다. 그 결과 발생하는 혼란을 이해하기 위한 형식적 시도는 ``완화된 메모리 모델(relaxed memory model)''로 알려져 있다. 기존 모델들은 순차적 합성을 직접 다루지 못하거나, 프로세서와 컴파일러를 지나치게 제한하거나, 실제로는 관찰할 수 없는 터무니없는 허공의 동작을 허용하기도 한다. 현대 하드웨어를 대상으로 하면서도 순차적 합성을 지원하기 위해, 우리는 표준 이벤트 기반 접근법을 전제 조건과 술어 변환기 군으로 보강한다. (S1;S2)의 의미를 계산할 때, S2의 이벤트 e의 전제 조건에 적용되는 술어 변환기는 e가 의존하는 S1 내의 이벤트 집합을 기반으로 선택됩니다. 우리는 이 접근 방식을 두 가지 기존 메모리 모델에 적용합니다.
