PI: Mark Batty, University of Kent

  • Concurrency in the C++ language is ill-specified in the current International Standards Organisation (ISO) definition: it allows values to be conjured out of thin air (OOTA).
  • Working towards verification of C++ code, we fixed this problem with a proposed change to the standard called Modular Relaxed Dependencies (MRD).
  • We presented our proposal to the ISO, and they voted unanimously to pursue it.
  • We developed a refinement relation that can be used to verify C++ code.
  • Further flaws recently uncovered in the standard must be rectified before full verification of data structure libraries is possible.

C and C++ semantics are an ongoing academic/industrial effort. The memory behaviour of modern systems is extremely subtle. Processor vendors avoid the cost of fully hiding micro-architectural details, such as buffering and speculation, by permitting unintuitive program executions. Compiler optimisations alter accesses to memory to similar effect. The end result is a system with relaxed memory behaviour: behaviour that deviates from sequential consistency (SC), where concurrent memory accesses are simply interleaved.

Relaxed memory breaks intuitions about system behaviour leading to bugs in language specifications, deployed processors, compilers, and vendor endorsed programming idioms – it is clear that current engineering practice is severely lacking. We have an ongoing academic/industrial partnership with the International Standards Organisation (ISO) that has exposed fundamental flaws in the way we specify programming languages.

We have shown that the state-of-the-art definitions of C and C++ concurrency are broken — a problem that stems from a tension between performance and the strength of ordering guarantees provided to programmers. Compilers optimise away some syntactic dependencies, but these programming patterns are an idiomatic way to provide ordering in machine code, and if they are left in place, they serve as a cheap source of ordering at the language level.

The language definition must specify which dependencies are left in place: too many, and useful optimisations will be forbidden, as in Java Hotspot; too few, and the semantics of the language permits bizarre behaviour, as in C++. It is provably impossible to strike this balance in C++ by making only minor changes to the concurrency design, so a different approach was necessary. To reason about code, we must fix these problems.

As part of this VeTSS project, we developed Modular Relaxed Dependencies, a model for C++ concurrency which is recognised by the ISO as the best solution to the pernicious OOTA problem. We went on to develop a refinement relation for this model that allows one to verify the correctness of C++ code. Most data structures use pointers, and as part of this work, we started to examine further newly-recognised flaws in the specification of pointers in C++.

PUBLICATIONS. M. Batty, S. Cooksey, S. Owens, A. Paradis, M. Paviotti, and D. Wright. “Modular relaxed dependencies: A New Approach to the Out-of-Thin-Air Problem”. ESOP 2020.

IMPACT. The ISO unanimously passed the following motion endorsing our semantics: “OOTA is a major problem for C++, modular relaxed dependencies is the best path forward we have seen, and we wish to continue to pursue this direction.”