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 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
- CO545: Functional and Concurrent Programming
- CO657: Internet of Things
- CO658: Programming Language Implementation
- CO661: Theory and Practice of Concurrency
- CO663: Programming Languages: Applications and Design
- CO883: Systems Architecture
I primarily teach on Programming Language theory courses.
I am a member of the following research groups:
My research interests relate to Weak Memory Models, Semantics, and Correctness.
In my free time I like to fly gliders. I keep a personal website here, and I can be found on the KentIRC.