2012/07/14 by Salvatore La Torre, P. Madhusudan, Gennaro Parlato · 26 citations
Computer Science · Mathematics · #Algorithm #Artificial intelligence #Assertion #Computer science #Distributed systems and fault tolerance #Formal Methods in Verification #Mathematical optimization #Mathematics #Parallel Computing and Optimization Techniques #Parallel computing #Parameterized complexity #Programming language #Reachability #Salient #Scheduling (production processes) #Theoretical computer science #Thread (computing) #cs.LO #cs.SE
paper · pdf · doi:10.4204/eptcs.87.4
published in Electronic Proceedings in Theoretical Computer Science 87, 34-47 (Open Publishing Association) · In Proceedings FIT 2012, arXiv:1207.3485
openalex publication_date 2012/07/14 · arxiv created 2012/07/18 · arxiv updated 2012/07/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.