Simplifying Concurrent Programming via Synchronization Synthesis
summary
Given an implicit-monitor spec using conditional critical regions, the system synthesizes concrete locks and condition-variable operations by reducing signaling choices to discharging Hoare-style triples and encoding locking as a MaxSAT encoding that enforces data-race freedom, atomicity and deadlock-freedom. Implementations Expresso and Cortado run in minutes on benchmarks from Gradle and Spring; Expresso matches handwritten monitors and is on average 1.6× faster than AutoSync, Cortado yields finer-grained locks and often outperforms both Expresso and the original expert code.
AI-written summary · about
chapters (16)
- 0:00Start
- 0:44Automatic Synthesis of Synchronization Protocols
- 2:17Main Models of Concurrency
- 3:32Monitor Programming Abstraction
- 8:49Trade-Offs between these Explicit and Implicit Monitors
- 11:23Synthesizing the Signaling Code
- 18:22Optimal Signaling
- 19:51Recap
- 21:05Synthesis Workflow
- 31:50Evaluation
- 32:43Autosync
- 42:51High Level Approach
- 45:16Static Analysis
- 51:15Hard Constraints
- 52:40Ensure Atomicity
- 55:00Soft Constraints
related talks
31mSynthesizing fine-grained synchronization protocols for implicit monitors
52mSTM and Structured Concurrency — The Battle with Multithreading Dragons
03h 29mConcurrency with Clojure
25mResponsive Parallelism with Synchronization
26mConcurrency: Unlocking a Solution
54mReasoning about Progress of Concurrent Objects
41mEverything You Don’t Want to Know About Concurrency on the JVM
39mLet's talk concurrency