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 snapshots protocol on fully connected networks and a dining philosophers protocol on hypercubes.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications

  • Ruoxi Zhang,
  • Richard Trefler,
  • Kedar S. Namjoshi

摘要

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 snapshots protocol on fully connected networks and a dining philosophers protocol on hypercubes.