Simplifying Reasoning under Weak Memory Concurrency

Abstract

본 논문에서는 느슨한 메모리에서 동시성 프로그램을 구현하는 것을 쉽게 만드는 방법을 제시한다. 쓰레드들이 같은 메모리에 접근하는 동시성 프로그램에서는 하드웨어와 컴파일러의 최적화 덕분에 굉장히 비직관적인(혹은, 느슨한) 행동이 일어난다. 이러한 느슨한 메모리 행동까지 전부 고려해서 프로그램을 올바르게 구현하는 것은 굉장히 어렵다. 우리는 느슨한 메모리 행동을 거의 고려하지 않고도 쉽고 프로그램을 구현할 수 있게 만드는 두 이론을 개발했다. 먼저, 데이터 경쟁이 없는 메모리 영역에서는 느슨한 메모리 행동이 일어나지 않는다는 부분적 무경쟁 보장을(Local Data-Race-Freedom Guarantees) 엄밀히 나타내고 증명했다. 이를 통해 데이터 경쟁을 피하는 프로그래머는 느슨한 메모리를 고려하지 않고도 동시성 프로그램을 올바르게 이해하고 작성할 수 있다. 다음으로, 동시성 프로그램을 최적화할 때 느슨한 메모리 행동과 동시성을 무시할 수 있게 해주는 이론을 개발했다. 느슨한 메모리의 복잡성을 전혀 가지지 않으며 싱글 쓰레드만 있는 것처럼 동작하는 모델 SEQ를 개발했고, 느슨한 메모리 동시성에서 올바른 최적화를 구현하기 위해서는 SEQ 위에서의 실행만 고려하면 된다는 것을 보였다. 이 결과들은 느슨한 메모리 행동을 설명하는 모델인 약속 메모리 모델을(Promising Semantics) 통해 옳다는 것이 검증되었다.

This thesis presents ways to easily implement concurrent programs in weak memory. In shared memory concurrency, programs have counterintuitive (or weak) behavior due to hardware and compiler optimizations. It is difficult to implement a correct program with a full understanding of weak behavior. I develop two theories that simplify reasoning under weak memory concurrency. First, I formalize and prove local data-race-freedom guarantees that ensure strong semantics for locations accessed by non-racy instructions. These allow programmers who avoid data races to understand and write concurrent programs without understanding of weak behavior. Next, I show that sequential reasoning is adequate and sufficient for establishing soundness of compiler optimizations under weak memory. I introduce a sequential model SEQ which has no weak behavior and no concurrency, and show that correct optimizations under SEQ executions are also correct under weak memory. Our results are fully verified against a weak memory model, the promising semantics.