Formal Semantics for C-like Languages

Dr Mark Batty, University of Cambridge

For performance, modern CPUs (and GPUs) admit relaxed behaviour: violations of sequential consistency. To enable efficient implementation above relaxed hardware without fencing simple memory accesses, programming languages like C11 and C++11/14 also admit relaxed behaviour, introducing substantial complexity to the programming model. My work provides a formal semantics for C11 and C++11/14 concurrency that was developed in close communication with the ISO committees that define the languages. The precise formal model has been used for several positive results: to identify and fix problems in the ISO specification, for proofs of the soundness of compilation mappings, in the development of formal reasoning principles, and in the proofs of basic tenets of the design. At the same time, the formal model allows us to criticise the design, and pinpoint its flaws.

In this talk I will review some of the positive results built on the formal C++11 memory model, including the proof of one of the key design goals of the language: that simple data-race-free programs are provided with sequentially consistent semantics (DRF-SC). I will then show that the C++11 memory model is fatally flawed when applied to C-like languages. I will discuss what might be done about this open problem, and I will talk about the extension of formal relaxed memory models to cover GPU computing.