Parameterized Verification of Asynchronous Shared-Memory Systems

DOI10.1145/2842603zbMATH Open1426.68169arXiv1304.1185OpenAlexW1662711380MaRDI QIDQ3177767FDOQ3177767

Pierre Ganty, Javier Esparza, Rupak Majumdar

Publication date: 2 August 2018

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

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.

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)

Cited In (14)

• Title not available (Why is that?)
• Fine-grained complexity of safety verification
• Complexity of Liveness in Parameterized Systems
• Title not available (Why is that?)
• Model checking parameterized asynchronous shared-memory systems
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Liveness in broadcast networks
• Parameterized verification under TSO with data types
• Title not available (Why is that?)
• Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent
• Round-bounded control of parameterized systems
• Title not available (Why is that?)
• Verifying the correctness of distributed systems via mergeable parallelism

   Recommendations

• Model checking parameterized asynchronous shared-memory systems 👍 👎
• Model checking parameterized asynchronous shared-memory systems 👍 👎
• 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 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Synchronizability for Verification of Asynchronously Communicating 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)