Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors (Extended Version)
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, Isil, Dillig

TL;DR
This paper introduces a novel static analysis and MaxSAT-based synthesis method to automatically generate fine-grained explicit synchronization protocols from implicit monitors, enabling better parallelization.
Contribution
It proposes a new static analysis technique and MaxSAT formulation for synthesizing efficient, fine-grained synchronization protocols from implicit monitors, improving parallelism.
Findings
Cortado can synthesize synchronization protocols competitive with expert solutions.
The approach exploits parallelization opportunities in implicit monitors.
Synthesized protocols improve performance on benchmark monitors.
Abstract
A monitor is a widely-used concurrent programming abstraction that encapsulates all shared state between threads. Monitors can be classified as being either implicit or explicit depending on the primitives they provide. Implicit monitors are much easier to program but typically not as efficient. To address this gap, there has been recent research on automatically synthesizing explicit-signal monitors from an implicit specification, but prior work does not exploit all paralellization opportunities due to the use of a single lock for the entire monitor. This paper presents a new technique for synthesizing fine-grained explicit-synchronization protocols from implicit monitors. Our method is based on two key innovations: First, we present a new static analysis for inferring safe interleavings that allow violating mutual exclusion of monitor operations without changing its semantics. Second,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Distributed systems and fault tolerance · Logic, programming, and type systems
