Parameterized Verification of Asynchronous Shared-Memory Systems

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

Authors: Javier Esparza, Pierre Ganty, 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

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

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 (17)

• Title not available (Why is that?)
• Fine-grained complexity of safety verification
• Fine-grained complexity of safety verification
• Complexity of Liveness in Parameterized Systems
• Keeping a crowd safe: on the complexity of parameterized verification (invited talk)
• Reconfiguration and message losses in parameterized broadcast networks
• Title not available (Why is that?)
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Data tracking in parameterized systems
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Liveness in broadcast networks
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• 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
• Verifying the correctness of distributed systems via mergeable parallelism

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)