Disentanglement with Futures, State, and Interaction
summary
Formalizes disentanglement for a language with futures, I/O, and mutable references and proves that purely functional programs are disentangled; extends to stateful programs that are determinacy race free by defining a determinacy race as two concurrent accesses to the same location with at least one write; introduces the join transformation that rewrites completed futures to preserve ancestor allocation sets in action traces; shows a deadlock free corollary and a weaker theorem allowing races on small values (weak determinacy race freedom) so CAS on booleans does not break disentanglement.
AI-written summary · about
chapters (18)
- 0:00Disentanglement with Futures
- 0:23What is disentanglement
- 1:48Futures in interaction
- 2:53Allocation traces in Futures
- 4:39Join transformation impact
- 5:22Disentanglement with IO and state
- 6:05Disentanglement as safety
- 6:45Defining disentanglement over traces
- 8:10Computation trees and contexts
- 8:53Determinacy races
- 10:41Determinacy race example
- 12:05Weak determinacy freedom
- 13:31Disentanglement and deadlock
- 14:34Key theorems summary
- 15:17Q&A: Join transformation
- 15:58Q&A: Synchronization primitives
- 16:39Q&A: Unification variables
- 18:03Q&A: Intermediate states
related talks
30mCONQUERING CONCURRENCY WITH FUNCTIONAL PROGRAMMING
20mDegrees of Separation: A Flexible Type System for Safe Concurrency
26mDegrees of Separation: A Flexible Type System for Data Race Prevention
24mA Concurrent Program Logic with a Future and History
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
25mAll for One and One for All: Program Logics for Exploiting Internal Determinism in(…)
23mA Denotational Approach to Release/Acquire Concurrency
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz