Sequentializing Parameterized Programs

TL;DR

This paper introduces a method to transform parameterized concurrent shared-memory programs into sequential programs that preserve reachability and local invariants under a k-round process schedule, using linear interfaces.

Contribution

It presents a novel sequentialization technique for parameterized programs that maintains assertion-preserving properties without extra counters, based on linear interfaces.

Findings

Sequential programs track only one thread's local variables.

Uses only O(k) copies of shared variables, no counters.

Ensures the sequential program explores only reachable states.

Abstract

We exhibit assertion-preserving (reachability preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Our transformation utilizes linear interfaces to sequentialize the program, and to ensure the sequential program explores only reachable states and preserves local invariants.