SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 11:30 - 12:00 at Lecture Theatre 2 - Synthesis II Chair(s): Loris D'Antoni

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, we use the results of this static analysis to generate a MaxSAT instance whose models correspond to correct-by-construction synchronization protocols. We have implemented our approach in a tool called Cortado and evaluate it on monitors that contain parallelization opportunities. Our evaluation shows that Cortado can synthesize synchronization policies that are competitive with, or even better than, expert-written ones on these benchmarks.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Synthesis IIOOPSLA at Lecture Theatre 2
Chair(s): Loris D'Antoni University of Wisconsin-Madison
10:30
30m
Talk
Neural Architecture Search using Property Guided Synthesis
OOPSLA
Charles Jin Massachusetts Institute of Technology, Phitchaya Mangpo Phothilimthana Google Research, Sudip Roy Cohere.ai
DOI
11:00
30m
Talk
Synthesizing Axiomatizations using Logic Learning
OOPSLA
Paul Krogmeier University of Illinois at Urbana-Champaign, Zhengyao Lin Carnegie Mellon University, Adithya Murali University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
11:30
30m
Research paper
Synthesizing fine-grained synchronization protocols for implicit monitors
OOPSLA
Kostas Ferles Veridise Inc., Benjamin Sepanski The University of Texas at Austin, Rahul Krishnan University of Wisconsin-Madison, James Bornholt University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI