The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
summary
Extends existing axiomatic models for x86, Power, ARMv8 and C++ with concrete TM rules and proves sanity properties (transactions never enable previously forbidden behaviours), checks compiler mappings, and uses a constraint-solver test synthesis to produce small litmus tests (up to six–seven events) then runs them many times (often ~100,000 trials) on x86 and Power, observing forbidden behaviours never occur. Discovers an ARMv8 lock elision incompatibility that permits a surprising X==2 outcome.
AI-written summary · about
chapters (6)
- 0:00Introduction to the topic
- 1:04Understanding weak memory
- 5:25Integrating transactions
- 7:55Validation methods
- 11:12Lock elision applications
- 14:14Conclusion and Q&A
related talks
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
01h 11mProgramming language memory models: Problems, solutions, and directions
22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
20mRelaxed systems semantics and how we (hope to) reason above it
21mWeak Memory Demands Model-based Compiler Testing
30mA Tale of Shared Memory Concurrency in Programming Languages
01h 00mWhat did C++ do for Transactional Memory?