Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs

TL;DR

This paper introduces a framework for automatically synthesizing synchronization in shared-memory concurrent programs based on temporal specifications, enhancing correctness and flexibility in concurrent system design.

Contribution

It presents a novel method for the algorithmic synthesis of synchronization that supports various program types and a rich specification language, improving automation and expressiveness.

Findings

Successfully synthesizes synchronization ensuring correct global behavior.

Supports a wide range of program structures and initialization methods.

Enables synthesis at different abstraction levels.

Abstract

We present a framework that takes a concurrent program composed of unsynchronized processes, along with a temporal specification of their global concurrent behaviour, and automatically generates a concurrent program with synchronization ensuring correct global behaviour. Our methodology supports finite-state concurrent programs composed of processes that may have local and shared variables, may be straight-line or branching programs, may be ongoing or terminating, and may have program-initialized or user-initialized variables. The specification language is an extension of propositional Computation Tree Logic (CTL) that enables easy specification of safety and liveness properties over control and data variables. The framework also supports synthesis of synchronization at different levels of abstraction and granularity.