Stateless model checking for TSO and PSO

DOI10.1007/S00236-016-0275-0MaRDI QIDQ1683934zbMATH OpenOpenAlexFDO

Authors Parosh A. Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, K. Sagonas

Publication date 1 December 2017

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00236-016-0275-0

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Stateless model checking for TSO and PSO
• Sound and complete monitoring of sequential consistency for relaxed memory models
• On the verification problem for weak memory models
• Studying Operational Models of Relaxed Concurrency
• Effective Abstractions for Verification under Relaxed Memory Models

Cites work

• scientific article; zbMATH DE number 4030996 (Why is no real title available?)
• Analyses and optimizations for shared address space programs.
• Checking and enforcing robustness against TSO
• Counter-Example Guided Fence Insertion under TSO
• Dynamic partial-order reduction for model checking software
• Effective Program Verification for Relaxed Memory Models
• Myths about the mutual exclusion problem
• Optimal dynamic partial order reduction
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Software verification for weak memory via program transformation
• Sound and complete monitoring of sequential consistency for relaxed memory models
• State space reduction using partial order techniques
• Stateless model checking for TSO and PSO

Cited in

(14)

• A pragmatic approach to stateful partial order reduction
• Operational semantics with semicommutations
• Stateless model checking under a reads-value-from equivalence
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• Stateless model checking for TSO and PSO
• Sound and complete monitoring of sequential consistency for relaxed memory models
• Making Linearizability Compositional for Partially Ordered Executions
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• A load-buffer semantics for total store ordering
• Stateless model checking for TSO and PSO
• Verification of Concurrent Programs on Weak Memory Models
• Optimal stateless model checking for causal consistency
• Reconciling preemption bounding with DPOR
• Reachability of scope-bounded multistack pushdown systems

Describes a project that uses

Uses Software

• veriSoft
• Checkfence

This page was built for publication: Stateless model checking for TSO and PSO

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