MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Correct Compilation of Relaxed Memory Concurrency

Soham Chakraborty
MMCI
SWS Student Defense Talks - Thesis Proposal
SWS  
Public Audience
English

Date, Time and Location

Thursday, 16 November 2017
14:00
60 Minutes
G26
111
Kaiserslautern

Abstract

Compilation of shared memory concurrent programs faces
many challenges in the presence of relaxed memory models.
On the one hand, relaxed memory models enable multiple
transformations on shared memory accesses and fences.
On the other hand, not all transformations which are correct
for sequential programs are correct in the concurrent setting.
Thus, compiler writers have to perform careful analysis to
determine which transformations are correct.

In my thesis, I explore the correctness of the multiple steps
during the compilation of concurrent C/C++ programs (termed
C11). First, I consider the correctness of C11 source to source
transformations. Next, I study the compilation of C11 programs
by LLVM, a state-of-the-art optimizing compiler. LLVM performs
a number of optimizing transformations before generating the
target code for architectures such as X86 and PowerPC. To
perform these transformations, LLVM follows an informal
refinement of C11 concurrency semantics. I formalize the
LLVM concurrency semantics and study at the abstract level
the correctness of various LLVM transformations. Finally,
I develop a validator to check if LLVM optimizations are
indeed performing only transformations that are correct
according to the LLVM and/or the C11 model.

Contact

--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only

Maria-Louise Albrecht, 11/02/2017 15:42 -- Created document.