一句话：提出从隐式监视器合成细粒度显式同步协议的静态分析与 MaxSAT 方法，生成可媲美专家手写的协议。
监视器是封装线程间共享状态的常用并发抽象。隐式监视器易于编程但效率通常较低；现有从隐式规格自动合成显式 signal 监视器的工作因对整个监视器使用单把锁，未能利用全部并行机会。本文提出为隐式监视器合成细粒度显式同步协议的方法：首先通过新的静态分析推断可在不改变语义的前提下破坏监视器操作互斥的安全交错；随后据此构造 MaxSAT 实例，其模型对应构造即正确的同步协议。作者实现工具 Cortado，并在含并行机会的监视器上评估；结果表明其合成的同步策略可与专家手写策略竞争，甚至更优。
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.
@article{paperbot1531,
title = {Synthesizing fine-grained synchronization protocols for implicit monitors},
author = {Kostas Ferles and Benjamin Sepanski and Rahul Krishnan and James Bornholt and Işil Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527311}
}