Weak Memory Concurrency and Verified Compilation – WMC

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.