Parameterized Verification of Asynchronous Shared-Memory Systems

DOI10.1145/2842603MaRDI QIDQ3177767zbMATH OpenOpenAlexFDO

Authors Javier Esparza, Pierre Ganty, Rupak Majumdar

Publication date 2 August 2018

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.1185

zbMATH Keywords

decidabilityformal languagesasynchronous shared memoryparameterized systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in case of pushdown-systems, some language-theoretic constructions of independent interest.

Recommendations

• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Practical abstractions for automated verification of shared-memory concurrency
• Convergence Verification: From Shared Memory to Partially Synchronous Systems
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• scientific article; zbMATH DE number 2102714
• scientific article; zbMATH DE number 2087551
• Synchronizability for Verification of Asynchronously Communicating Systems

Cited in

(17)

• Parameterized verification under TSO with data types
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Fine-grained complexity of safety verification
• Fine-grained complexity of safety verification
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• scientific article; zbMATH DE number 7295368 (Why is no real title available?)
• scientific article; zbMATH DE number 911851 (Why is no real title available?)
• Liveness in broadcast networks
• Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent
• Keeping a crowd safe: on the complexity of parameterized verification (invited talk)
• Round-bounded control of parameterized systems
• Data tracking in parameterized systems
• Reconfiguration and message losses in parameterized broadcast networks
• Verifying the correctness of distributed systems via mergeable parallelism
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Complexity of Liveness in Parameterized Systems

This page was built for publication: Parameterized Verification of Asynchronous Shared-Memory Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3177767)