Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
DOI10.1007/978-3-031-37706-8_10zbMath1547.68108MaRDI QIDQ6535632
Mihir Vahanwala, Mohamed Faouzi Atig, Unnamed Author, Adwait Godbole, Parosh Aziz Abdulla
Publication date: 1 February 2024
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Runtime analysis of probabilistic programs with unbounded recursion
- The decidability of verification under PS 2.0
- Explaining relaxed memory models with program transformations
- A formal hierarchy of weak memory models
- Model checking with strong fairness
- Recursive Markov Decision Processes and Recursive Stochastic Games
- Taming release-acquire consistency
- Well (and Better) Quasi-Ordered Transition Systems
- Deciding Fast Termination for Probabilistic VASS with Nondeterminism
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Zero-reachability in probabilistic multi-counter automata
- On Thin Air Reads Towards an Event Structures Model of Relaxed Memory
- Source Sets
- On the verification problem for weak memory models
- Relaxed memory models
- Model Checking Probabilistic Pushdown Automata
- A promising semantics for relaxed-memory concurrency
- Mathematizing C++ concurrency
- Decisive Markov Chains
- Tools and Algorithms for the Construction and Analysis of Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Well-structured transition systems everywhere!
- Probabilistic total store ordering
This page was built for publication: Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
