Understanding and Fulfilling the Desiderata for Relaxed Memory Models

Abstract

Defining a relaxed memory model has been a major challenge for a couple of decades. The challenge stems from a sharp conflict between the two desiderata for relaxed memory models, usability and efficiency. Usability requires a model to be sensible and understandable, allowing programmers to use the model for developing and reasoning about concurrent programs. Efficiency requires a model to be efficiently implementable, i.e., it validates common compiler transformations and can be efficiently mapped to hardware. While the two desiderata are the key principles in designing a relaxed memory model, a significant challenge exists in balancing between them. This dissertation thoroughly understands the desiderata for relaxed memory models, identifies inherent conflicts between them, and resolves the conflicts at a minimal price. The first part of this dissertation presents PS 2.0, the first relaxed memory model that provably supports compiler transformations based on global analyses. PS 2.0 redesigns the key components of the promising semantics (PS) by Kang et al. and validates global value optimization and register promotion, while preserving the known results for PS, such as data-race-freedom guarantees. PS 2.0 also resolves the problem of the inefficiency in compiling read-modify-write (RMW) operations of PS to Armv8, which requires an unintended extra fence. The second part investigates the problem of developing an in-order memory model that executes instructions following their program order, placing emphasis on amenability to reasoning and verification. We demonstrate that an in-order model can validate all the compiler optimizations performed on single-threaded code by utilizing the distinction between an in-order source model and an out-of-order intermediate representation model. For atomics, we propose a pragmatic solution for mapping relaxed writes, for which reordering with previous reads should be prevented, with negligible performance overhead.

느슨한 메모리 모델을 정의하는 것은 수십 년 간 프로그래밍 언어 분야의 중요한 난제로 여겨져 왔다. 문제는 느슨한 메모리 모델에 대한 두 가지 주요 요구사항인 사용성과 효율성이 첨예하게 대립하는 데에 기인한다. 사용성은 모델이 상식적이고 이해할 수 있어야 한다는 것으로, 프로그래머가 메모리 모델을 이용하여 동시성 프로그램을 개발하고 논증할 수 있도록 한다. 효율성은 모델을 효율적으로 컴파일할 수 있어야 한다는 것으로, 메모리 모델이 일반적인 컴파일러 최적화를 허용하고, 하드웨어로도 효율적으로 컴파일될 수 있어야 함을 의미한다. 이 두 가지 요구사항은 느슨한 메모리 모델을 설계하는 데 있어 핵심적인 원칙이지만, 두 원칙을 모두 충족하는 메모리 모델을 정의하는 것은 매우 어려운 일이다. 본 학위논문에서는 느슨한 메모리 모델에 요구되는 성질을 깊게 이해하고, 여러 요구사항 사이의 본질적인 충돌을 발견하며, 이러한 충돌을 최소한의 비용으로 해결하는 느슨한 메모리 모델을 설계한다. 먼저 본 논문에서는 글로벌 분석에 기반한 컴파일러 최적화를 지원하는 최초의 느슨한 메모리 모델인 PS 2.0 모델을 제안한다. PS 2.0은 기존 모델인 Promising semantics (PS)의 핵심 요소를 새롭게 설계하여 데이터 경쟁 정리를 비롯한 PS에 대한 기존의 결과를 보장하면서도 글로벌 값 분석을 이용한 최적화 및 레지스터 프로모션을 지원한다. 또한, PS 2.0은 기존 PS의 RMW 연산을 Armv8 아키텍처로 컴파일 할 때 발생하는 비효율성 문제를 해결하였다. 두 번째로 프로그램 명령어를 순서대로 실행하면서도 사실상의 성능 저하를 수반하지 않는 쉽고 간단한 메모리 모델을 제안한다. 먼저, 순서대로 실행하는 프로그래밍 언어 모델과 순서를 바꾸어 실행하는 컴파일러 중간 언어 모델을 분리함으로써 프로그래머에게 간단한 모델을 제공하면서도 기존 컴파일러가 수행하는 모든 컴파일러 최적화를 지원하는 방법을 고안하였다. 하드웨어로 컴파일할 때는 일부 쓰기 명령어가 앞선 읽기 명령어와 순서가 바뀌어 실행되는 것을 방지해야 하는데, 이를 사실성의 성능 저하 없이 구현하는 방법을 소개한다.