Can we have software tools that automatically generate scalable distributed programs? Such programs should scale to an arbitrary number of nodes while ensuring correctness and resilience.
An article by Dr. Ali Ebnenasir (CS, ICC-SAS), “Verification and Synthesis of Responsive Symmetric Uni-Rings,” explores this research. The article, available for early access, is featured in the journal, IEEE Transactions on Software Engineering.
Abstract: This paper investigates the verification and synthesis of parameterized protocols that satisfy leadsto properties on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic, self-disabling and constant-space processes. First, we show that when R and Q are conjunctive global state predicates, verifying ‘R leadsto Q’ for parameterized protocols on symmetric uni-rings is undecidable. Then, we show that surprisingly synthesizing symmetric uni-ring protocols that satisfy ‘R leadsto Q’ is actually decidable. We identify necessary and sufficient conditions for the decidability of synthesis based on which we design and implement a sound and complete algorithm that takes the predicates R and Q, and automatically generates a parameterized protocol that satisfies ‘R leadsto Q’ for unbounded (but finite) ring sizes. Moreover, we show that verifying leadsto properties remains undecidable even if R and Q are local state predicates! This result would lead to the impossibility of computing a cutoff for local leadsto on symmetric rings of deterministic, self-disabling and constant-space processes. We further show that verifying local and global deadlocks in our formal setting are decidable problems. We also present a cutoff theorem that enables the construction of symmetric rings where deadlocks are reachable.
Citation: A. Ebnenasir, “Verification and Synthesis of Responsive Symmetric Uni-Rings,” in IEEE Transactions on Software Engineering, doi: 10.1109/TSE.2021.3119771.