Mark Batty, “Relaxed memory concurrency semantics and reasoning, Part 1”, VeTSS Summer School 2024

Talk by Mark Batty, University of Kent, at the VeTSS Summer School 2024. 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. 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.