DISCOVER is an ANR JCJC 2014 project. Grant nºANR-14-CE28-0004. The DISCOVER project ended on september 30th, 2019.

Shared-memory concurrency is pervasive in modern software and multiprocessors hardware systems, yet it remains a challenge to program. Standard multiprocessors (x86, Power, ARM etc) and mainstream programming languages (C, C++, Java) have subtle, weakly consistent, memory models, exposing complex and counter-intuitive behaviors to the programmer. This complexity is rooted in the aggressiveness of the optimizations performed by compilers and hardware, which make programs behave as if some of the instructions would execute out-of-order. This complex semantics makes programming in such a setting particularly error-prone. Hence the need to establish program correctness is very strong.

In this context, traditional techniques, such as the one used in the safety-critical industry hardly apply: manual inspection of binary and source code would be too costly, and testing multi-threaded applications is particularly hard, as relaxations exposed by the weak memory models occur with a very low frequence, and are almost never reproducible. Thus, proving program correctness statically, by means of static analysis, deductive program proof or model checking, becomes an attractive approach due to its exhaustive cover of possible executions. Recent years have witnessed considerable progress in the formalization of weak memory models for both hardware and languages, and verification techniques, based on program logic, start to emerge. However, these verification tools are usually applied at the source level of programs, and miscompilation (i.e. a bug in the compiler) could invalidate those hard-won guarantees.

Compiler correctness for shared-memory concurrency remains a wide-open problem, compared to the sequential case, and Leroy et al.'s ground-breaking achievements with the CompCert verified C compiler. Indeed, besides the challenges to verification that application-level concurrency introduces, components of the implementation may also run concurrently with application threads, improving scalability and performance, at the cost of additional complexity. The interaction among components is typically regulated by compiler-injected code that maintains and updates information useful to the runtime system during program execution. Examples of such code include handlers for memory allocation fast paths, read and write barriers for memory management, fences, etc. These concurrent snippets are sophisticated, can contain data-races (i.e. simultaneous, conflicting accesses to shared-memory), and must operate correctly in an environment subject to program transformations.

The DISCOVER project aims at leveraging recent foundational work on formal verification and proof assistants to design, implement and verify compilation techniques used for high-level concurrent and managed programming languages. The ultimate goal of DISCOVER is to devise new formalisms and proof techniques able to scale to the mechanized correctness proof of a compiler involving a rich class of optimizations, leading to efficient and scalable applications, written in higher-level languages than those currently handled by cutting-edge verified compilers.

In the light of recent work in optimizations techniques used in production compilers of high-level languages, control-flow-graph based intermediate representations seems too rigid. Indeed, the analyses and optimizations in these compilers work on more abstract representations, where programs are represented with data and control dependencies. The most representative representation is the sea-of-nodes form, used in the Java Hotspot Server Compiler, and which is the rationale behind the highly relaxed definition of the Java memory model. DISCOVER proposes to tackle the problem of verified compilation for shared-memory concurrency with a resolute language-based approach, and to investigate the formalization of adequate program intermediate representations and associated correctness proof techniques.