Loading…
This event has ended. View the official site or create your own event → Check it out
This event has ended. Create your own
View analytic
Monday, March 27 • 15:15 - 15:55
Formalizing the Concurrency Semantics of an LLVM Fragment

Sign up or log in to save this to your schedule and see who's attending!

The LLVM compiler follows closely the concurrency model of C/C++ 2011, but with a crucial difference. While in C/C++ a data race between a non-atomic read and a write is declared to be undefined behavior, in LLVM such a race has defined behavior: the read returns the special `undef' value. This subtle difference in the semantics of racy programs has profound consequences on the set of allowed program transformations, but it has been not formally been studied before.

This work closes this gap by providing a formal memory model for a substantial fragment of LLVM and showing that it is correct as a concurrency model for a compiler intermediate language:
(1) it is stronger than the C/C++ model. (2) weaker than the known hardware models, an. (3) supports the expected program transformations.
In order to support LLVM's semantics for racy accesses, our formal model does not work on the level of single executions as the hardware and the C/C++ models do, but rather uses more elaborate structures called event structures.

Speakers
SC

Soham Chakraborty

Max Planck Institute for Software Systems (MPI-SWS)


Monday March 27, 2017 15:15 - 15:55
E2 2 (Günter Hotz Hall)

Attendees (11)