Correct Compilation of Relaxed Memory Concurrency

Summary

Shared memory concurrency is the pervasive programming model for multicore architectures such as x86, Power, and ARM. Depending on the memory organization, each architecture follows a somewhat different shared memory model. All these models, however, have one common feature: they allow certain outcomes for concurrent programs that cannot be explained by interleaving execution. In addition to the complexity due to architectures, compilers like GCC and LLVM perform various program transformations, which also affect the outcomes of concurrent programs.

To be able to program these systems correctly and effectively, it is important to define a formal language-level concurrency model. For efficiency, it is important that the model is weak enough to allow various compiler optimizations on shared memory accesses as well as efficient mappings to the architectures. For programmability, the model should be strong enough to disallow bogus ``out-of-thin-air'' executions and provide strong guarantees for well-synchronized programs. Because of these conflicting requirements, defining such a formal model is very difficult. This is why, despite years of research, major programming languages such as C/C++ and Java do not yet have completely adequate formal models defining their concurrency semantics.

In this thesis, we address this challenge and develop a formal concurrency model that is very good both in terms of compilation efficiency and of programmability. Unlike most previous approaches, which were defined either operationally or axiomatically on single executions, our formal model is based on event structures, which represents multiple program executions, and thus gives us more structure to define the semantics of concurrency.

In more detail, our formalization has two variants: the weaker version, WEAKEST, and the stronger version, WEAKESTMO. The \weakest model simulates the promising semantics proposed by Kang et al., while WEAKESTMO is incomparable to the promising semantics. Moreover, WEAKESTMO discards certain questionable behaviors allowed by the promising semantics. We show that the proposed WEAKESTMO model resolve out-of-thin-air problem, provide standard data-race-freedom (DRF) guarantees, allow the desirable optimizations, and can be mapped to the architectures like x86, PowerPC, and ARMv7. Additionally, our models are flexible enough to leverage existing results from the literature to establish data-race-freedom (DRF) guarantees and correctness of compilation.

In addition, in order to ensure the correctness of compilation by a major compiler, we developed a translation validator targeting LLVM's ``opt'' transformations of concurrent C/C++ programs. Using the validator, we identified a few subtle compilation bugs, which were reported and were fixed. Additionally, we observe that LLVM concurrency semantics differs from that of C11; there are transformations which are justified in C11 but not in LLVM and vice versa. Considering the subtle aspects of LLVM concurrency, we formalized a fragment of LLVM's concurrency semantics and integrated it into our WEAKESTMO model.

Main Text (PDF)

Technical appendix (PDF)

Related projects

Imprint | Data protection