Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)
Abstract: We present -- a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational semantics of PTSO induces an infinite-state Markov chain. We resolve the inherent non-determinism due to process schedulings and memory updates according to given probability distributions. We provide a comprehensive set of results showing the decidability of several properties for PTSO, namely (i) Almost-Sure (Repeated) Reachability: whether a run, starting from a given initial configuration, almost surely visits (resp. almost surely repeatedly visits) a given set of target configurations. (ii) Almost-Never (Repeated) Reachability: whether a run from the initial configuration, almost never visits (resp. almost never repeatedly visits) the target. (iii) Approximate Quantitative (Repeated) Reachability: to approximate, up to an arbitrary degree of precision, the measure of runs that start from the initial configuration and (repeatedly) visit the target. (iv) Expected Average Cost: to approximate, up to an arbitrary degree of precision, the expected average cost of a run from the initial configuration to the target. We derive our results through a nontrivial combination of results from the classical theory of (infinite-state) Markov chains, the theories of decisive and eager Markov chains, specific techniques from combinatorics, as well as, decidability and complexity results for the classical (non-probabilistic) TSO semantics. As far as we know, this is the first work that considers probabilistic verification of programs running on weak memory models.
Recommendations
Cites work
- A load-buffer semantics for total store ordering
- A note on the attractor-property of infinite-state Markov chains
- Analysing decisive stochastic processes
- Deciding fast termination for probabilistic VASS with nondeterminism
- Decisive Markov Chains
- Eager Markov Chains
- Efficient analysis of probabilistic programs with an unbounded counter
- Good lower and upper bounds on binomial coefficients
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- scientific article; zbMATH DE number 3972158 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3240812 (Why is no real title available?)
- scientific article; zbMATH DE number 3249395 (Why is no real title available?)
- Model checking
- Model Checking Probabilistic Pushdown Automata
- On the verification problem for weak memory models
- Recursive Markov decision processes and recursive stochastic games
- Runtime analysis of probabilistic programs with unbounded recursion
- Simulating perfect channels with probabilistic lossy channels
- Stochastic Games with Lossy Channels
- What's decidable about weak memory models?
- Zero-reachability in probabilistic multi-counter automata
Cited in
(6)- An integrated performance model for orderpicking systems with randomized storage
- Deciding Robustness against Total Store Ordering
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
- Concurrent stochastic lossy channel games
- TSO games -- on the decidability of safety games under the total store order semantics
- TSO games -- on the decidability of safety games under the total store order semantics
This page was built for publication: Probabilistic total store ordering
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166793)
