Veracity: Declarative Multicore Programming with Commutativity
summary
A new language, Veracity (implemented in Multicore OCaml), lets programmers mark commute blocks with logical predicates and the compiler either forks them or falls back to sequential execution. Correctness relies on a new scoped serializability criterion enforced via synthesized locks and shorter lock windows when possible. Commute conditions are generated and verified by translating blocks to logical ADT specs and querying SMT-based toolserver2. Implementations include a small in-memory filesystem and a crowdsourced smart contract; benchmarks show measurable speedups as the long computations grow.
AI-written summary · about
chapters (14)
- 0:00Multicore programming challenges
- 1:48Conditional sequential commutativity
- 3:36Commutativity for safe parallelization
- 6:01Formal semantics of commute
- 8:51Parallel execution semantics
- 10:14Limitations of serializability
- 12:44Enforcing serializability with locking
- 14:35Locking techniques
- 16:41Commutativity conditions validity
- 18:05Translating commute to ADTs
- 20:53Handling loops and summaries
- 21:56Synthesizing commutativity conditions
- 22:58Evaluation and benchmarks
- 24:42Summary and future
related talks
58mA New Perspective on Commutativity in Verification
01h 06mVerifying a compiler through equational means
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...- 01h 06mVerifying a compiler through equational means
17mA Formally Verified Foundation for Compositional Heterogeneous Coherence
46mMechanizing Abstract Interpretation
30mCalculating Compilers for Concurrency
23mCorrect Compilation of Concurrent C Code