Industrial concurrency specification for C/C++

Dr Mark Batty

Senior Lecturer, University of Kent

Modern computer systems have intricate memory hierarchies that violate the intuition of a global timeline of interleaved memory accesses. In these so-called relaxed-memory systems, it can be dangerous to use intuition, specifications are universally unreliable, and the outcome of testing is both wildly nondeterministic and dependent on hardware that is getting more permissive of odd behaviour with each generation. These complications pervade the whole system, and have led to bugs in language specifications, deployed processors, compilers, and vendor-endorsed programming idioms – it is clear that current engineering practice is severely lacking.

I will describe my part of a sustained effort in the academic community to tackle these problems by applying a range of techniques, from exhaustive testing to mechanised formal specification and proof. I will focus on a vein of work with strong industrial impact: the formalisation, refinement and validation of the 2011/14/17 C and C++ concurrency design, leading to changes in the ratified international standard, and ultimately uncovering fundamental flaws that lead us to the state of the art in concurrent language specification. This work represents an essential enabling step for verification on modern concurrent systems

About Dr Mark Batty

Batty has played a key role in the effort to understand relaxed concurrency in the pervasive C and C++ languages. He is a Senior Lecturer at Kent, with a fellowship from the Royal Academy of Engineering, supported by the Lloyds Register Foundation (2015–2020). Prior to his work, concurrency in the C and C++ languages was not well-defined. Batty worked with the ISO on the 2011, 2014 and 2017 revisions of the languages to define a rigorous formal model of C++ concurrency that is in tight correspondence with the standards [1]. He subsequently proved that C++ concurrency has fundamental problems that cannot be resolved without changing the founding paradigm of the design [2]. See: [1] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In POPL, 2011. [2] M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, and P. Sewell. The problem of programming language concurrency semantics. In ESOP at ETAPS, 2015.

Sponsored by