School of Computing

Simon Cooksey

Research Student

Photo of Simon Cooksey
  • Room SW103
    School of Computing
    University of Kent, CT2 7NF


Modular Relaxed Dependencies in Weak Memory Concurrency: 29th European Symposium on Programming Languages (2020).
Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, and Mark Batty

P1780 Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem: ISO/IEC C/C++ Standards Committee Paper.
Presented to SG1 in Cologne 2019 and Belfast 2019.
Mark Batty, Simon Cooksey, Scott Owens, Anouk Paradis, Marco Paviotti, and Daniel Wright

PrideMM: Second Order Model Checking for Memory Consistency Models: 10th Workshop on Tools for Automatic Program Analysism (2019).
Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, and Mikoláš Janota

PhD Project Summary

I am in the PLAS research group, studying Weak Memory behaviours with Mark Batty.

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

Internship at 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.

If you are a PhD Student who is interested in what an internship can offer for your research, feel free to email me and ask questions.


I have taught

I primarily teach on Programming Language theory courses.

Research Interests

I am a member of the following research groups:

My research interests relate to Weak Memory Models, Semantics, and Correctness.

Other interests

In my free time I like to fly gliders. I keep a personal website here, and I can be found on the KentIRC.

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 24/10/2020