| Title | : | Relaxed Memory Concurrency and Compiler Correctness |
| Speaker | : | Soham Chakraborty (Max Planck Institute for Software Systems) |
| Details | : | Tue, 12 Mar, 2019 11:00 AM @ A M Turing Hall |
| Abstract: | : | In most analysis/verification techniques, the behavior of concurrent programs is understood in terms of thread interleavings, a model formally known as sequential consistency (SC). For performance reasons, modern hardware implementations allow some executions which cannot be explained by thread interleavings. Similarly, standard compiler optimizations can affect the outcome of concurrent programs in ways that cannot be understood by SC. Therefore, to program concurrent systems correctly and effectively, it is important to come up with a programming language semantics that accounts for all the non-SC behaviors that hardware and compilers produce. Defining such a relaxed memory model is challenging due to conflicting requirements: the model should not only enable efficient compilation but also provide programmability guarantees. In this talk, I will introduce relaxed memory consistency and present our work on formally defining a good concurrency model for C/C++. As an application of our model, I will also present a translation validator for the optimizations of LLVM, a state-of-the-art C/C++ compiler. The validator has exposed bugs in LLVM concerning the compilation of concurrent C/C++ programs and has revealed interesting differences between the C/C++ and LLVM concurrency semantics. Bio: Soham Chakraborty is a PhD candidate in Max Planck Institute for Software Systems (MPI-SWS), Germany. His main research interests are relaxed memory concurrency and compiler correctness. He received the BE in Computer Science and Engineering from Vidyasagar University and the MS in Computer Science and Engineering from IIT Kharagpur. He has worked in various industrial research and development positions for 5 years before joining PhD. |
