Wednesday 14th August, Afternoon session
Mark Batty, University of Kent
BACKGROUND:
Processors and GPUs are concurrent, they rely on shared memory to communicate, and they feature complex and varied memory subsystems. Compilers aggressively optimise code through thread-local analysis and by leveraging global invariants. As a consequence, these systems admit relaxed memory behaviours, where no sequential interleaving of each thread’s memory accesses can explain the observed behaviour. Relaxed memory behaviours can be extremely subtle and they can be elusive: these behaviours have been missed and misrepresented by the official specifications of processors and languages.
PREPARATION:
In these lectures, we will review techniques for formally describing the semantics of relaxed memory systems. These formalisms have been adopted by processor vendors and languages specifiers, but understanding the semantics of compiler optimisations is ongoing work. Established verification techniques assume orderings that are not preserved under relaxed memory, we will discuss how these techniques must be altered to match the behaviour that modern systems guarantee.
SPEAKER:
Mark Batty is a Professor at the University of Kent, where he works on the development of rigorous mathematical specifications, testing tools, and verification techniques for real-world concurrent systems, with a focus on established interfaces (e.g. C, C++ and, OpenCL) and concrete testable artefacts (e.g. x86, Power, ARM CPUs, and Nvidia, AMD GPUs). For his latest direction, see this Royal Society position paper.