JCJC SIMI 2 - JCJC - SIMI 2 - Science informatique et applications

Weak Memory Concurrency and Verified Compilation – WMC

Submission summary

Multiprocessors and multicore processors are now ubiquitous, but programming these systems, to deliver high-performance and reliable systems, is very challenging. Shared-memory is the programming abstraction exported by the hardware, and most multi-threaded programs communicate through memory shared between the threads. Traditionally concurrent execution was viewed as simply an interleaving of the steps from the threads participating in the computation. Thus if we started in an initial state in which all variables are zero, and one thread executes:

x = 1; r1 = y;

while another executes

y = 1; r2 = x;

either the assignment to x or the assignment to y must be executed first, and either r1 or r2 must have a value of one when the execution completes. However, it has proven impractical to guarantee such a restrictive memory behaviour, and all realistic programming language implementations supporting true concurrency allow both r1 and r2 to remain zero in the above example. There are two reasons for this:

- for efficiency reasons, compilers may reorder memory operations if that doesn't violate intra-thread dependencies;

- the hardware may reorder memory operations based on similar constraints.

The forthcoming revision of the C++ standard (the C standard will be updated accordingly to preserve compatibility) specifies all the constraints that the possible outcomes of a parallel program must respect. This requires special architecture-dependent support in C and C++ compilers.

The goal of this grant proposal is to investigate the formal verification of realistic compilers for concurrent dialects of the mainstream languages C and C++. We will target both the x86 and Power/ARM architectures, which require radically different compilation strategies and proof methods, focussing initially on sample compilation schemes and then lifting these results to fully-fledged compilers. In addition we will design and prove correct novel compile-time optimisations for these languages and compilers.

Project coordination

Francesco ZAPPA NARDELLI (INRIA Paris-Rocquencourt) – francesco.zappa_nardelli@inria.fr

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

INRIA INRIA Paris-Rocquencourt

Help of the ANR 204,880 euros
Beginning and duration of the scientific project: January 2012 - 48 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter