Probabilistic Total Store Ordering
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait, Godbole, Krishna S

TL;DR
This paper introduces Probabilistic Total Store Ordering (PTSO), extending classical TSO semantics with probabilistic behavior, and provides decidability results for various probabilistic reachability and cost properties in this model.
Contribution
It presents the first probabilistic extension of TSO semantics and establishes decidability results for key verification problems within this framework.
Findings
Decidability of almost-sure and almost-never reachability properties.
Decidability of approximate quantitative reachability measures.
Decidability of expected average cost calculations.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Advanced Software Engineering Methodologies
