Dissertation Award for Mark Batty

Dr Mark Batty profile picture

Dr Mark Batty has won the 2015 John C Reynolds Doctoral Dissertation Award. This prestigious prize is presented annually to the author of an outstanding doctoral dissertation in the area of Programming Languages from submissions received globally.

Mark, who is joined the School of Computing as a Lecturer in March 2015, completed his dissertation titled The C11 and C++11 Concurrency Model while at the University of Cambridge.

The dissertation award is given by ACM SIGPLAN, a special interest group of ACM that focuses on programming languages. In particular, SIGPLAN explores the design, implementation, theory, and efficient use of programming languages and associated tools.

The selection committee for the award consists of leading academics and industry leaders in computing.

The abstract, taken from Mark’s thesis:

Relaxed-memory concurrency is now mainstream in both hardware and programming languages, but there is little support for the programmer of such systems. In this highly non-deterministic setting, ingrained assumptions like causality or the global view of memory do not hold. It is dangerous to use intuition, specifications are universally unreliable, and testing outcomes are dependent on hardware that is getting more permissive of odd behaviour with each generation. Relaxed-memory concurrency introduces complications that pervade the whole system, from processors, to compilers, programming languages and software.

There has been an effort to tame some of the mystery of relaxed-memory systems by applying a range of techniques, from exhaustive testing to mechanised formal specifica- tion. These techniques have established mathematical models of hardware architectures like x86, Power and ARM, and programming languages like Java. Formal models of these systems are superior to prose specifications: they are unambiguous, one can prove proper- ties about them, and they can be executed, permitting one to test the model directly. The clarity of these formal models enables precise critical discussion, and has led to the dis- covery of bugs in processors and, in the case of Java, x86 and Power, in the specifications themselves.

In 2011, the C and C++ languages introduced relaxed-memory concurrency to the language specification. This was the culmination of a six-year process on which I had a significant impact. This thesis details my work in mathematically formalising, refining and validating the 2011 C and C++ concurrency design. It provides a mechanised formal model of C and C++ concurrency, refinements to the design that removed major errors from the specification before ratification, a proof in HOL4 (for a restricted set of programs) that the model supports a simpler interface for regular programmers, and, in collaboration with others, an online tool for testing intuitions about the model, proofs that the language is efficiently implementable above the relaxed x86 and Power architectures, a concurrent reasoning principle for proving specifications of libraries correct, and an in-depth analysis of problems that remain in the design.