Скачать или смотреть [VMCAI'25] Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications

Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications (Video, VMCAI)
Ruoxi Zhang, Richard Trefler, and Kedar Namjoshi
(University of Waterloo; University of Waterloo, Canada; Nokia Bell Labs)

Abstract: Scalable distributed systems are typically parametric in design. The key parameter is the number of isomorphic components, K. A second important parameter is the number of neighbors, k, of each component process. In this work, we describe a methodology that uses an automated synthesis procedure to construct parametric system instances where both K and k can vary arbitrarily, extending prior work on synthesis for a fixed k. The methodology relies crucially on locality, symmetry, and abstraction. The first step is to eliminate K by refining a general, system-wide specification to a local temporal specification for a generic process in its parameterized neighborhood. Next, the local process specification is abstracted to remove its dependence on k. These steps are done by hand. The given synthesis procedure then automatically constructs an abstract process from the abstract local specification with a worst-case cost exponential in the length of the abstract local specification. We show that, for any k, the concretized abstract process meets the local specification. We then show that instantiating the abstract process with different k and K forms system instances that satisfy the system-level specification. The worst-case cost of instantiation is linear in K. We use this method to synthesize an atomic snapshot protocol on fully connected networks and a dining philosophers protocol on hypercubes.


Presentation at the VMCAI conference, January 20-21, 2025, https://popl25.sigplan.org/home/vmcai...
Sponsored by ACM SIGPLAN