Automatic Synthesis of Distributed Protocols
Automatic Synthesis of Distributed Protocols
复制标题
分布式协议的自动合成
DOI：
10.1145/3061640.3061652
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Tripakis
中科院分区：
文献类型：
--
作者：
R. Alur;S. Tripakis
并发过程之间的协调协议是现代多处理器和分布式系统的重要组成部分。数十年[25，35，13，32]。 ]。传统上，分布式协议被建模为一组有限状态的过程。在反应性合成中，目标是从给定的逻辑要求自动得出一个协议。最近将这些结果转化为实践的一些努力[39，30，8]（有关反应性合成理论的出色调查，请参见[18]，而www.syntcomp.org进行基准和求解器的竞争我们需要分发实现，然后反应性合成是不可月的[40，21]。通过合成器来满足所有正确性要求。不确定，例如，关于角落案例和处理意外消息，该工具会自动填充协议合成问题，然后减少到以下协议完成问题：给定一组有限状态的机器过渡功能，给定环境模型，并给定一组安全性和livesice要求，找到了该过程的FSM的完成，以使组成满意度所有要求。但是，分布式协议的模型检查。对于任何给定的完成，模型检查提供了一种处理方式，而反示例性归纳合成（CEGIS）是一种新技术，是对前者的潜在解决方案[49，3，47]。在两个阶段的迭代调用中：学习者选择了候选人的完成，然后通过验证者对正确性要求进行检查；
Protocols for coordination among concurrent processes are an essential component of modern multiprocessor and distributed systems. The multitude of behaviors arising due to asynchronous concurrency makes the design of such protocols difficult, and consequently analyzing such protocols has been a central theme of research in formal verification for decades [25, 35, 13, 32]. Sustained research in improving verification tools has resulted in powerful heuristics for coping with the computational intractability of problems such as Boolean satisfiability and search through the state-space of concurrent systems [11, 26, 15]. Now that automated verification tools are mature enough to be applied to debugging of real-world protocols [12, 33, 23], the new research frontier is protocol synthesis for simplifying the design process via more intuitive programming abstractions for specifying the desired behavior. Traditionally a distributed protocol is modeled as a set of communicating finite-state processes. The correctness is specified by both safety and liveness requirements. In model checking, a given model of the distributed protocol is checked against its correctness requirements specified in temporal logic. In reactive synthesis, the goal is to automatically derive a protocol from the given logical requirements. The synthesis problem for reactive systems goes back to work in the 1960’s [10], with finite automata on infinite words and trees providing the crucial algorithmic apparatus, with some recent efforts to translate these results into practice [39, 30, 8] (see [18] for an excellent survey of the theory of reactive synthesis, and www.syntcomp.org for benchmarks and a competition of solvers). However, if we require the implementation to be distributed, then reactive synthesis is undecidable [40, 21]. An alternative, and potentially more feasible approach inspired by program sketching [49, 48], is to ask the programmer to specify an incomplete protocol to be completed by the synthesizer so as to satisfy all the correctness requirements. This methodology for protocol specification can be viewed as a fruitful collaboration between the designer and the synthesis tool: the programmer has to describe the structure of the desired protocol, but some details that the programmer is unsure about, for instance, regarding corner cases and handling of unexpected messages, are filled in automatically by the tool. The protocol synthesis problem then reduces to the following protocol completion problem: given a set of finite-state machines for communicating processes with incomplete transition functions, given a model of the environment, and given a set of safety and liveness requirements, find a completion of the FSMs for the processes such that the composition satisfies all the requirements. The computational complexity of this problem is Pspace, the same as that of model checking of distributed protocols. However, now we need to cope with a search with two nested exponentials: the number of possible completions of the incomplete input model is exponential and so is the number of states of the product of all the component processes for any given completion. Advances in model checking offer a way of dealing with the latter, while counterexampleguided inductive synthesis (CEGIS) is a new technology that is a potential solution for the former [49, 3, 47]. The synthesis algorithm then consists of iterative invocations of two phases: the learner chooses a candidate completion, which is then checked with respect to correctness requirements by the verifier ; violations of the requirements are supplied to the learner to prune the search space in subsequent iterations.