Pomsets with Preconditions: A Simple Model of Relaxed Memory
summary
A denotational memory model called pomsets with preconditions represents executions as labeled partial orders augmented with logical preconditions, uses fulfillment rules to decide reads, and restricts to MCA hardware with a single publication order to avoid POWER anomalies. The paper gives a compositional proof rule for past‑time propositional linear temporal logic, proves local data race freedom, describes an efficient ARM compilation strategy, shows common optimizations and internal reads validate, and notes limits: no POWER, loops, or mixed‑size accesses yet.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:12Memory model
- 1:51Preconditions for dependency Pomset a single execution
- 3:04Can this program write 1 to z?
- 6:08Comparing attempted executions
- 7:05We've been trying for 20 years...
- 8:19Semantic Operations (1/2)
- 10:38Concurrent Semantics: Fulfillment
- 11:22Buffering
- 11:37Publication
- 11:59Coherence
- 12:48Internal Reads+Synchronization
- 13:27Other Transformations
- 14:02Local data race freedom
- 14:26Other results and limitations
related talks
21mCSL and relaxed memory
23mA Reachability Logic for a Weak Memory Model with Promises
20mThe Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc
16mCompositional Symbolic Execution for the Next 700 Memory Models
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
14mMaking Weak Memory Models Fair
22mProbabilistic Refinement Session Types