PI: Mark Batty, Co-I: Simon Cooksey, University of Ken

  • 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).
  • The ISO has acknowledged our approach as its best path forward to fix the problems of C and C++.

The path taken in this project was radically different than proposed because COVID-19 interrupted ISO meetings quite severely. With the ISO meetings postponed or cancelled, we pivoted from planning in-person travel to the development of online interactive tools, reallocating travel resources that could not be spent to equipment for remote and future in-person demos, and hiring Abigail Pattenden to develop a web-based interface to our executable model, MRDer, for remote experimentation by committee members.

Pattenden, Cooksey, Batty then attended ISO meetings, presenting MRDer to the concurrency subgroup. Following this project, we secured a larger grant for studying C semantics.

We have previous experience of making changes to the ISO definitions of C and C++, and instrumental to our changes was the CPPMem tool. CPPMem allows one to explore the behaviour of small test programs online, under the C++ concurrency specification. ISO committee members use CPPMem to answer their own questions about corner cases of the concurrency specification.

We have exposed further problems in the concurrency specification of C++, problems that require more fundamental change. MRD is a possible solution to those problems, and ISO SG1 voted to pursue this direction. To present the finer details of MRD at a time with no in-person meeting, we developed an online variant of our new model, following the familiar style of the previous CPPMem tool (see above). The tool itself is available here.

PUBLICATION. JEFFREY, A., Riely, J., Batty, M., Cooksey, S., KAYSIN, I. and PODKOPAEV, A. ‘The Leaky Semicolon’, Principles of Programming Languages. ACM, pp. 1-30, (2022)

RELATED GRANTS. Mark Batty, PI; S. Kell, Co-I. UKRI DSbD grant “CapC: Capability C semantics, tools and reasoning” (EP/V000470/1), 08/2020-07/2023, £485,168.

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”