Simon Cooksey

PhD Student

I study modern multi-processor computers to understand the behaviours admitted by their complex micro-architectural designs. My research has focussed particularly on so-called weak memory behaviours, which are exhibited on machines that allow out-of-order execution and caching.

These intricate behaviours present challenges for programmer reasoning. Formal models help to clarify precisely what is allowed, and my tools bridge the gap between mathematical formalisation and programmer intuition about computer behaviour. My tools make these formal models executable. This informs the development of the model by allowing quick refinement of definitions, and also permits a programmer to probe the behaviour of a model to grasp the precise meaning of a given program.

These models stand as cutting edge specifications for verification of concurrent programs executing on modern high-performance hardware.

Postgraduate

I am a PhD candidate in the Programming Languages and Systems group at the University of Kent. I work with Mark Batty researching weak memory behaviours and compiler verification. My academic profile page is here. I am currently writing up my thesis.

In June 2020 I recieved the Kent Postgraduate Prize, recognising the impact of my research.

Publications

Modular Relaxed Dependencies

Modular Relaxed Dependencies (MRD) is a denotational semantics for weak memory consistency in C and C++. As well as helping to define the denotation, I built an evaluation tool (MRDer) in OCaml to enable fast calculation of the semantics against a corpus of litmus tests. Further, I proved meta-theoretic properties about the semantics with respect to industry standard models of C/C++.

Modular Relaxed Dependencies in Weak Memory Concurrency. To appear, ESOP 2020.
Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty
[PDF]
@inproceedings{MPaviotti:ESOP20,
  author="Paviotti, Marco and Cooksey, Simon and Paradis, Anouk and Wright, Daniel and Owens, Scott and Batty, Mark",
  title="Modular Relaxed Dependencies in Weak Memory Concurrency",
  booktitle="Proceedings of the 29th European Symposium on Programming Languages",
  year="2020",
  note="To appear"
}
P1780R0: Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem. ISO/IEC JTC1/SC22/WG21.
Mark Batty, Simon Cooksey, Scott Owens, Anouk Paradis, Marco Paviotti, Daniel Wright
Online working document
@techreport{MBatty:P1780,
  author="Batty, Mark and Cooksey, Simon and Owens, Scott and Paradis, Anouk and Paviotti, Marco and Wright, Daniel",
  title="Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem",
  institution="ISO/IEC JTC1/SC22/WG21",
  month="June",
  year="2019",
  number="P1780R0"
}

PrideMM

PrideMM is a tool written in OCaml which provides an API for building Second Order logical formulae and uses this API to express memory models. We use cutting edge Quantified Boolean Formulae (QBF) solvers to efficiently simulate a new class of memory model which solve the thin-air problem. We encode the problems in a high-level second order logic giving us flexibility in problem expression. This then gets translated into a QBF model checking problem for a solver to efficiently execute.

PrideMM: Second Order Model Checking for Memory Consistency Models. TAPAS 2019.
Simon Cooksey, Sarah Harris, Mary Batty, Radu Grigore, Mikoláš Janota
[PDF]
@inproceedings{SCooksey:TAPAS19,
  author="Cooksey, Simon and Harris, Sarah and Batty, Mark and Grigore, Radu and Janota, Mikol\'{a}\v{s}",
  title="PrideMM: Second Order Model Checking for Memory Consistency Models",
  booktitle="10th Workshop on Tools for Automatic Program Analysis",
  year="2019"
}

Grants

Fixing the thin-air problem: ISO dissemination
(VeTSS, 2020)

I am a named researcher and co-author of a VeTSS grant of £60,455 to persue futher integration of MRD into the ISO C++ Standard. This grant funds travel to ISO meetings, and research time for me to prepare papers ahead of these meetings.

CAPC: Capability C semantics, tools and reasoning
(Digital Security by Design, 2020)

I am a named researcher and co-author of a Digital Security by Design Grant of £596,634. This is a longer term project to build verified concurrent libraries for the CHERI platform. CHERI is an interesting extension to ARM where memory accesses are tagged with capabilities to keep code secure.

Industrial Experience

NVIDIA

As an intern at NVIDIA I extended the Memory Consistency Model for NVIDIA’s virtual instruction set (PTX) to support "memory views". This enables writing well defined programs which mix generic load and store operations with specialised load and store operations for texture, surface and constant accesses.

XMOS

I worked for the Bristol based semiconductor company XMOS. XMOS produce a line of multi-core embedded processors called the xCORE. I built tools and applications for the platform, including a port of an MP3 library, lib_mp3 and adaptations to their debugging toolchain to enable remote debugging of hardware targets over the network, and to allow interfacing the debugger with a fast simulator.

Undergraduate

I graduated from the University of Kent with a First in Computer Science with a Year in Industry.

TinkerSoc

I was the president of TinkerSoc, a society dedicated to making things, particularly electronics.

Contact

You can contact me via email, sjc205@kent.ac.uk. I use PGP, so if that floats your boat: my PGP fingerprint is 49BC 8FD6 E61B B9CA BA97 A33C 33AA 9C37 025D 2B62 and I have a keybase profile here.

My CV can be found here.