Coarser Equivalences for Causal Concurrency
summary
Proves a linear space lower bound for deciding causal concurrency under the fullest reads‑from style relaxation, shows classic trace/commutativity lets the same decision be done in constant space, and introduces grain equivalence (contiguous and scattered grains) that is strictly coarser than trace equivalence yet admits constant‑space streaming algorithms. Builds a grain graph to encode ordering constraints for scattered grains, gives constant‑space decision procedures (theoretical nondeterminism present), and flags implementation costs driven by number of threads and shared variables.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:11Equivalence relations and soundness
- 2:13Causal concurrency and decision
- 3:16Reads-from equivalence limits
- 4:40Monitoring hardness under reads-from
- 5:23Coarser equivalences for monitoring
- 6:46Grains and commutativity
- 8:33Non-determinism and grain equivalence
- 9:56Context sensitivity in grains
- 11:00Grain graphs and scattered grains
- 13:25Constant-space algorithms challenges
- 14:53Future work and implementation
- 15:59Broader applications and open problems
- 16:21Summary
- 16:45Q&A
related talks
19mScenario-based Proofs for Concurrent Objects
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
25mThe Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Un...
31mTermination in Concurrency, Revisited
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
01h 01mThe Future of Concurrency and Parallelism
54mReasoning about Progress of Concurrent Objects
20mDegrees of Separation: A Flexible Type System for Safe Concurrency