Research

Relaxed Memory Semantics

Modern processors and compilers reorder memory operations for performance, breaking the intuition of a single, sequentially consistent memory. My work verifies concurrent algorithms against the weak memory models that result, establishing that they remain correct under the relaxed orderings these models permit.

Publications

All publications on ResearchGate →

Blog Posts

Links

  • Relaxed Memory Model Zoo
    A living survey of 107 weak memory models and the 161 evidence-typed relations between them.
  • rmm-zoo-dataset
    The machine-readable dataset behind the Zoo, where corrections and additions go.
  • MoRDor
    A weak memory explorer for C-like programs: it computes a litmus test's justified executions and checks them against sMRD, RC11, IMM and 37 more models from the Zoo. The reference implementation of Symbolic Modular Relaxed Dependencies (sMRD), in OCaml.