High-level managed languages, such as Java, provide strong semantic guarantees, but these guarantees are only as good as the underlying software stack. The research funded by this EAGER award will address the problem of verifying the compiler and runtime systems of managed languages and address the interplay between the formal verification of the underlying software stack and the memory models used by these languages
The correctness of safety-critical code is very important, but also very difficult to guarantee. Existing practice relies on manual code reviews and testing to ensure correctness, which are methods that do not provide strong guarantees. This research has the potential to improve the safety and robustness of managed-language implementations. These implementations, in turn, will improve the reliability of safety-critical software that runs on them.
In the EAGER project we have defined a new semantics for Java cognizant of the relaxed memory model existing in current x86 architectures. We have formalized this semantics in the Coq proof assistant, and used it to verify programs that implement components of a Java-like virtual machine. Furthermore, we defined a new methodology to verify the atomicity of certain pieces of concurrent code that supports reasoning about the relaxed memory model. To the best of our knowledge this is the first effort to achieve atomicity verification for a relaxed memory model. In more detail, we have leveraged the relaxed memory model of x86 architectures to the level of Java bytecode. To that end, we designed an Intermediate Representation that we use to compile Java programs to x86, and to implement the runtime components of the Java Virtual Machine, including the Garbage Collector. The importance of thie IR is that it is amenable to verification in the Coq proof assistant. We have deployed our develpment on top of the CompcertTSO certified C compiler, which we use as a backend. To support our claims, we wrote a Concurrent Garbage Collector in our intermediate representation, for which we later verified atomicity properties of certain crucial pieces. Our Atomicity Verification methodology was able to discharge the atomicity of important pieces of code, for which considering all possible interleavings would make the certification of the Garbage Collector intractable. Our preliminary results indicate that this methodology is not limited to the verification of the code of a compiler, but it can generally be applied to the verificaiton of concurrent code that exploits the x86 relaxed memory model semantics. Similarly, our developlemnt gives insights on how to further relax our atomicity verification methodology to cover more, perhaps more relaxed, memory models of different architectures. We consider our developments to be an important stepping-stone towards the end-to-end certification of a full Java infrastructure that embraces the relaxed memory concurrency present in current computer architectures.
