Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
summary
Extends x86 semantics to cover non-temporal stores and page memory types, delivering EX86/PEx86 models in both operational and declarative forms and proving their equivalence; validates via diy/klitmus with 2,200 tests run on Core i5/6 and Xeon implementations (some tests exercised up to 600 million runs or more); reports that the Intel manual is wrong about non-temporal stores — non-temporal stores behave differently and can exhibit both store-buffering and message-passing; classifies WB/WT as TSO, UC as SC, and WC as allowing write–write reordering but forbidding store–read reordering.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 0:37Store Operations
- 1:36Memory Cache
- 2:40Ex86
- 2:56TSO
- 4:33canonical litmus tests
- 7:42strong uncashable
- 8:12strong ordering
- 8:43WC memory
- 9:26Weak ordering
- 9:57Nontemporal stores
- 10:58Validation
- 12:15Order Table
- 13:54Ex86 Model
- 14:24What is Consistency
- 15:32Sequential programs
- 17:17Consistency vs Consistency
- 17:38Extension Model
- 17:56Operational Model
- 18:20Examples
- 18:42Conclusion
related talks
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
16mPersistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-
01h 11mProgramming language memory models: Problems, solutions, and directions
23mMemory Consistency Model Status Update
23mPersistence Semantics for Weak Memory
25mParametrised Verification of Intel-x86 Programs
16mCompound Memory Models