동기화할 때까지는 아무것도 공유되지 않는다: 데이터 레이스 자유를 위한 Java 재해석

주류 공유 메모리 언어에서 프로그래머들은 데이터 레이스를 방지하기 위해 락(locks)과 같은 동기화 메커니즘을 사용하여 스레드 간의 공유 데이터 접근을 격리합니다. 하지만 동기화는 단지 시간적 순서(temporal ordering)만을 강제할 뿐이며, 공유 메모리는 여전히 모든 일반적인 읽기 및 쓰기 과정에서 스레드 간에 업데이트를 통신합니다. 따라서 프로그래머들은 순서와 통신의 관계를 이해하고, 컴파일러와 하드웨어가 그러한 가정을 기반으로 최적화하는 상황에서도 동기화를 올바르고 일관되게 적용해야 합니다. 프로그래머들이 잘못 동기화하면 격리를 잃고, 프로그램의 의미론(semantics)이 아무도 모르게 변경됩니다. 우리는 공유 메모리에 대한 접근 순서가 아닌, 격리(isolation)와 통신(communication)을 기반으로 하는 메모리 모델인 Sync-as-Share를 제안합니다. 우리는 각 스레드가 메모리의 사적인 뷰(private view)를 읽고 쓰는 스레드 격리(thread isolation)에서 시작하여, 프로그램의 기존 동기화 동작들이 업데이트를 명시적으로 통신하도록 재해석합니다. 아무것도 동기화 동작 외부에서 통신되지 않으므로, 데이터 레이스는 구조적으로 불가능해집니다. 대신, 충돌하는 업데이트는 동기화 지점(synchronisation points)에서 감지됩니다. 동기화를 명시적인 통신으로 간주하는 것은 무엇이 누구에게 전달되어야 하는지, 그리고 무엇이 충돌로 간주되는지에 대한 설계 결정을 노출합니다. 우리는 서로 다른 트레이드오프를 가진 두 가지 통신 토폴로지를 제안합니다. Java의 메모리 모델에 의해 이미 정의된 동기화 동작만을 스레드가 통신하는 유일한 지점으로 만들어 Sync-as-Share를 Java에 구현함으로써, Java 프로그램이 수정 없이 Sync-as-Share를 채택할 수 있도록 합니다. 우리는 이 구현을 버전 제어 메모리(version-controlled memory)로 형식화하며, 여기서 동기화 동작은 사적인 뷰 간에 업데이트를 밀고 당깁니다(push and pull). 그리고 이를 Rocq에서 메커니즘화합니다. 우리는 Java 메모리 모델 하에서 올바르게 동기화된 Java 프로그램이 공유 메모리와 Sync-as-Share 모두에서 동일하게 작동함을 보여줍니다.