Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Correct Compilation of Relaxed Memory Concurrency
Speaker:Soham Chakraborty
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Defense
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Tuesday, 16 July 2019
Duration:60 Minutes
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 a 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, ARMv7. Additionally, our models are flexible enough to leverage existing results from the literature. 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.

Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:005
Meeting ID:SWS Space 2 (6312)
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Carina Schmitt, 07/02/2019 02:05 PM
  • Maria-Louise Albrecht, 07/02/2019 10:31 AM -- Created document.