"I love Simon Cooksey"

2022-06-12 04:59:14

Simon Cooksey Research Associate I study modern multiprocessor 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. Research Associate I am working on the CAPC research programme, funded by the UKRI investigation into Digital Security by Design. I am open to industrial collaboration investigating weak memory behaviours and the semantics of compiler optimised programs. I am happy to work on an ad-hoc contractor basis, or as part of a traditionally funded research program, please get in touch. Postgraduate I am a Post-doctoral researcher 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 completed my thesis in September 2021. In June 2020 I received the Kent Postgraduate Prize, recognising the impact of my research. Publications Mixed-Proxy Extensions to NVIDIA PTX An extension of NVIDIA's PTX ISA to support mixing load and store operations that target different proxies of memory. This gives well-defined semantics to programs with both, for example, constant loads and generic stores to the same address. The memory model extension was built in the relational model checking tool, Alloy, and we showed that our extension to the PTX model is sound and complete with respect to the existing industrial model. To appear in the proceedings of ISCA 2022. Mixed-Proxy Extensions for the NVIDIA PTX Memory Consistency Model Daniel Lustig, Simon Cooksey, Olivier Giroux @inproceedings{Lustig:2022, title={Mixed-Proxy Extensions for the NVIDIA PTX Memory Consistency Model}, author={Lustig, Daniel and Cooksey, Simon and Giroux, Olivier}, booktitle={Proceedings of the 49th {ACM/IEEE} International Symposium on Computer Architecture, {ISCA} 2022, New York, USA, June 11-15, 2022} year={2022}, publisher={{ACM/IEEE}}, note={To appear},} Pomsets with Predicate Transformers Pomsets with Predicate Transformers (PwT) is a recent fully denotational semantics for weak memory consistency. It captures program dependencies by embedding a logic into predicate transformers which compose to create proof burdens necessary to remove dependencies which are syntactic only from list of dependencies actually present in a program. I developed an OCaml tool to automatically evaluate PwT over a series of litmus tests. Appears in the proceedings of POPL 2022. The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffery, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, Anton Podkopaev [PDF] @inproceedings{Jeffrey:2022, title={The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency}, author={Jeffrey, Alan and Riely, James and Batty, Mark and Cooksey, Simon and Kaysin, Ilya and Podkopaev, Anton}, booktitle={Proceedings of the 49th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages, {POPL} 2022, Philadelphia, USA, January 18-20, 2022}, editor={Rajeev Alur and Hongseok Yang}, pages={54--84}, publisher={{ACM}}, year={2022}, url={https://doi.org/10.1145/3498716}} 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. ESOP 2020. Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty [PDF] @inproceedings{MPaviotti:ESOP20, title={Modular Relaxed Dependencies in Weak Memory Concurrency}, author={Pavoitti, Marco and Cooksey, Simon and Paradis, Anouk and Wright, Daniel and Owens, Scott and Batty, Mark}, booktitle="Programming Languages and Systems", editor="M{\"u}ller, Peter", year="2020", publisher="Springer International Publishing", address="Cham", pages="599--625",} 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 Complementing capabilities: introducing pointer-safe programming to DSBD tech (Innovate UK ICSF, 2022) I am a Researcher Co-Investigator for a grant of £494,770 (80% FEC) responding to the Innovate UK call to extend the DSbD ecosystem with new CHERI-compatible software. This work will be focussed on porting the Rust compiler to CHERI and formally demonstrating how the guarantees provided by Rust join up nicely with the guarantees of the capability hardware. Fixing the thin-air problem: ISO dissemination (VeTSS, 2020) I am a named researcher and co-author of a VeTSS grant of £60,455 (80% FEC) to pursue further 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 £485,168 (80% FEC). 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, [email protected]. 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. My CV is available too, although I am not currently looking for a job.