Probabilistic Total Store Ordering

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 $\textit{Probabilistic Total Store Ordering (PTSO)}$ -- 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.