A Counter-Example-Driven Approach to the Bounded Synthesis of Synchronization Code for Distributed Algorithms

In this paper, we present an approach to automatically syn- thesize synchronization code for distributed programs assuming a multi- thread shared-variables model of computation, common in object-oriented programming languages like JAVA. Our method combines SAT solving over logical theories written in First-Order Logic with Transitive Closure, and symbolic model checking. Intuitively, our approach starts by using SAT solving to enumerate potential implementations of the (local) pro- cesses, and checking whether their concurrent composition satisfies the required global properties, until a valid synchronization code is obtained. This latter step is performed using symbolic model checking, and the ob- tained counterexamples are used to incrementally refine the SAT-based search for local process implementations. We developed a prototype of our approach and applied it to well-known case studies of distributed algorithms