Portrait of Simon Cooksey

Simon Cooksey

Research Student

About

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 {}, 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.

Research interests

I am a member of the following research groups:

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

Publications

Modular Relaxed Dependencies in Weak Memory Concurrency: To appear at ESOP 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: 10 Workshop on Tools for Automatic Program Analysism 2019. 
Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, and Mikoláš Janota

Teaching

I have taught

I primarily teach on Programming Language theory courses.

Last updated