Pomsets with preconditions: a simple model of relaxed memory
Radha Jagadeesan, Alan Jeffrey, James Riely
Abstract
Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.
Topics & Concepts
Computer scienceThread (computing)CompilerSimple (philosophy)Memory modelProgramming languageTheoretical computer scienceParallel computingShared memoryPhilosophyEpistemologySecurity and Verification in ComputingParallel Computing and Optimization TechniquesDistributed systems and fault tolerance