Synthesizing fine-grained synchronization protocols for implicit monitors
summary
A tool called Cortado statically proves safe interleavings by commutativity checks, builds a MaxSAT encoding that assigns locks per code snippet, and instruments monitor code with acquire/release on CFG edges; in a bounded FIFO example it emits two locks plus an atomic counter and preserves atomicity, race- and deadlock-freedom. Evaluation on Java monitors shows Cortado’s synthesized explicit monitors often run faster than both the prior single-global-lock generator (Espresso) and hand-written implementations, so the synthesis both builds and improves real code.
AI-written summary · about
chapters (10)
- 0:00Implicit monitors introduction
- 3:59Explicit vs implicit trade-offs
- 7:05Global locks reduce parallelism
- 10:59Synthesis approach overview
- 11:42Static analysis for safe interleavings
- 16:21MaxSAT encoding for optimal locking
- 22:01Instrumenting code with locks
- 23:02Experimental evaluation
- 25:11Summary and contributions
- 25:38Q&A: Other synchronization
related talks
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
28mAutomated Correctness Analysis for core.async
20mAtomiS: Data-Centric Synchronization Made Practical
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
25mResponsive Parallelism with Synchronization
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
52mSTM and Structured Concurrency — The Battle with Multithreading Dragons
15mSoundness of Predictive Concurrency Analyses