11institutetext: Uppsala University, Sweden 22institutetext: IIT Bombay, India
33institutetext: University of California Berkeley, USA

# Probabilistic Total Store Ordering

Parosh Aziz Abdulla 11 Mohamed Faouzi Atig 11 Raj Aryan Agarwal 22
Adwait Godbole 33 Krishna S 22

###### Abstract

We present 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.

##  1 Introduction

The classical Sequential Consistency (SC) semantics [1] has been a fundamental
assumption in concurrent programming. SC guarantees that process operations
are atomic. A write operation, performed by a given process, is immediately
visible to all the other processes. However, designers of modern computer
systems, in their quest of increased system efficiency, often sacrifice the SC
guarantee. Instead, the processes communicate asynchronously, allowing a delay
in the propagation of write operations. Due to the propagation delay, written
values can become available to processes at different time points, and in an
order that may be different from the order in which they are generated. This
asynchronous behavior gives rise to new semantics, collectively referred to as
weak memory models [2]. In the presence of weak memory models, programs
exhibit new, and often unexpected, behaviors, bringing about complex
challenges in the design and analysis of concurrent systems. Even text-book
programs may behave erroneously. The classical Dekker mutual exclusion
protocol is a case in point. The ubiquity of weak memory models has led to an
extensive research effort for the testing and verification of concurrent
programs running under such semantics.

Existing works on the verification of programs running on weak memory models,
consider safety properties such as state reachability, assertion violation,
and robustness. While safety properties are fundamental, we need also to prove
liveness properties, i.e., to show that the program indeed makes progress.
This is, of course, true already in the case of SC. A program, such as a
mutual exclusion protocol, needs to guarantee that each process will
eventually reach its critical section. The satisfiability of liveness
properties is often dependent on the type of fairness conditions on process
executions that are provided by the underlying platform [3, 4]. The reason is
the presence of concurrency non-determinism, i.e., the inherent non-
determinism in program behavior due to the different possible ways in which
the scheduler can interleave the processes. The scheduler may always neglect a
given process, which means that the process will never make progress (e.g.,
never reaches its critical section). Therefore, we need the scheduler to
follow a fair selection policy that allows each process to advance in its
execution. The situation is even more complicated in the case of weak memory
models, since we also need to deal with a second source of non-determinism,
besides concurrency non-determinism, namely (data) propagation non-
determinism. Since write operations are propagated asynchronously, there is in
general no way to predict if, when, and in which order, write operations
become visible to the processes.

In this paper we present a framework for the verification of liveness
properties for concurrent programs running under the classical Total Store
Ordering (TSO) semantics [5]. The TSO model puts an unbounded store (write)
buffer between each process and the main memory. The buffer carries pending
write operations that have been performed by the process. These operations are
propagated from the buffer to the shared memory in a FIFO manner. When a
process performs a write operation, it appends the operation as a message to
its buffer. When a process reads a variable, it searches its buffer for a
pending write operation on that variable. If such operations exist then it
reads from the most recent one. If no such operation exists, it fetches the
value of the variable from the main memory. The TSO propagation mechanism is a
typical example of how propagation non-determinism arises: the write
operations are propagated to the shared memory non-deterministically, and a
process sees the other processes’ write operations only when the latter are
available in the memory. Therefore, having a scheduler that fairly selects the
processes is not sufficient. We also need to ensure that the write operations
propagate to the processes sufficiently often.

Traditional fairness conditions such as strong or weak fairness [3, 4, 6]
cannot capture propagation policies adequately since they irrationally allow
slow propagation, i.e., they allow write operations to propagate at a lower
rate than the rate by which they are issued. For instance, strong fairness
guarantees that messages are transferred infinitely often from the buffers to
the memory. Still, it does not constrain the relative frequency of write and
update operations, and hence it does not prevent the buffer contents from
growing unboundedly. In such a scenario, more and more un-propagated messages
may be clustered inside the buffers, and a given process may, from some point
on, be confined only to read its own writes, since it will not see the memory
updates by the other processes. Accordingly, verifying liveness properties
subject to strong fairness may wrongly deem the system to be incorrect: even
if a process is selected infinitely often by the scheduler and write
operations are propagated infinitely often to the memory, a given process may
incorrectly be judged not to make progress due to slow propagation.

While slow propagation can arise theoretically under the above mentioned
fairness conditions, it is almost never observed in practice. Existing
platforms implement different policies, such as invalidation or write-back
policies, to flush the buffers at regular intervals [7, 8]. This prevents the
buffer sizes from growing beyond certain sizes, and implicitly ensure
propagation fairness. In fact, this is true to the degree that non-SC
behaviors are (relatively) rarely observed on TSO platforms [9, 10].

In this paper, we perform verification of liveness properties for concurrent
programs under TSO using probabilistic fairness [11]. As far as we know, this
is the first work that considers probabilistic verification of programs
running on weak memory models. In our model, both process scheduling and
message propagation are carried out according to given probability
distributions. We assign a weight (a natural number) to each process. We
resolve concurrency non-determinism probabilistically by letting the scheduler
select the next process to execute with a probability that reflects the weight
of the process compared to the weights of the other processes that are enabled
in the same configuration. After each process step, we allow an update step,
in which the buffers transfer parts of their contents to the memory. We make
the probability distribution equal among all possible update operations in the
given configuration111Our framework allows several other types of probability
distributions (see Sec. 9.). As we will see later in the paper, defining the
model in this way implies that we assign low probabilities to program runs
that unboundedly increase the number of messages inside the buffers.
Accordingly, our model is more faithful to real program behavior compared to
models induced by non-probabilistic fairness conditions.

We perform a comprehensive analysis of the decidability of verifying liveness
properties for concurrent programs running under the TSO semantics, subject to
probabilistic fairness. In fact, verifying programs running on the TSO memory
model, even with respect to safety properties, poses a difficult challenge.
The unboundedness of the buffers implies that the state space of the system is
infinite, even in the case where the input program is finite-state [12, 13].
Similarly, the operational semantics of our model gives rise to Markov chains
with infinite state spaces. Furthermore, in general, liveness properties give
rise to more difficult problems than safety properties, since the former are
interpreted over infinite program executions while the latter are interpreted
over finite executions. Our results rely on nontrivial combinations of results
from the classical theory of (infinite-state) Markov chains [14, 15], the
theories of decisive and eager Markov chains [16, 17], specific techniques
from combinatorics [18], as well as, decidability and complexity results for
the classical (non-probabilistic) TSO semantics [19, 13]. Concretely, we show
the decidability of the following problems, each of which is defined by giving
an initial configuration $\gamma_{\it init}$ and a set ${\tt Target}$ of
process target states.

Qualitative Analysis (Sec. 6). In qualitative reasoning, we are interested in
knowing whether the given property is satisfied with probability $1$ (almost
surely satisfied), or with probability $0$ (almost never satisfied). We show
that the satisfiability of these properties can be reduced to similar problems
on the underlying (non-probabilistic) transition systems for classical TSO.
The actual probabilities appearing in the induced Markov chains then are
inconsequential and only their non-zeroness matters. This is useful whenever
the probabilities have not been measured exactly, or the portion of the system
giving rise to probabilistic behavior has not been designed yet. We consider
the following different flavors of qualitative analysis: Almost-Sure
(Repeated) Reachability222While repeated reachability is a liveness property,
plain reachability in the non-probabilistic case is a safety property.
However, in the presence of probabilities, plain reachability measures the
probability of convergence towards a target state, and hence it can be
considered a form of liveness property. In any case, this is a matter of
definition and has no bearing on the rest of the paper.: whether a run of the
system from $\gamma_{\it init}$ will almost surely visit (resp. repeatedly
visit) ${\tt Target}$; Almost-Never (Repeated) Reachability: whether a run of
the system from $\gamma_{\it init}$ will almost never visit (resp. repeatedly
visit) ${\tt Target}$. Furthermore, we show that all these problems have non-
primitive-recursive complexities.

Quantitative Analysis (Sec. 7). The task is to estimate to an arbitrary degree
of precision the probability by which a run from $\gamma_{\it init}$
(repeatedly) visits ${\tt Target}$, rather than only checking whether the
probability is equal to one or zero.

Expected Average Cost (Sec. 8). We study the expected cost for runs that start
from $\gamma_{\it init}$ until they reach ${\tt Target}$. To that end, we
extend our model by providing a cost function that assigns a fixed cost to
each instruction in the language. Calculating expected costs of runs has many
potential applications. For instance, one might be interested in the mean-time
of reaching a target, i.e., the average number of steps before reaching the
target [20]. In the context of weak memory models, in general, and TSO in
particular, one can perform a more refined analysis by also taking into
account the fact that specific instructions, e.g., memory fences, have higher
costs [21]. Incorporating instruction costs in the model makes average cost
analysis reflect more faithfully the efficiency of the program compared to an
instruction count based metric. There have been several approaches towards
optimizing fence implementations in hardware [22, 23, 24] which exploit the
fact that non-SC behaviours are rare even in unfenced code. A quantitative
analysis of the prevalence of behaviours and cost of executing instructions
can help determine the efficacy of such implementations.

The supplementary material contains detailed proofs of all the lemmas and
theorems.

##  2 Preliminaries

In this section, we introduce notation, recall basics of transition systems,
Temporal logic and Markov chains.

##### Basic Notation

The size of a set $A$ is denoted by $\left|{A}\right|$. We use ${A}^{*}$ and
${A}^{\omega}$ to denote the set of finite resp. infinite words over (a
possibly infinite set) $A$, and let $\epsilon$ be the empty word. For
$w\in{A}^{*}$, $\left|{w}\right|$ denotes the length of $w$
($\left|{w}\right|=\infty$ if $w$ is infinite). For $i:1\leq
i\leq\left|{w}\right|$, we use $w[i]$ to denote the $i^{th}$ element of $w$.
We define ${\tt head}\left({w}\right):=w[1]$ and ${\tt
tail}\left({w}\right):=w[2]\cdots w[\left|{w}\right|]$. We use $a\in w$ to
denote that $w[i]=a$ for some $i:1\leq i\leq\left|{w}\right|$. For words
$w_{1}\in{A}^{*}$ and $w_{2}\in({A}^{*}\cup{A}^{\omega})$, we use
$w_{1}\boldsymbol{\cdot}w_{2}$ to denote their concatenation. For
$k\in\mathbb{N}$, we define
${A}^{k}:=\left\\{w\in{A}^{*}~{}|~{}\;{\left|{w}\right|=k}\right\\}$, i.e., it
is the set of words over $A$ of length $k$.

##### Transition Systems

A transition system is a pair
$\left\langle\Gamma,\stackrel{{\scriptstyle}}{{\rightarrow}}\right\rangle$
where $\Gamma$ is a (potentially) infinite set of configurations, and
$\stackrel{{\scriptstyle}}{{\rightarrow}}\subseteq\Gamma\times\Gamma$ is the
transition relation. We write
$\gamma\stackrel{{\scriptstyle}}{{\rightarrow}}{}\gamma^{\prime}$ to denote
that
$\left\langle\gamma,\gamma^{\prime}\right\rangle\in\stackrel{{\scriptstyle}}{{\rightarrow}}$,
and use $\stackrel{{\scriptstyle*}}{{\rightarrow}}$ to be the reflexive
transitive closure of $\rightarrow_{\mbox{\tiny${}$}}{}$. For
$k\in\mathbb{N}$, we write $\gamma\stackrel{{\scriptstyle
k}}{{\rightarrow}}\gamma^{\prime}$ to denote that there is a sequence
$\gamma_{0}\stackrel{{\scriptstyle}}{{\rightarrow}}\gamma_{1}\stackrel{{\scriptstyle}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle}}{{\rightarrow}}\gamma_{k}$
where $\gamma_{0}=\gamma$ and $\gamma_{k}=\gamma^{\prime}$, i.e., there is a
sequence of $k$ transition steps leading from $\gamma$ to $\gamma^{\prime}$.
For $\sim\in\left\\{<,\leq,=\right\\}$, we write
$\gamma\stackrel{{\scriptstyle\sim k}}{{\rightarrow}}\gamma^{\prime}$ to
denote that $\gamma\stackrel{{\scriptstyle m}}{{\rightarrow}}\gamma^{\prime}$
for some $m:0\leq m\sim k$.

##### Temporal Logic

A run $\rho$ of transition system
${\mathcal{T}}=\left\langle\Gamma,\stackrel{{\scriptstyle}}{{\rightarrow}}\right\rangle$
is an infinite word $\gamma_{0}\gamma_{1}\ldots$ of configurations such that
$\gamma_{i}\stackrel{{\scriptstyle}}{{\rightarrow}}\gamma_{i+1}$ for $i\geq
0$. We use $\rho[i]$ to denote $\gamma_{i}$. We say that $\rho$ is a
$\gamma$-run if $\rho[0]=\gamma$. We use ${\tt Runs}\left(\gamma\right)$ to
denote the set of $\gamma$-runs. A path $\pi$ is a finite prefix of a run, and
a $\gamma$-path is a finite prefix of a $\gamma$-run. We use the standard
notation $\gamma\models_{{\mathcal{T}}}\phi$ to represent that $\gamma$
satisfies the $\mathit{CTL}^{*}$ state formula $\phi$ and
$\rho\models_{{\mathcal{T}}}\phi$ to mean that $\rho$ satisfies the path333We
term infinite sequences as runs and finite sequences as paths. However,
traditionally, $\mathit{CTL}^{*}$ refers to properties of infinite-sequences
(our runs) as _path_ -formulae. formula $\phi$. We refer the reader to [25]
for details of CTL.

For $\gamma\in\Gamma$ and $G\subseteq\Gamma$, we say that $G$ is reachable
from $\gamma$, denoted $\gamma\models_{{\mathcal{T}}}\exists\Diamond G$, if
there is a $\gamma$-run $\rho$ such that $\rho[i]\in G$ for some $i$. For
$k\in\mathbb{N}$, $\gamma\in\Gamma$, and $G\subseteq\Gamma$,
$\rho\models_{{\mathcal{T}}}\Diamond^{\\!\\!k}G$ says that $\rho$ reaches $G$
first at the $k^{\it th}$ step. For
$\sim~{}\in\left\\{<,\leq,=,\geq,>\right\\}$,
$\rho\models_{{\mathcal{T}}}\Diamond^{\\!\\!\sim k}G$ says that
$\rho\models_{{\mathcal{T}}}\Diamond^{\\!\\!m}G$ holds for some $m:0\leq m\sim
k$. The statement $\rho\models_{{\mathcal{T}}}\bigcirc^{\\!k}G$ says that
$\rho$ visits $G$ at the $k^{\it th}$ step (but possibly earlier).

##### Markov Chains

A Markov chain ${\mathcal{C}}$ is a pair
$\left\langle\Gamma,{\texttt{M}}\right\rangle$ where $\Gamma$ is a
(potentially infinite) set of configurations, and
${{\texttt{M}}}\\!:{\Gamma\times\Gamma}\rightarrow{[0,1]}$ is a transition
probability matrix over $\Gamma$, called the probability matrix of
${\mathcal{C}}$, i.e. M satisfies: $\forall a\in A.\sum_{b\in
A}{\texttt{M}}\left(a,b\right)=1$. A Markov chain
${\mathcal{C}}=\left\langle\Gamma,{\texttt{M}}\right\rangle$ induces an
underlying transition system, denoted ${{\mathcal{C}}}^{\downarrow}$. We
define
${{\mathcal{C}}}^{\downarrow}:=\left\langle\Gamma,\stackrel{{\scriptstyle}}{{\rightarrow}}\right\rangle$,
where
$\stackrel{{\scriptstyle}}{{\rightarrow}}:=\left\\{\left\langle\gamma,\gamma^{\prime}\right\rangle~{}|~{}\;{{\texttt{M}}\left(\gamma,\gamma^{\prime}\right)>0}\right\\}$.
The underlying transition system has the same configuration set, with
transitions between configurations that have non-zero transition probability
under ${\mathcal{C}}$. This allows us to lift the temporal logic concepts
defined above to Markov chains.

##### Probability Measures

Consider a Markov chain
${\mathcal{C}}=\left\langle\Gamma,{\texttt{M}}\right\rangle$. The probability
of taking path $\pi$ is the product of single step probabilities along $\pi$:

${\it
Prob}_{{\mathcal{C}}}\left(\pi\right):=\prod_{i=0,...,\left|{\pi}\right|-1}{\texttt{M}}\left(\pi[i],\pi[i+1]\right)$

For a configuration $\gamma$, we adopt the usual probability space on
$\gamma$-runs with the $\sigma$-algebra over cylindrical sets starting from
$\gamma$ (see [26, 20] for details). For path formula $\phi$, we define ${\it
Prob}_{{\mathcal{C}}}\left(\gamma\models\phi\right)={\it
Prob}_{{\mathcal{C}}}\left(\\{\rho\in{\tt
Runs}\left(\gamma\right)~{}|~{}\rho\models_{{\mathcal{C}}}\phi\\}\right)$
(which is measurable by [27]), e.g. given a set $F\subseteq G$, ${\it
Prob}_{{\mathcal{C}}}\left(\gamma\models\Diamond F\right)$ is the measure of
$\gamma$-runs which reach $F$. If ${\it
Prob}_{{\mathcal{C}}}\left(\gamma\models\phi\right)=1$ the we say that almost
all $\gamma$-runs of ${\mathcal{C}}$ satisfy $\phi$. Following the literature,
we say that $\gamma\models_{{\mathcal{C}}}\phi$ holds almost surely (almost
certainly), or that $\phi$ holds almost surely from $\gamma$.

##  3 Concurrent Programs

A (concurrent) program consists of a set of processes that run in parallel and
communicate through a set of shared variables. The operation of the program is
controlled by a central scheduler that selects the processes to execute one
after the other. We assume a finite set ${\sf Procs}$ of processes that share
a set ${\mathcal{X}}$ of variables. Fig. 1 gives the grammar for a small but
general assembly-like language that we use for defining the syntax of
concurrent programs. A program instance, ${\mathcal{P}}$ is described by a set
of shared variables, var∗, followed by the codes of the processes, (proc reg∗
instr∗)∗. Each process $p\in{\sf Procs}$ has a finite set ${\sf Regs}_{p}$ of
(local) registers. We assume that the sets of registers of the different
processes are disjoint, and define ${\sf Regs}_{{\mathcal{P}}}:=\cup_{p\in{\sf
Procs}}{\sf Regs}_{p}$.

⬇

prog ::= var∗(proc reg∗ instr∗)∗

instr ::= lbl : stmt

stmt ::= | var:=reg

| reg:=var

| reg:=expr

| reg:=CAS(var,reg,reg)

| if reg then lbl

| term

Figure 1: A simple programming language.

Each process declares its set of registers, reg∗, followed by a sequence of
instructions. We assume that the data domain of ${\mathcal{X}}$ and ${\sf
Regs}_{{\mathcal{P}}}$ is a finite set ${\mathcal{V}}$, with a special element
$0\in{\mathcal{V}}$.

##### Instructions

An instruction $\mathsf{i}$ is of the form ${\mathsf{l}}:{\mathsf{s}}$ where
$\mathsf{l}$ is a unique (across processes) label and $\mathsf{s}$ is a
statement. Labels represent program counters of processes and indicate the
instruction that the process executes the next time it is scheduled. A
read/write statement either writes the value of a register to a shared
variable, reads the value of a shared variable into a register, or updates the
value of a register by evaluating an expression. We assume a set expr of
expressions over constants and registers, but not referring to the shared
variables. The CAS statement is the standard compare-and-swap operation, and
if-statements have their usual interpretations. Iterative constructs such as
while and for, as well as goto-statements, can be encoded with branching if-
statements as usual.

The fence statement, that flushes the contents of the buffer of the process,
can be simulated using the CAS statement. The statement term will cause the
process to terminate its execution. Sometimes, we will refer to an instruction
by its statement, e.g. the instruction r:=x, (where r is a register and x is a
shared variable) a read instruction, similarly for a write instruction, etc.
Semantics of these instructions are explained through a set of inference rules
in Sec. 4.

##### Labels

We define $\mathsf{Lbl}_{p}$ to be the set of labels that occur in the code of
the process $p$, and define $\mathsf{Lbl}_{{\mathcal{P}}}:=\cup_{p\in{\sf
Procs}}\mathsf{Lbl}_{p}$. We assume that term has the label
${\mathsf{l}^{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}}}}_{p}$.
We define $\mathsf{Instr}_{p}$ to be the set of instructions occurring in $p$,
and define $\mathsf{Instr}_{{\mathcal{P}}}:=\cup_{p\in{\sf
Procs}}\mathsf{Instr}_{p}$. For instruction $\mathsf{i}$ of the form
${\mathsf{l}}:{\mathsf{s}}$ we define
$\lambda\left(\mathsf{i}\right):=\mathsf{l}$ and ${\tt
stmt}\left(\mathsf{i}\right):=\mathsf{s}$. Abusing notation, we also define
${\tt stmt}\left(\mathsf{l}\right):=\mathsf{s}$. For a process $p\in{\sf
Procs}$ instruction $\mathsf{i}\in\mathsf{Instr}_{p}$, with ${{\tt
stmt}\left(\mathsf{i}\right)\neq\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}}$,
we define ${\tt next}\left(\mathsf{i}\right)$ to be the (unique) instruction
next to $\mathsf{i}$ in the code of $p$. For an instruction
${\mathsf{l}_{1}}:{({\tt if}\;{\tt a}\;{\tt then}\;\mathsf{l}_{2})}$, we
assume, without loss of generality444We make the restriction for technical
convenience. The case where $\mathsf{l}_{1}=\mathsf{l}_{2}$ do not introduce
conceptual difficulties. However, it simplifies the presentation by
eliminating some corner cases when we define probability measures (Sec. 5) and
when we introduce our cost model (Sec. 8)., that
$\mathsf{l}_{1}\neq\mathsf{l}_{2}$.

##### Scheduler

The scheduler selects the process from ${\sf Procs}$ to run next. The
operational model for classical TSO [28] uses a non-deterministic scheduler.
We adopt a scheduler that selects the next process probabilistically. The
scheduler policy is defined by a function ${\tt Sched}$: ${\tt
Sched}\left(p\right)\in\mathbb{N}$ denotes the scheduling weight assigned to
to the process $p$. If $p$ is enabled (i.e. the process can execute the next
instruction, formally defined in Sec. 4) then $p$ is scheduled at the next
step with a probability that is proportional to ${\tt Sched}\left(p\right)$.

##  4 Operational Semantics

The operational model for classical TSO [28] describes the semantics as a
transition system. We also take an operational approach. However, we differ in
a fundamental aspect: classical TSO models choice between transitions as non-
deterministic choice. We on the other hand, model this as probabilistic
choice, to get a system called as Probabilistic TSO (PTSO for short). Adding
probabilities induces a Markov chain, which governs the behaviours of PTSO.

A program is described by a pair: the set of processes, ${\sf Procs}$ and the
scheduler policy ${\tt Sched}$. In this section, we fix such a program
${\mathcal{P}}=\left\langle{\sf Procs},{\tt Sched}\right\rangle$. We develop
the operational semantics of ${\mathcal{P}}$ under PTSO as an infinite-state
Markov chain $\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}:=\left\langle\Gamma_{{\mathcal{P}}},{\texttt{M}}_{{\mathcal{P}}}\right\rangle$.
We begin by defining the set of configurations $\Gamma_{{\mathcal{P}}}$ (Sec.
4.1). Then we describe the behavior of ${\mathcal{P}}$ under classical TSO
using a transition system $\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ (Sec.
4.2); Finally, we extend the transition system to a Markov chain
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ by giving probability
distributions that define govern process scheduling, and memory updates.

###  4.1 Configurations

The central feature of TSO is the store buffer: a FIFO buffer in which pending
write operations are queued as messages. The semantics equips each process
$p\in{\sf Procs}$ with an unbounded buffer, here called the $p$-buffer, that
carries pending write operations issued by $p$, but that have yet not reached
the shared memory.

A configuration,
$\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$,
describes four attributes: a labeling state ($\lambda$), a register state
(${\mathcal{R}}$), a buffer state (${\mathcal{B}}$), and a memory state
(${\mathcal{M}}$). We use $\Gamma_{{\mathcal{P}}}$ to denote the set of
configurations of ${\mathcal{P}}$.

A labeling state is a function ${\lambda}\\!:{{\sf
Procs}}\rightarrow{\mathsf{Lbl}_{{\mathcal{P}}}}$ that defines, for $p\in{\sf
Procs}$, the label $\lambda\left(p\right)\in\mathsf{Lbl}_{p}$ of the next
instruction to be executed by $p$.

A register state is a function ${{\mathcal{R}}}\\!:{{\sf
Regs}_{{\mathcal{P}}}}\rightarrow{{\mathcal{V}}}$ that maps each register
${\tt a}\in{\sf Regs}_{{\mathcal{P}}}$, to its current value
${\mathcal{R}}({\tt a})\in{\mathcal{V}}$. For an expression $e$, we use
${\mathcal{R}}(e)$ to denote the evaluation of $e$ against the register state
${\mathcal{R}}$.

A single-buffer state $w$ is a word in
${({\mathcal{X}}\times{\mathcal{V}})}^{*}$, describing the content of the
$p$-buffer for some process $p\in{\sf Procs}$. The buffer contains a sequence
of pending write messages, i.e. pairs of form
$\left\langle\mathsf{x},\varv\right\rangle$ representing a write to
$\mathsf{x}$, with value $\varv$. A buffer state is a function
${{\mathcal{B}}}\\!:{{\sf
Procs}}\rightarrow{{({\mathcal{X}}\times{\mathcal{V}})}^{*}}$ that defines,
for each process $p\in{\sf Procs}$, a single-buffer state describing the
content of the $p$-buffer.

A memory state is a function
${{\mathcal{M}}}\\!:{{\mathcal{X}}}\rightarrow{{\mathcal{V}}}$ that assigns to
each variable $\mathsf{x}\in{\mathcal{X}}$ its current value
${\mathcal{M}}\left(\mathsf{x}\right)\in{\mathcal{V}}$ in the shared memory.

${{\begin{array}[]{c}\begin{array}[]{ccc}\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{write}}}\\\
\inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=(\mathsf{x}:={\tt
a})\\\ \\\
{\mathcal{B}}^{\prime}={{\mathcal{B}}}\left[p\leftarrow\left\langle\mathsf{x},{\mathcal{R}}({\tt
a})\right\rangle\boldsymbol{\cdot}{\mathcal{B}}\left(p\right)\right]\\\ \\\
\lambda^{\prime}={\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}},{\mathcal{B}}^{\prime},{\mathcal{M}}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{read}}}\\\
\inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt
a}:=\mathsf{x})\\\ \\\ {\tt
FetchVal}\left(\mathsf{x}\right)\left({\mathcal{B}}\left(p\right)\right)\left({\mathcal{M}}\left(\mathsf{x}\right)\right)=\varv\\\
{\mathcal{R}}^{\prime}={{\mathcal{R}}}\left[{\tt a}\leftarrow\varv\right]\\\
\\\ \lambda^{\prime}={\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{expr}}}\\\
\inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt a}:=e)\\\ \\\
{\mathcal{R}}^{\prime}={{\mathcal{R}}}\left[{\tt
a}\leftarrow{\mathcal{R}}(e)\right]\\\ \\\
\lambda^{\prime}={\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}\end{array}\\\\[28.45274pt]
\begin{array}[]{cc}\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{CAS-
true}}}\\\ \inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt
b}:=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}CAS}}}}}}\left(\mathsf{x},{\tt
a}_{1},{\tt a}_{2}\right))\\\
{\mathcal{M}}\left(\mathsf{x}\right)={\mathcal{R}}({\tt a}_{1})\\\ \\\
{\mathcal{R}}^{\prime}={{\mathcal{R}}}\left[{\tt b}\leftarrow{\tt
true}\right]\\\ {\mathcal{B}}\left(p\right)=\epsilon\\\
{\mathcal{M}}^{\prime}={{\mathcal{M}}}\left[\mathsf{x}\leftarrow{\mathcal{R}}({\tt
a}_{2})\right]\\\ \\\ \lambda^{\prime}={\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}},{\mathcal{M}}^{\prime}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{CAS-
false}}}\\\ \inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt
b}:=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}CAS}}}}}}\left(\mathsf{x},{\tt
a}_{1},{\tt a}_{2}\right))\\\
{\mathcal{M}}\left(\mathsf{x}\right)\neq{\mathcal{R}}({\tt a}_{1})\\\ \\\
{\mathcal{R}}^{\prime}={{\mathcal{R}}}\left[{\tt b}\leftarrow{\tt
false}\right]\\\ {\mathcal{B}}\left(p\right)=\epsilon\\\ \\\
\lambda^{\prime}={\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}\end{array}\\\\[28.45274pt]
\begin{array}[]{cccc}\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{if-
true}}}\\\ \inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt
if}\;{\tt a}\;{\tt then}\;\mathsf{l})\\\ \\\ {\mathcal{R}}({\tt a})={\tt
true}\\\ \\\
\lambda^{\prime}={\lambda}\left[p\leftarrow\mathsf{l}\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{if-
false}}}\\\ \inferrule{{\tt stmt}\left(\lambda\left(p\right)\right)=({\tt
if}\;{\tt a}\;{\tt then}\;\mathsf{l})\\\ \\\ {\mathcal{R}}({\tt a})={\tt
false}\\\ \\\ {\lambda}\left[p\leftarrow{\tt
next}\left(\lambda\left(p\right)\right)\right]}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{proc}}}\\\
\inferrule{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{disabled}}}\\\
\inferrule{\gamma\text{ is disabled}}{\gamma\xrightarrow{}_{{\tt
proc}}\gamma}\end{array}\end{array}\\\\[28.45274pt]
\begin{array}[]{ccc}\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{empty-
update}}}\\\
\inferrule{~{}}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{\epsilon}_{{\tt
update}}\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{single-
update}}}\\\
\inferrule{{\mathcal{B}}^{\prime}\left(p\right)=w\boldsymbol{\cdot}\left\langle\mathsf{x},\varv\right\rangle\\\
{\mathcal{B}}^{\prime\prime}={{\mathcal{B}}^{\prime}}\left[p\leftarrow
w\right]\\\ \\\
{\mathcal{M}}^{\prime\prime}={{\mathcal{M}}^{\prime}}\left[\mathsf{x}\leftarrow\varv\right]\\\
\\\
\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{\alpha}_{{\tt
update}}\left\langle\lambda,{\mathcal{R}},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{p\boldsymbol{\cdot}\alpha}_{{\tt
update}}\left\langle\lambda,{\mathcal{R}},{\mathcal{B}}^{\prime\prime},{\mathcal{M}}^{\prime\prime}\right\rangle}\end{array}&\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{update}}}\\\
\inferrule{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{\alpha}_{{\tt
update}}\left\langle\lambda,{\mathcal{R}},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{}_{{\tt
update}}\left\langle\lambda,{\mathcal{R}},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle}\end{array}\end{array}\\\\[28.45274pt]
\begin{array}[]{c}{\color[rgb]{0.890625,0.140625,0.109375}\definecolor[named]{pgfstrokecolor}{rgb}{0.890625,0.140625,0.109375}\texttt{{Full-
TSO}}}\\\
\inferrule{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{}_{{\tt
proc}}\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle\\\
\left\langle\lambda^{\prime},{\mathcal{R}}^{\prime},{\mathcal{B}}^{\prime},{\mathcal{M}}^{\prime}\right\rangle\xrightarrow{}_{{\tt
update}}\left\langle\lambda^{\prime\prime},{\mathcal{R}}^{\prime\prime},{\mathcal{B}}^{\prime\prime},{\mathcal{M}}^{\prime\prime}\right\rangle}{\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle\xrightarrow{}_{{\mathcal{P}}}\left\langle\lambda^{\prime\prime},{\mathcal{R}}^{\prime\prime},{\mathcal{B}}^{\prime\prime},{\mathcal{M}}^{\prime\prime}\right\rangle}\end{array}\end{array}$

Figure 2: The classical TSO semantics: process transitions (green), update
transitions (orange) and overall transition (Full-TSO)

.

Consider a configuration
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$.
We say that $\gamma$ is plain if ${\mathcal{B}}\left(p\right)=\epsilon$ for
all $p\in{\sf Procs}$, i.e., all the buffers in $\gamma$ are empty. We use
$\Gamma^{\tt plain}_{{\mathcal{P}}}$ to denote the set of plain configurations
of ${\mathcal{P}}$. Notice that $\Gamma^{\tt
plain}_{{\mathcal{P}}}\subseteq\Gamma_{{\mathcal{P}}}$ and that $\Gamma^{\tt
plain}_{{\mathcal{P}}}$ is finite. For a label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$, we write $\mathsf{l}\in\gamma$ if
$\lambda\left(p\right)=\mathsf{l}$ for some $p\in{\sf Procs}$. We define
$\Gamma^{\mathsf{l}}_{{\mathcal{P}}}:=\left\\{\gamma\in\Gamma_{{\mathcal{P}}}~{}|~{}\;{\mathsf{l}\in\gamma}\right\\}$,
i.e., configurations in which $\mathsf{l}$ occurs.

For a configuration
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$
we define the size of $\gamma$ by $\left|{\gamma}\right|:=\sum_{p\in{\sf
Procs}}\left|{{\mathcal{B}}\left(p\right)}\right|$, i.e., it is the total
number of messages in the buffers in $\gamma$. For
$\sim\in\left\\{<,\leq,=,\geq,>\right\\}$, we define
$\Gamma_{{\mathcal{P}}}^{\sim\ell}:=\left\\{\gamma\in\Gamma_{{\mathcal{P}}}~{}|~{}\;{\left|{\gamma}\right|{\sim\ell}}\right\\}$.
, i.e. configurations where the total number of messages, $m$, relates to
$\ell$ by $m\sim\ell$.

###  4.2 The Classical TSO Semantics

We recall the classical semantics of TSO, using a transition system
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt
TS}=\left\langle\Gamma_{{\mathcal{P}}},\xrightarrow{}_{{\mathcal{P}}}\right\rangle$.
We define the transition relation $\xrightarrow{}_{{\mathcal{P}}}$ through the
set of inference rules in Fig. 2. The relation
$\xrightarrow{}_{{\mathcal{P}}}$ is the composition of two relations: the
relation $\xrightarrow{}_{{\tt proc}}$ describes the processes’ execution
steps, and the relation $\xrightarrow{}_{{\tt update}}$ describes memory
updates, where pending writes are propagated to the memory.

####  4.2.1 Process Transitions

We define the process transition relation $\xrightarrow{}_{{\tt
proc}}:=\cup_{p\in{\sf Procs}}\xrightarrow{p}_{{\tt proc}}$ as a union of
relations each corresponding to one process (the rule proc). The inference
rules defining $\xrightarrow{p}_{{\tt proc}}$, for a process $p\in{\sf Procs}$
are depicted in Fig.2. Each rule corresponds to one step performed by $p$.
After executing an instruction, $p$ will move on to the next instruction in
its code. It executes the latter instruction when again selected by the
scheduler.

A write instruction ($\mathsf{x}:={\tt a}$) assigns the value of the local
register ${\tt a}$ to the shared variable $\mathsf{x}$. The process appends a
write message consisting of $\mathsf{x}$ together with the value
${\mathcal{R}}({\tt a})$ of ${\tt a}$, to the head of the $p$-buffer. A read
instruction, (${\tt a}:=\mathsf{x}$), assigns the value of the shared variable
$\mathsf{x}$ to the local register ${\tt a}$. The value of $\mathsf{x}$ is
either fetched from the $p$-buffer (read-own-write), or from the shared memory
(read-from-memory). We capture both cases in one inference rule, using the
function ${\tt FetchVal}$ defined as follows. Let $w$ be the contents of the
$p$-buffer. We write $\mathsf{x}\in w$ if
$\left\langle\mathsf{x},\varv\right\rangle\in w$ for some
$\varv\in{\mathcal{V}}$, and write $\mathsf{x}\not\in w$ otherwise. We define
(i) ${\tt
FetchVal}\left(\mathsf{x}\right)\left(w\right)\left({\mathcal{M}}\right):=\varv$
if $\mathsf{x}\in w$ and
$w=w_{1}\boldsymbol{\cdot}\left\langle\mathsf{x},\varv\right\rangle\boldsymbol{\cdot}w_{2}$
with $\mathsf{x}\not\in w_{1}$; and (ii) define ${\tt
FetchVal}\left(\mathsf{x}\right)\left(w\right)\left({\mathcal{M}}\right):={\mathcal{M}}\left(\mathsf{x}\right)$
if $\mathsf{x}\not\in w$. In case (i), the value of $\mathsf{x}$ is taken from
the latest $\mathsf{x}$-message from the $p$-buffer. In case (ii), no
$\mathsf{x}$-messages exist in the $p$-buffer, and the value is read from the
shared memory.

The instruction ${{\tt
b}:=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}CAS}}}}}}\left(\mathsf{x},{\tt
a}_{1},{\tt a}_{2}\right)$ checks whether the $p$-buffer is empty and the
value of the shared variable $\mathsf{x}$ is equal to the value of the
register ${\tt a}_{1}$. If yes, we assign atomically the value of the register
${\tt a}_{2}$ to $\mathsf{x}$, and assign the value ${\tt true}$ to ${\tt b}$
(the rule CAS-true). If the value of $\mathsf{x}$ is different from the value
of ${\tt a}_{1}$ then we do not change the value of $\mathsf{x}$, but assign
the value ${\tt false}$ to ${\tt b}$ (the rule CAS-false). If the $p$-buffer
is not empty then $p$ is disabled in the current configuration. We define the
set of disabled processes at configuration $\gamma$:

${{\small{\sf disab}\left(\gamma\right):=\left\\{p~{}~{}|~{}\;{({\tt
stmt}\left(p\right)=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}})\lor(({\tt
stmt}\left(p\right)=(b:=\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}CAS}}}}}}\left(\mathsf{x},{\tt
a}_{1},{\tt
a}_{2}\right)))\land({\mathcal{B}}\left(p\right)\neq\epsilon))}\right\\}$

In other words, it is the set of processes that are disabled in $\gamma$
either because they have terminated or because they are about to perform a CAS
operation and their buffers are not empty. We say that $p$ is disabled in
$\gamma$ if $p\in{\sf disab}\left(\gamma\right)$, and that $\gamma$ is
disabled if all the processes are disabled in $\gamma$. If a process (resp.
configuration) is not disabled then it is enabled. If $\gamma$ is disabled, we
make a dummy transition that does not change $\gamma$ (the rule
disabled)555The latter transition is not strictly needed, but it is included
for technical convenience.. Notice that if $\gamma\xrightarrow{p}_{{\tt
proc}}\gamma^{\prime}$ then there is unique process $p\in{\sf Procs}$ such
that $\gamma\xrightarrow{p}_{{\tt proc}}\gamma^{\prime}$.

####  4.2.2 Update Transitions

Between two process transitions, the system may perform a (possibly empty)
sequence of update steps. The rule empty-update describes an empty update
step. Each single-update step pops one write message at the end of the
$p$-buffer for some process $p$ and uses it to update the memory. The update
rule captures the effect of a sequence of such single-update steps. We define
the update transition relation $\xrightarrow{}_{{\tt
update}}:=\cup_{\alpha\in{{\sf Procs}}^{*}}\xrightarrow{\alpha}_{{\tt
update}}$ as a union of relations each corresponding to a given sequence of
update steps. The word $\alpha$ gives the sequence of processes that perform
the updates. The net effect is that the system (i) pops a sequence of (
possibly empty) suffixes from the buffer of each process, (ii) shuffles these
into one sequence, and (iii) uses the resulting sequence to update the memory.
Notice that each selection of possible suffixes in step (i) may result in
several different sequences due to multiple interleavings in step (ii).
Observe that $\xrightarrow{}_{{\mathcal{P}}}$ is deadlock-free, i.e., for each
configuration $\gamma\in\Gamma$, there is at least one configuration
$\gamma^{\prime}\in\Gamma$ such that
$\gamma\xrightarrow{}_{{\mathcal{P}}}\gamma^{\prime}$.

###  4.3 Adding Probabilities: PTSO

We define the Markov Chain $\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}=\left\langle\Gamma_{{\mathcal{P}}},{\texttt{M}}_{{\mathcal{P}}}\right\rangle$.
The set $\Gamma_{{\mathcal{P}}}$ of configurations is defined as above. The
probability matrix ${\tt M}_{{\mathcal{P}}}$ is defined as the composition of
two probability distributions: (i) the process probability distribution ${\tt
M}_{\tt proc}$ (ii) the update probability distribution ${\tt M}_{\tt update}$
which add probabilities to the process transition relation
$\xrightarrow{}_{{\tt proc}}$, and the update transition relation
$\xrightarrow{}_{{\tt update}}$ respectively.

####  4.3.1 The Process Probability Distribution: the Scheduler

At each program step ($\xrightarrow{}_{{\mathcal{P}}}$), a process is selected
for execution according to a probability given by the scheduler. In a
configuration $\gamma$, the scheduler selects an enabled process $p\in{\sf
enab}\left(\gamma\right)$ with a probability that reflects the relative weight
of $p$ compared to those of the other enabled processes, ${\tt
Rweight}\left(\gamma\right)\left(p\right)$:

${\tt Rweight}\left(\gamma\right)\left(p\right)=\begin{cases*}0&if $p\in{\sf
disab}\left(\gamma\right)$\\\ \frac{{\tt
Sched}\left(p\right)}{\sum_{p^{\prime}\in{\sf enab}\left(\gamma\right)}{\tt
Sched}\left(p^{\prime}\right)}&if $p\in{\sf
enab}\left(\gamma\right)$\end{cases*}$ (1)

This gives the probability that $p$ to execute in the next step from $\gamma$.
For configurations $\gamma$ and $\gamma^{\prime}$, with
$\gamma\xrightarrow{p}_{{\tt proc}}\gamma^{\prime}$, we define ${\tt M}_{\tt
proc}\left(\gamma,\gamma^{\prime}\right):={\tt
Rweight}\left(\gamma\right)\left(p\right)$. In other words, we move from
$\gamma$ to $\gamma^{\prime}$ with a probability that is given by the relative
weight of $p$ in $\gamma$. We define ${\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right):=0$ if
$\gamma\not{\xrightarrow{}_{{\tt proc}}}\gamma^{\prime}$. To account for the
case where all the processes are disabled in $\gamma$, we define ${\tt M}_{\tt
proc}\left(\gamma,\gamma\right):=1$ if $\gamma$ is disabled.

##### Faithfulness

Our model uses a scheduling policy that assigns a fixed scheduling weight,
${\tt Sched}\left(p\right)$, to each process $p$ in the system. This is a case
of memoryless scheduling, i.e., the probability distribution over processes
does not depend on the execution history. However, we can relax this
constraint to allow for any scheduling policy that satisfies the faithfulness
condition:

$\forall p\in{\sf Procs}~{}~{}{\tt
Rweight}\left(\gamma\right)\left(p\right)=0\iff p\in{\sf
disab}\left(\gamma\right)$

In words, at each step, each enabled process should be scheduled with non-zero
probability. A scheduler that assigns scheduling weights such that the above
condition holds is said to be a faithful scheduler.

##### Schedulers with memory

The above criterion allows for schedulers that are more refined as compared to
the memoryless scheduler. As an example, on implementations of TSO, processes
are often scheduled for multiple consecutive steps since unnecessary context
switching wastes processor resources. To reflect this detail, we can consider
a scheduler that assigns a higher probability to the previously scheduled
process, $p_{\textit{prv}}$. For some choice of constant weights, ${\tt
Sched}$, we can define a new choice of weights ${\tt Sched}^{\prime}$ where
$\lambda>1$ is some parameter.

${\tt Sched}^{\prime}(p)={\tt Sched}\left(p\right)~{}~{}\text{ if }~{}~{}p\neq
p_{\textit{prv}}~{}~{}\text{ and }~{}~{}\lambda\cdot{\tt
Sched}\left(p\right)~{}~{}\text{otherwise}$

In this case, $p_{prv}$ is re-scheduled with a weight which is larger by a
factor of $\lambda$. A larger $\lambda$ implies a stronger tendency to re-
schedule a process. This scheduling policy still satisfies faithfulness. One
can extend this by formulating more intricate policies, e.g. ones that account
for $k$ previous steps.

To better illustrate the concerns and challenges of verification, we continue
to adopt the simple (memoryless) scheduler proposed earlier. However, we
emphasize that our results extend to faithful schedulers.

The Update Probability Distribution: the Memory update policy Between the
process steps, pending messages from the store buffers are propagated to the
shared memory (the update transition). The details of this write propagation
are implementation-specific, with policies tuned towards system performance.
Classical TSO models this update propagation non-deterministically. We, on the
other hand, consider a probabilistic update policy. In a similar manner to the
scheduling probabilities, the update probability distribution defines the
probability by which a configuration $\gamma$ reaches another configuration
$\gamma^{\prime}$ through an update step ($\xrightarrow{}_{{\tt update}}$).
Recall that an update step consists of a sequence of (single) update
operations. The number of possible update sequences from $\gamma$ is finite
since the sizes of each buffer is finite. In our model, we assume that the
update distribution is the uniform distrbution over all possible update
sequences. We note that starting from $\gamma$, different update sequences can
lead to the same configuration $\gamma^{\prime}$. The reason is that different
shufflings of the selected suffixes (see Sec. 4.2.2) may lead to the same
memory state. To reflect this, for configurations $\gamma$ and
$\gamma^{\prime}$, we define ${\tt M}_{\tt
update}\left(\gamma,\gamma^{\prime}\right):=\frac{\left|{\left\\{\alpha~{}|~{}\;{\gamma\xrightarrow{\alpha}_{{\tt
update}}\gamma^{\prime}}\right\\}}\right|}{\left|{\left\\{\alpha~{}|~{}\;{\exists\gamma^{\prime\prime}.\;\gamma\xrightarrow{\alpha}_{{\tt
update}}\gamma^{\prime\prime}}\right\\}}\right|}$, i.e. the fraction of update
sequences that lead to the configuration $\gamma^{\prime}$.

##### Left-Biasedness

Though we adopt a specific update distribution, we provide a generic condition
on that update policy that is sufficient for our results to hold. We call this
the left-biasedness property. Here we provide an intuitive description of
left-biasedness and defer the formal definition to Sec. 8.

Intuitively, left-biasedness requires that for sufficiently large
configurations, the probability that the configuration size reduces in a
single $\xrightarrow{}_{{\mathcal{P}}}$ step is strictly greater than $p$ for
some $p>\frac{1}{2}$. Left-biasedness allows a wide class of more refined
scheduling policies, e.g., where no message propagation is performed when the
number of messages is smaller than a certain value, or where only the messages
inside the buffers of some (probabilistically selected) processes are
propagated.

Though our results apply more generally to models characterized by
faithfulness (scheduler policy), and left-biasedness (update policy), we
continue to adopt the fixed-weight (memoryless) scheduler and uniform update
policy for reasons described above.

The Full Probability Distribution. We combine the process and update
probability distributions, to derive the probability matrix
${\texttt{M}}_{{\mathcal{P}}}$, and thus obtain the Markov chain
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$. Consider configurations
$\gamma$ and $\gamma^{\prime}$ where
$\gamma\xrightarrow{}_{{\mathcal{P}}}\gamma^{\prime}$. Let
$\gamma^{\prime\prime}$ be the unique configuration such that
$\gamma\xrightarrow{}_{{\tt proc}}\gamma^{\prime\prime}\xrightarrow{}_{{\tt
update}}\gamma^{\prime}$. Then, we define ${\tt
M}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right):={\tt M}_{\tt
proc}\left(\gamma,\gamma^{\prime\prime}\right)\cdot{\tt M}_{\tt
update}\left(\gamma^{\prime\prime},\gamma^{\prime}\right)$.

###### Lemma 1

${\tt M}_{{\mathcal{P}}}$ is a prob. distribution on $\Gamma_{{\mathcal{P}}}$;
hence, $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is a Markov chain.

##  5 PTSO: Concepts and Properties

Now, we intuit some concepts underlying Probabilistic TSO and its properties.

PTSO Refines Classical TSO. After introducing
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ and
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ in Sec. 4, we s.t. they are
closely related; $\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ is the
underlying transition system of $\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}$.

###### Lemma 2

${\left(\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}\right)}^{\downarrow}=\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ for any
program ${\mathcal{P}}$.

In particular, this means that the PTSO system
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is a refinement of
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$: a behaviour is observed in
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$ iff it is seen in
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ with non-zero probability.
Whenever the context is clear, we write ${\mathcal{P}}$ instead of
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$,
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$.

Label Reachability. We formulate our verification problems in terms of
reachability to instruction labels. To simplify the notation, we identify a
label $\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$ with the set
$\Gamma^{\mathsf{l}}_{{\mathcal{P}}}$ of configurations in which $\mathsf{l}$
occurs. We say that “$\mathsf{l}$ is reachable” rather than
“$\Gamma^{\mathsf{l}}_{{\mathcal{P}}}$ is reachable”, and write
$\Diamond\mathsf{l}$ instead of
$\Diamond\left\\{\gamma\in\Gamma_{{\mathcal{P}}}~{}|~{}\;{\mathsf{l}\in\gamma}\right\\}$.
In [13, 12] the authors show that label reachability from a plain
configuration is decidable. The following lemma, generalizes this to the case
where the source configuration need not be plain and destination can be a
particular plain configuration.

###### Lemma 3

For a program ${\mathcal{P}}$, a configuration
$\gamma\in\Gamma_{{\mathcal{P}}}$, and a plain configuration
$\gamma^{\prime}\in\Gamma^{\tt plain}_{{\mathcal{P}}}$, it is decidable
whether $\gamma\xrightarrow{*}_{{\mathcal{P}}}\gamma^{\prime}$.

Extending this, we have Lemma 4: we can query whether
$\gamma\xrightarrow{*}_{{\mathcal{P}}}\gamma^{\prime}$ for each
$\gamma^{\prime}\in\Gamma^{\mathsf{l}}_{{\mathcal{P}}}\cup\Gamma^{\tt
plain}_{{\mathcal{P}}}$. Decidability of Lemma 4 follows since $\Gamma^{\tt
plain}_{{\mathcal{P}}}$ is finite and the subroutine is decidable by Lemma 3.

###### Lemma 4

For a program ${\mathcal{P}}$, a configuration
$\gamma\in\Gamma_{{\mathcal{P}}}$, and a label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$, it is decidable whether
$\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$.

###  5.1 Left-Orientedness and Attractors

We show that the set of plain configurations $\Gamma^{\tt
plain}_{{\mathcal{P}}}$ set has an attractor property in the sense of [16]. In
our setting, this means that any run of
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ almost surely visits
$\Gamma^{\tt plain}_{{\mathcal{P}}}$ infinitely often.

##### Small and large configurations

To arrive at this result, we consider a generalization of plain
configurations, called small configurations, denoted $\Gamma^{\tt
small}_{{\mathcal{P}}}$. $\Gamma^{\tt small}_{{\mathcal{P}}}$ consists of
configurations with a small number of messages inside their buffers.
Concretely, a configuration $\gamma$ is small if $\left|{\gamma}\right|\leq
4$, i.e., the total number of messages inside the buffers does not exceed $4$.
666This value is an artifact of the probabilistic policies we have adopted in
Sec. 4 We define the set of large configurations by $\Gamma^{\tt
large}_{{\mathcal{P}}}:=\Gamma_{{\mathcal{P}}}-\Gamma^{\tt
small}_{{\mathcal{P}}}=\Gamma_{{\mathcal{P}}}^{\geq 5}$. We show that the
Markov chain $\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ is left-oriented
in the sense of [29]. That is, for any large configuration
$\gamma\in\Gamma^{\tt large}_{{\mathcal{P}}}$, the expected change in
configuration size for a single $\xrightarrow{}_{{\mathcal{P}}}$ step is
negative.

##### An illustrative example

⬇ 2: x = 2 3: a = x 4: goto 2
---

We explain the update probability distribution through the code snippet on the
right. To begin with let us only consider the process on the left (procL). It
executes an infinite loop, writing 1 to variable x. Let us consider the
evolution of the buffer-sizes of procL, i.e. the number of (x,1) messages in
the procL-buffer. Assume that on reaching label 0, procL has $6$ messages in
its buffer. The $\xrightarrow{}_{{\mathcal{P}}}$ step consists of a process
transition, $\xrightarrow{}_{{\tt proc}}$ followed by an update transition,
$\xrightarrow{}_{{\tt update}}$. In the $\xrightarrow{}_{{\tt proc}}$ step,
the write increases the size of the buffer by one, thus obtaining a buffer of
size 7. Following this the $\xrightarrow{}_{{\tt update}}$ step may push any
number of messages to the memory. Since the update policy chooses uniformly
amongst possible update sequences, the resulting configuration has one amongst
$\\{0,\dots,7\\}$ messages in the procL-buffer, each occurring with an equal
probability of $1/8$. The next $\xrightarrow{}_{{\tt proc}}$ step (a goto),
does not change the buffer size, but the $\xrightarrow{}_{{\tt update}}$ step
can still propagate messages. The reasoning for the next steps follows
similarly.

##### Comparison with other notions of fairness

At each $\xrightarrow{}_{{\tt proc}}$ step atmost one message is added to the
process buffers (when the process performs a write), however in the following
$\xrightarrow{}_{{\tt update}}$ can still remove large number of messages.
Hence, from sufficient large configuration sizes, the system has a tendency to
move towards configurations with smaller buffer sizes. Formally, we prove the
following lemma, using the left-orientedness property mentioned earlier.

###### Lemma 5

${\it Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\tt
plain}_{{\mathcal{P}}}\right)=1$ for all configurations
$\gamma\in\Gamma_{{\mathcal{P}}}$.

For the above example, PTSO guarantees that the process on the right (procR)
eventually reads value 1 into register a. This follows since in a plain
configuration, the buffer of procR is empty and hence it can read the value
from the memory - this happens almost surely. We highlight that other notions
of fairness such as strong fairness in process scheduling (discussed in [30])
as well memory fairness [31], cannot provide this guarantee. In particular,
memory fairness from [31], would consider the execution which exactly
alternates writes of both processes but procR reads before its own write is
pushed memory to be fair and hence permissible.

x = 1 x = 2 a = x // 2 x = 1 x = 2 a = x // 2 x = 1 $\cdots$

##### B-Plain Configurations

We can refine our analysis of the attraction property enjoyed by the set
$\Gamma^{\tt plain}_{{\mathcal{P}}}$ of plain configurations. We consider a
subset of $\Gamma^{\tt plain}_{{\mathcal{P}}}$ which we call the set of bottom
plain configurations, (or B-plain configurations, for short), denoted
$\Gamma^{\tt Bplain}_{{\mathcal{P}}}$. Intuitively, a B-plain configuration is
a member of a bottom strongly connected component in the graph of plain
configurations. Formally, a configuration $\gamma\in\Gamma_{{\mathcal{P}}}$ is
said to be B-plain if (i) $\gamma\in\Gamma^{\tt plain}_{{\mathcal{P}}}$, and
(ii) for any $\gamma^{\prime}\in\Gamma^{\tt plain}_{{\mathcal{P}}}$, if
$\gamma\xrightarrow{*}_{{\mathcal{P}}}\gamma^{\prime}$ then
$\gamma^{\prime}\xrightarrow{*}_{{\mathcal{P}}}\gamma$. Since any run of the
system almost surely visits the set of $\Gamma^{\tt plain}_{{\mathcal{P}}}$
infinitely often, it will also almost surely visit a B-plain configuration
infinitely often.

###### Lemma 6

${\it Prob}_{{\mathcal{P}}}\left(\gamma\models\Box\Diamond\Gamma^{\tt
Bplain}_{{\mathcal{P}}}\right)=1$ for all configurations
$\gamma\in\Gamma_{{\mathcal{P}}}$.

##  6 Qualitative (Repeated) Reachability

Given: a program ${\mathcal{P}}$, a configuration $\gamma_{\it
init}\in\Gamma_{{\mathcal{P}}}$, a label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$ Qual_Reach: Determine whether
${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)=1$ Qual_Rep_Reach: Determine whether
${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)=1$

In this section, we perform qualitative reachability analysis for PTSO. Given
a program ${\mathcal{P}}$, configuration $\gamma_{\it init}$, and label
$\mathsf{l}$, we check whether a $\gamma_{\it init}$-run almost surely reaches
$\mathsf{l}$. We also consider qualitative repeated reachability, where, we
ask whether a $\gamma_{\it init}$-run repeatedly visits $\mathsf{l}$ (visits
$\mathsf{l}$ infinitely often) w.p. 1. We also consider almost-never variants
of the problems, where we check whether the probabilities are $0$ rather than
$1$. We prove that these problems are decidable, and have non-primitive-
recursive complexities.

###  6.1 Almost-Sure Reachability

The qualitative reachability problem, Qual_Reach, is defined above. The
algorithm in Figure 3 solves Qual_Reach by analyzing the transition system
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt TS}$, the underlying transition
system of PTSO. If $\mathsf{l}$ occurs in $\gamma_{\it init}$ then the
property trivially holds, and hence we answer positively. Otherwise, the
algorithm considers a new program ${\mathcal{P}}^{\prime}$ obtained by
replacing the statement labeled $\mathsf{l}$, by a new statement that makes
${\mathcal{P}}^{\prime}$ terminate immediately if $\mathsf{l}$ is reached. Let
$p\in{\sf Procs}$ be the unique process such that
$\mathsf{l}\in\mathsf{Lbl}_{p}$. We define
${\mathcal{P}}\ominus\mathsf{l}:=\left\langle{\sf
Procs}-\left\\{p\right\\}\cup\left\\{p^{\prime}\right\\},{\tt
Sched}\right\rangle$ where $p^{\prime}$ is a fresh process derived from $p$ by
replacing ${\tt stmt}\left(\mathsf{l}\right)$ by
${{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}goto}}}}}}~{}\mathsf{l}^{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}}}}_{new}$
for a fresh label
${{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}goto}}}}}}~{}\mathsf{l}^{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}}}}_{new}\not\in\mathsf{Lbl}_{{\mathcal{P}}}$
and adding a term at label
${\mathsf{l}^{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}term}}}}}}}}_{new}$.
The remaining instructions of $p^{\prime}$ are identical to $p$.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration; $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label.

1 if  _$\mathsf{l}\in\gamma_{\it init}$_ then return _${\tt true}$_ ;

2 ${\mathcal{P}}^{\prime}:={\mathcal{P}}\ominus\mathsf{l}$;

3 for  _each $\gamma\in\Gamma^{\tt plain}_{{\mathcal{P}}}$_ do

4 if  _$\gamma_{\it init}\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\gamma$ and
$\neg\left(\gamma\xrightarrow{*}_{{\mathcal{P}}^{\prime}}\mathsf{l}\right)$_
then return _${\tt false}$_ ;

5

return _${\tt true}$_

Algorithm 1 Qual_Reach

Figure 3: Almost-sure reachability algorithm.

The loop on line 3 cycles through the (finite) set of plain configurations.
For each plain configuration $\gamma$ from the original program
${\mathcal{P}}$, we check: (i) Whether $\gamma$ is reachable from the initial
configuration $\gamma_{\it init}$ in ${\mathcal{P}}^{\prime}$. By the
construction of ${\mathcal{P}}^{\prime}$, this is equivalent to checking
whether $\gamma$ is reachable from $\gamma_{\it init}$ in ${\mathcal{P}}$
without observing label $\mathsf{l}$. (ii) Whether it can reach the label
$\mathsf{l}$. If the answer to (i) is yes, and the answer to (ii) is no, then
we have found a finite path $\pi$ in ${\mathcal{P}}$ that starting from
$\gamma_{\it init}$, without visiting $\mathsf{l}$, reaches configuration
$\gamma$ from which $\mathsf{l}$ is not reachable. This implies that ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)<1$. If none of the plain configurations
satisfy the condition, then each plain configuration $\gamma$ reachable from
$\gamma_{\it init}$ has a path to $\mathsf{l}$. Now by the attractor lemma,
any run will almost surely visit $\Gamma^{\tt plain}_{{\mathcal{P}}}$
infinitely often and by the fairness property of Markov chains, it almost
surely visits $\mathsf{l}$.

###  6.2 Almost-Sure Repeated Reachability

For almost-sure repeated reachability we are interested in determining whether
the $\gamma_{\it init}$-runs visit $\mathsf{l}$ infinitely often with
probability 1. The algorithm for this is similar to the case for almost-sure
reachability: we check whether $\exists$ a plain configuration $\gamma$ that
satisfies $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\gamma\land\neg\left(\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}\right)$,
in which case we return false. The difference is that we do not need to
transform the program as in the case of almost-sure reachability. Details are
in the supplementary material.

###  6.3 Almost-Never (Repeated) Reachability

Given: a program ${\mathcal{P}}$, a configuration $\gamma_{\it
init}\in\Gamma_{{\mathcal{P}}}$, a label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$ Never_Qual_Reach: Determine
whether ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)=0$ Never_Qual_Rep_Reach: Determine
whether ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)=0$

The almost-never variants of the (repeated) reachability problems,
Never_Qual_Reach resp. Never_Qual_Rep_Reach, ask whether the probabilities
equal to $0$ rather than $1$. The solution to Never_Qual_Reach is
straightforward, since ${\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)=0$ iff $\neg(\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l})$. On the other hand, the
Never_Qual_Rep_Reach problem requires a search over B-plain configurations
$\gamma$ satisfying $\gamma_{\it
init}\xrightarrow{*}_{{\mathcal{P}}}\gamma\xrightarrow{*}_{{\mathcal{P}}}\mathsf{l}$.
Due to space constraints, we defer the algorithm and proofs to the appendix.

###  6.4 Decidability and Complexity

The algorithms can be effectively implemented since (i) $\Gamma^{\tt
plain}_{{\mathcal{P}}}$ is finite; and (ii) the conditions of the for-loops
and if-statements can be checked effectively, as implied by Lemma 4. This
gives Theorem 1. Theorem 2 is proved through reductions from the reachability
problem under the classical (non-probabilistic) TSO semantics [19]. The non-
primitive-recursive lower bounds follow from the corresponding result for
reachability of classical TSO.

###### Theorem 1

Qual_Reach, Qual_Rep_Reach, Never_Qual_Reach, Never_Qual_Rep_Reach are all
decidable.

###### Theorem 2

Qual_Reach, Qual_Rep_Reach, Never_Qual_Reach, Never_Qual_Rep_Reach all have
non-primitive-recursive complexities.

##  7 Quantitative (Repeated) Reachability

In this section we discuss quantitative reachability problems for PTSO. In
contrast to qualitative analysis from Sec. 6, the task here is to compute the
actual probability. We are not able to compute the probabilities exactly, but
we can approximate the probability with an arbitrary degree of precision.

###  7.1 Approximate Quantitative Reachability

Given: program ${\mathcal{P}}$, configuration $\gamma_{\it
init}\in\Gamma_{{\mathcal{P}}}$, label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$, precision value
$\epsilon\in\mathbb{R}^{+}$ Quant_Reach: Determine $\theta$ s.t. ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\in[\theta,\theta+\varepsilon]$
Quant_Rep_Reach: Determine $\theta$ s.t. ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Box\Diamond\mathsf{l}\right)\in[\theta,\theta+\varepsilon]$

In the approximate quantitative reachability problem, Quant_Reach, given a
precision parameter $\varepsilon$, we are interested in determining an
approximation $\theta$ satisfying $\theta\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)\leq\theta+\varepsilon$.

The algorithm in Fig. 4 solves the problem by successively improving the
approximation at each iteration until we are within $\varepsilon$-precision of
the exact value. The algorithm maintains two variables:
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ (positive approximation) is an under-approximation of the
probability with which $\mathsf{l}$ is reachable from $\gamma_{\it init}$, and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ (negative approximation) is an under-approximation of the
probability with which $\mathsf{l}$ is not reachable from $\gamma_{\it init}$.
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ serves as a lower bound on $\theta$, while,
$1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ serves as an upper bound:
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}\leq\theta\leq
1-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration; $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label;
$\varepsilon\in\mathbb{R}^{>0}$: precision.

1 Var

2
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}\in\mathbb{R}$: approximations,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}\in{(\Gamma_{{\mathcal{P}}}\times\mathbb{R})}^{*}$: queue

3

4${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}:=0$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}:=0$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:=\left\langle\gamma_{\it init},1\right\rangle$

5 while
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx} <1-\varepsilon$_ do

6 $\left\langle\gamma,\phi\right\rangle:={\tt
head}\left({{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}}\right)$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:={\tt
tail}\left({{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}}\right)$

7 if  _$\mathsf{l}\in\gamma$_ then
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}+\phi$

8 else if
_$\neg(\gamma\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\mathsf{l})$_
then
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}+\phi$

9 else

10 for  _each $\gamma^{\prime}$ with
$\gamma\rightarrow_{\mbox{\tiny${{\mathcal{P}}}$}}\gamma^{\prime}$_ do
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}\boldsymbol{\cdot}\left\langle\gamma^{\prime},\phi\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right\rangle$

11

return
_${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$_

Algorithm 2 Quant_Reach

Figure 4: The quantitative reachability algorithm.

The algorithm iteratively improves these approximations until we reach a point
where their sum is within $\varepsilon$ from 1 (line 4). In such a case, the
desired value of
$\theta={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ is an $\varepsilon$-precise approximation.

To calculate the approximations, the algorithm performs forward reachability
analysis starting from the initial configuration $\gamma_{\it init}$. It
generates the set of $\gamma_{\it init}$-paths in a breadth-first manner,
using the
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ FIFO queue. For each generated path $\pi$ it also calculates the
probability of $\pi$. Instead of the whole path $\pi$,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ only stores the last configuration, $\gamma$, of $\pi$ and the
probability of $\pi$, $\phi$, as a pair $\langle\gamma,\phi\rangle$.

The approximation variables are initialized (line 3) to zero, and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ queue is initialized to contain a single pair, $\langle\gamma_{\it
init},1\rangle$, representing the initial configuration $\gamma_{\it init}$
(which occurs with probability one). The while-loop executes until we achieve
the desired precision. At each iteration, we check whether we already have
reached the desired precision. If not, the algorithm pops the pair
$\left\langle\gamma,\phi\right\rangle$ from the
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$-queue. There are three possibilities depending on $\gamma$:

  1. 1.

If $\mathsf{l}\in\gamma$ (if-branch, line 6), the current path reaches
$\mathsf{l}$ and, consequently, we increment
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ by $\phi$, the weight of the current path.

  2. 2.

If $\mathsf{l}$ is not reachable from $\gamma$ (else-if branch, line 7), the
measure of runs that reach $\mathsf{l}$ starting from $\gamma$ is zero, and
hence we increment
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ by $\phi$.

  3. 3.

If neither of the above hold (line 10), the current path needs to be explored
further, we enqueue all successors $\gamma^{\prime}$ of $\gamma$ into the
queue. The probability of the new path to $\gamma^{\prime}$ is
$\phi\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)$.

To show correctness of the algorithm, let
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ represent the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ prior to performing the $i^{\it th}$ iteration. We show that in the
limit as $i\rightarrow\infty$, the value of
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ tends to $1$. Technically this follows by Lemma 5. By this
lemma, any $\gamma_{\it init}$-run almost surely either (i) reaches a plain
configuration from which $\mathsf{l}$ is not reachable, or (ii) repeatedly
reaches a plain configuration from which $\mathsf{l}$ is reachable. In case
(ii) it will almost surely reach $\mathsf{l}$. This implies that ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models(\Diamond(\mathsf{l}\vee\neg\exists\Diamond\mathsf{l}))\right)=1$,
i.e., an $\gamma_{\it init}$-run will almost surely either reach $\mathsf{l}$
or reach a configuration from which $\mathsf{l}$ is not reachable, implying
that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ tends to $1$. Finally, by Lemma 4 we can effectively check
the condition of the if-statement, and hence the algorithm terminates.

The correctness of the approximation on termination follows by the property
that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ are under-approximations of the reach and non-reach
probabilities. This follows from the following invariants:

$\displaystyle{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\mathsf{l}\right)$
$\displaystyle\qquad{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}\leq{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\forall\Box\neg\mathsf{l}\right)$ $\displaystyle{\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it init}\models\Diamond\mathsf{l}\right)$
$\displaystyle\leq 1-{\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond\forall\Box\neg\mathsf{l}\right)$
$\displaystyle{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}^{(i)}}$ $\displaystyle>1-\varepsilon\text{ holds on termination}$

These imply that, on termination,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ is within $\varepsilon$-precision of $\theta$.

###### Theorem 3

Quant_Reach is solvable.

###  7.2 Approximate Quantitative Repeated Reachability

In the case of the approximate quantitative repeated reachability problem, we
are interested in approximating the probability of visiting a given label
$\mathsf{l}$ infinitely often. We develop an algorithm that uses an iterative
approximation scheme similar to the reachability case. We defer full details
of this algorithm to the supplementary material and instead give an intuitive
explanation on how it differs from Sec.7.1.

This algorithm too maintains approximations
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
NegApprx}$ and iteratively narrows the error margin until it is smaller than
$\varepsilon$. The main difference is in the condition at line 6 of Figure 4.
In the case of reachability the lower estimate
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
PosApprx}$, is increased when $\mathsf{l}\in\gamma$. In the repeated
reachability case, this is not sufficient; we need to ensure that there is no
state $\gamma^{\prime}$ that is reachable from the current state $\gamma$ and
such that $\mathsf{l}$ is not reachable from $\gamma^{\prime}$. The existence
of such a $\gamma^{\prime}$ implies existence of a non-zero measure
continuation of the current run in which $\mathsf{l}$ is not reached
infinitely often. Hence, the conditional of the if-statement is modified to:
$\forall\gamma^{\prime}\in{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}.~{}~{}(\gamma\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\gamma^{\prime})\Rightarrow(\gamma^{\prime}\stackrel{{\scriptstyle*}}{{\rightarrow}}_{\mbox{\tiny${{\mathcal{P}}}$}}\mathsf{l})$.

We note that naively we would have to check the above condition for all
configurations $\gamma^{\prime}\in\Gamma_{{\mathcal{P}}}$, which is infeasible
since $\Gamma_{{\mathcal{P}}}$ is an infinite set. We address this by using
Lem. 6, which shows that runs from all configurations eventually reach a
B-plain configuration. Hence it is sufficent to only check the condition for
the (finitely many) B-plain configurations, which are precomputed in
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
BPlain}$.

###### Theorem 4

Quant_Rep_Reach is solvable.

##  8 Expected Average Costs

In this section, we develop a cost model for concurrent programs where we
assign a cost to the execution of each instruction, the goal begin to
approximate the expected cost of runs that reach a given label.

###  8.1 Computing costs over runs

A cost function ${{\tt
Cost}}\\!:{\mathsf{Lbl}_{{\mathcal{P}}}}\rightarrow{\mathbb{N}^{>0}}$ for
program ${\mathcal{P}}$ defines for each label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$ the cost of executing the
instruction at $\mathsf{l}$. A particular way to define the function is to
assign a cost to each instruction in the programming language, so that ${\tt
Cost}\left(\mathsf{l}\right)$ depends only on ${\tt
stmt}\left(\mathsf{l}\right)$ and not on $\mathsf{l}$ itself. But we consider
the general case. We extend ${\tt Cost}$ to runs as follows. Consider
configurations
$\gamma=\left\langle\lambda,{\mathcal{R}},{\mathcal{B}},{\mathcal{M}}\right\rangle$
and $\gamma^{\prime}$ such that
$\gamma\xrightarrow{}_{{\mathcal{P}}}\gamma^{\prime}$. If
$\gamma\xrightarrow{p}_{{\mathcal{P}}}\gamma^{\prime}$, for process $p$, then
we define ${\tt Cost}\left(\gamma,\gamma^{\prime}\right):={\tt
Cost}\left(\lambda\left(p\right)\right)$. In other words, it is the cost of
the instruction executed by $p$. Recall from Sec. 4 that $p$ is unique and
therefore the function is well-defined. If ${\sf disab}\left(\gamma\right)$ or
if $\neg(\gamma\xrightarrow{}_{{\mathcal{P}}}\gamma^{\prime})$ then we define
${\tt Cost}\left(\gamma,\gamma^{\prime}\right):=0$. Consider a run
$\rho\in\\{{\tt
Runs}\left(\gamma\right)~{}|~{}\rho\models_{{\mathcal{P}}}\Diamond^{\\!\\!=i}\mathsf{l}\\}$,
i.e. a $\gamma$-run that reaches $\mathsf{l}$ for the first time at step $i$.
We define ${\tt Cost}\left(\rho\right)\left(\mathsf{l}\right)=\sum_{1\leq
j\leq\left|{i}\right|-1}{\tt Cost}\left(\rho[j],\rho[j+1]\right)$, i.e, the
sum of costs of all executed instructions along $\rho$ up to the first visit
to $\mathsf{l}$.

For a configuration $\gamma$, a label $\mathsf{l}$, and a cost function ${\tt
Cost}$, we define a random variable ${X_{\gamma,\mathsf{l},{\tt
Cost}}}\\!:{\Omega}\rightarrow{\mathbb{R}}$ over support
$\Omega=\gamma\boldsymbol{\cdot}{\Gamma}_{{\mathcal{C}}}^{\omega}$ as follows:

$X_{\gamma,\mathsf{l},{\tt
Cost}}\left(\rho\right)=\begin{cases}0&\rho\not\in\\{{\tt
Runs}\left(\gamma\right)~{}|~{}\rho\models_{{\mathcal{P}}}\Diamond^{\\!\\!=i}\mathsf{l}\\}\\\
X_{\gamma,\mathsf{l},{\tt Cost}}\left(\rho\right)={\tt
Cost}\left(\rho\right)\left(\mathsf{l}\right)&\text{otherwise }\end{cases}$

Given: program ${\mathcal{P}}$, configuration $\gamma_{\it init}\in\Gamma^{\tt
plain}_{{\mathcal{P}}}$, cost function ${{\tt
Cost}}\\!:{\mathsf{Lbl}_{{\mathcal{P}}}}\rightarrow{\mathbb{N}^{>0}}$, label
$\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}$ s.t. $\gamma_{\it
init}\models\Diamond\mathsf{l}$, precision value $\epsilon\in\mathbb{R}^{+}$
Exp_Ave_Cost: Determine $\theta$ s.t. $E\left(X_{\gamma_{\it
init},\mathsf{l},{\tt Cost}}~{}\mid~{}{\gamma_{\it
init}}\models\exists\Diamond{\mathsf{l}}\right)\in[\theta,\theta+\varepsilon]$

The expected average cost problem $E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}\right)$ is defined as the expected cost of reaching $\mathsf{l}$ from
$\gamma$ and $E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}~{}\mid~{}{\gamma}\models\exists\Diamond{\mathsf{l}}\right)$ as the
conditional expectation over runs that reach $\mathsf{l}$. If
$\neg(\gamma\models_{{\mathcal{P}}}\exists\Diamond\mathsf{l})$ then the
expected cost is not defined. If however
$\gamma\models_{{\mathcal{P}}}\exists\Diamond\mathsf{l}$ then
$E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}~{}\mid~{}{\gamma}\models\exists\Diamond{\mathsf{l}}\right)={E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}\right)}/{{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond\mathsf{l}\right)}$,
which follows since for the non-reaching runs, the cost is zero. We present
the expected average cost problem, in the figure above, where we want to
approximate $E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}~{}\mid~{}{\gamma}\models\exists\Diamond{\mathsf{l}}\right)$ to
$\varepsilon$-precision.

###  8.2 Eagerness

Our solution to Exp_Ave_Cost relies on the fact that
$\llbracket{{\mathcal{P}}}\rrbracket^{\tt MC}$ satisfies an eagerness property
in the sense of [17]. In our setting, eagerness means that the probability of
avoiding the target label $\mathsf{l}$ decreases exponentially with the number
of steps. Concretely, we show that there are two constants: the eagerness
degree ${\mathcal{E}}_{{\mathcal{P}}}\in\mathbb{R}^{>0}$, and the eagerness
threshold $\eta_{{\mathcal{P}}}\in\mathbb{R}^{>0}$ satisfying the following:

$\forall\gamma\in\Gamma^{\tt
small}_{{\mathcal{P}}}~{}\forall\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}~{}\forall
n\geq\eta_{{\mathcal{P}}}\quad\gamma\models_{{\mathcal{P}}}\exists\Diamond\mathsf{l}\Rightarrow{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\mathsf{l}\right)\leq\left({\mathcal{E}}_{{\mathcal{P}}}\right)^{n}$

i.e. for $n\geq\eta_{{\mathcal{P}}}$, the probability of avoiding $\mathsf{l}$
during the first $n$ steps decreases exponentially with $n$. The following
lemma forms the crux of this section.

######  Lemma 7 (Eagerness Lemma)

${\mathcal{E}}_{{\mathcal{P}}}$ and $\eta_{{\mathcal{P}}}$ exist and are
computable.

We devote this sub-section to give an overview of the the proof of Lemma 7
(the formal proof is provided in the supplementary material). We consider the
behavior of runs with respect to the small and large configurations,
exploiting the fact that the runs of the system tend to gravitate towards the
small configurations. However here we use a property, called left-biasedness
(defined in Sec. 8.2.1), that is stronger than the left-orientedness property
of Sec. 5.1.

To prove Lemma 7, we show that, for a small configuration
$\gamma\in\Gamma^{\tt small}_{{\mathcal{P}}}$, the runs from $\gamma$ satisfy
the following three properties with a high probability: (i) they make their
first return to $\Gamma^{\tt small}_{{\mathcal{P}}}$ within a small number of
steps, (ii) they return to $\Gamma^{\tt small}_{{\mathcal{P}}}$ multiple
times, within a small number of steps, and (iii) if they eventually reach
$\mathsf{l}$ then they will do that within a few steps. We collect these
results to obtain the proof of Lemma 7.

####  8.2.1 Gravity: First Return

We recall that buffer sizes can increase by at most one during process
transitions, and that any number of messages can be flushed to the memory
during an update transition (Sec. 4 and Sec. 5.1). Based on this, we show
left-biasedness, defined as follows:

> Left-biasedness $\forall\gamma\in\Gamma^{\tt large}_{{\mathcal{P}}}$ the
> probability of moving from $\gamma$ to a smaller configuration is bounded
> below by 2/3 and that of moving to a larger configuration is bounded above
> by 1/3, regardless of ${\mathcal{P}}$.

Using left-biasedness, we show that the set $\Gamma^{\tt
small}_{{\mathcal{P}}}$ has a gravity property, namely, a run starting from a
small configuration will, with a high probability, return to the set
$\Gamma^{\tt small}_{{\mathcal{P}}}$ (for the first time) within a few number
of steps. Formally, we define the gravity parameter
${\mathcal{G}}_{{\mathcal{P}}}$ as follows: $\hat{q}:=2/3$, $\hat{p}:=1/3$,
and
${\mathcal{G}}_{{\mathcal{P}}}:=2\sqrt{\hat{q}\cdot\hat{p}}=\frac{2\cdot\sqrt{2}}{3}$.
We prove the following lemma.

######  Lemma 8 (Gravity Lemma)

${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\bigcirc\Diamond^{\\!\\!\geq
n}\Gamma^{\tt
small}_{{\mathcal{P}}}\right)\leq\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n}$,
for all $\gamma\in\Gamma^{\tt small}_{{\mathcal{P}}}$ and all $n\in\mathbb{N}$
.

The lemma states that, starting from a small configuration, the probability
that a run avoids $\Gamma^{\tt small}_{{\mathcal{P}}}$ in the next $n$ steps
decreases exponentially with $n$.

####  8.2.2 Multiple Revisits

Notice that the gravity lemma is concerned with the first return to the set of
small configurations. We will now apply this argument repeatedly to conclude
that, with high probability, multiple re-visits to small configurations take
place “quickly”. That is, the set of runs starting from $\Gamma^{\tt
small}_{{\mathcal{P}}}$ and frequently re-visiting $\Gamma^{\tt
small}_{{\mathcal{P}}}$ has a high measure. To formalize these arguments, we
make the following definition. For $m,n:1\leq m\leq n$, we define ${\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)$ to be the set of runs that visit the
set $\Gamma^{\tt small}_{{\mathcal{P}}}$ exactly $m$ times in their first
$n-1$ steps777For technical convenience, we use $n-1$ instead of $n$ in the
definition of ${\tt Visit}$. This allows us to avoid some corner cases in the
proofs.. We use the ${\tt Visit}$ predicate to partition the set of
$\gamma$-runs, depending on how often they return to $\Gamma^{\tt
small}_{{\mathcal{P}}}$ during their first $n$ steps. We distinguish these as
Sporadic-Runs (S-Runs): runs that visit the $\Gamma^{\tt
small}_{{\mathcal{P}}}$ sporadically during their first $n$ steps, and
Frequent-Runs (F-Runs): runs that visit $\Gamma^{\tt small}_{{\mathcal{P}}}$
frequently during their first $n$ steps. We will derive a constant
$\nu\in\mathbb{N}$ (see below) that delineates the border between these sets.
We formally define:

$\displaystyle{\tt SRuns}\left(\gamma\right)\left(n\right)$ $\displaystyle:=$
$\displaystyle\cup_{1\leq
m\leq\left\lfloor\frac{n}{\nu}\right\rfloor}\left\\{\rho\in{\tt
Runs}\left(\gamma\right)~{}|~{}\;{\rho\models{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)}\right\\}$ $\displaystyle{\tt
FRuns}\left(\gamma\right)\left(n\right)$ $\displaystyle:=$
$\displaystyle\cup_{\left\lfloor\frac{n}{\nu}\right\rfloor+1\leq m\leq
n}\left\\{\rho\in{\tt Runs}\left(\gamma\right)~{}|~{}\;{\rho\models{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)}\right\\}$

Figure 5:  Figure depicting configuration sequences of S, F and D runs. Green
dots represent small configurations, blue dots represent large configurations.
All runs start in a small (plain) configuration. Within the first $n$
configurations: the S-run visits $\Gamma^{\tt small}_{{\mathcal{P}}}$ at most
$\lfloor\frac{n}{\nu}\rfloor$ times, the F, D runs visit $\Gamma^{\tt
small}_{{\mathcal{P}}}$ at least $\lfloor\frac{n}{\nu}\rfloor+1$ times. A
D-run is a special case of an F-run which does not visit label $\mathsf{l}$
(red dot) in the first $n$ steps.

The value of $n/\nu$ distinguishes the S-Runs from the F-Runs. Our goal is to
give an upper bound on the measure of the S-Runs. For a prefix path $\pi$ of
length $n$, there are $\genfrac{(}{)}{0.0pt}{2}{n-1}{m-1}$ ways to choose the
$m-1$ indices along $\pi$ at which $\Gamma^{\tt small}_{{\mathcal{P}}}$ is
reached (since the run starts from $\Gamma^{\tt small}_{{\mathcal{P}}}$). Each
of the $m-1$ path fragments between these indices represents one consecutive
revisit of $\Gamma^{\tt small}_{{\mathcal{P}}}$. By Lemma 8, the measure of
the set of such runs is bounded by
$\left({\mathcal{G}}_{{\mathcal{P}}}\right)^{n-m}=\left(\frac{2\sqrt{2}}{3}\right)^{n-m}$,
giving

${\it Prob}_{{\mathcal{P}}}\left({\tt
SRuns}\left(\gamma\right)\left(n\right)\right)\,\leq\,\sum_{m=1}^{\lfloor\frac{n}{\nu}\rfloor}\genfrac{(}{)}{0.0pt}{2}{n-1}{m-1}\cdot{\mathcal{G}}_{{\mathcal{P}}}^{n-m}\;\leq\;\left(\sqrt{\frac{8}{3}}\cdot\left(\frac{\nu}{\nu-1}\right)\cdot\left(2+\sqrt{3}\cdot\nu\right)^{\lfloor\frac{1}{\nu}\rfloor}\right)^{n}$

under the condition that $4\leq 2\cdot\nu\leq n$. The second inequality is
obtained through algebraic manipulations using
${\mathcal{G}}_{{\mathcal{P}}}=\frac{2\cdot\sqrt{2}}{3}$. Define
$f(x):=\sqrt{\frac{8}{3}}\cdot\left(\frac{x}{x-1}\right)\cdot\left(2+\sqrt{3}\cdot
x\right)^{\lfloor\frac{1}{x}\rfloor}$. We have $f(150)=0.986<1$. Hence, for
parameter $\nu:=150$, defining ${\mathcal{E}}^{\tt
S}_{{\mathcal{P}}}:=f(\nu)$, we have the following lemma, where the bound
decays exponentially with $n$ since ${\mathcal{E}}^{\tt S}_{{\mathcal{P}}}<1$.

######  Lemma 9 (S-Run Bound)

${\it Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}{\tt
SRuns}\left(\gamma\right)\left(n\right)\right)\leq\left({\mathcal{E}}^{\tt
S}_{{\mathcal{P}}}\right)^{n}$, for all $\gamma\in\Gamma^{\tt
small}_{{\mathcal{P}}}$ and all $n$ such that $300=2\cdot\nu\leq n$.

####  8.2.3 Reaching the label $\mathsf{l}$

We now turn our attention to the set of F-Runs. Our goal is to show that if an
F-Run reaches $\mathsf{l}$ then, with a high probability, it will reach
$\mathsf{l}$ “quickly”. To that end, we consider the opposite scenario and
introduce a subset of the F-Runs which we call Delayed Runs (D-Runs):

${\tt
DRuns}\left(\gamma\right)\left(\mathsf{l}\right)\left(n\right):=\cup_{m=\lfloor\frac{n}{\nu}\rfloor+1}^{n}\left\\{\rho\in{\tt
Runs}\left(\gamma\right)~{}|~{}\;{\rho\models_{{\mathcal{P}}}\Diamond^{\\!\\!=n}\mathsf{l}\land{\tt
Visit}_{{\mathcal{P}}}\left(n,m\right)}\right\\}$

A D-Run is an F-Run that delays its first visit to the label $\mathsf{l}$
until the $n^{\it th}$ step for some $n$. We show that the measure of D-Runs
decreases $n$ increases. Note that $\mathsf{l}$ is reachable from all
configurations from a path that ends at $\mathsf{l}$. Therefore, we consider
the set ${\mathcal{A}}:=\left\\{\gamma\in\Gamma^{\tt
small}_{{\mathcal{P}}}~{}|~{}\;{\gamma\models_{{\mathcal{P}}}\exists\Diamond\mathsf{l}}\right\\}$,
of small configurations from which $\mathsf{l}$ is reachable. We analyze how
often a run starting from a small configuration, visits ${\mathcal{A}}$ before
finally visiting the label $\mathsf{l}$. For sets of configurations
$G_{1},G_{2}\subseteq\Gamma_{{\mathcal{P}}}$, a run $\rho$, and
$m\in\mathbb{N}$, we write $\rho\models G_{1}\,{\tt Before}^{m}\,G_{2}$ to
denote that $\rho$ visits the set $G_{1}$ at least $m$ times before visiting
$G_{2}$ for the first time. Notice

$\displaystyle{\tt
DRuns}\left(\gamma\right)\left(\mathsf{l}\right)\left(n\right)$
$\displaystyle\subseteq$
$\displaystyle\bigcup_{m=\lfloor\frac{n}{\nu}\rfloor+1}^{n}\left\\{\rho\in{\tt
Runs}\left(\gamma\right)~{}|~{}\;{\rho\models_{{\mathcal{P}}}{\mathcal{A}}\,{\tt
Before}^{m}\,\mathsf{l}}\right\\}$ (2)

To upper bound the measure of D-Runs, we start by upper bounding the measure
of the set $\left\\{\rho\in{\tt
Runs}\left(\gamma\right)~{}|~{}\;{\rho\models_{{\mathcal{P}}}{\mathcal{A}}\,{\tt
Before}^{m}\,\mathsf{l}}\right\\}$, i.e. $\gamma$-runs making $m$ visits to
${\mathcal{A}}$ before visiting $\mathsf{l}$. We consider the probability that
a run from a small configuration $\gamma$ does visit $\mathsf{l}$ before
returning to $\gamma$. We can compute a $\mu$ such that

$\displaystyle 0<\mu\leq\min_{\gamma\in{\mathcal{A}}}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models\bigcirc(\mathsf{l}\,{\tt
Before}^{1}\,\gamma)\right)$ (3)

Hence $\mu$ is a lower bound on the measure of runs that start from some
configuration in $\gamma\in{\mathcal{A}}$ and visit $\mathsf{l}$ before
returning to $\gamma$. To obtain an upper bound on the measure of D-Runs, we
show the following inequality:

${\it Prob}_{{\mathcal{P}}}\left({\tt
DRuns}\left(\gamma\right)\left(\mathsf{l}\right)\left(n\right)\right)\leq\sum\limits_{m=\lfloor\frac{n}{\nu}\rfloor+1}^{n}\sum\limits_{\gamma^{\prime}\in{\mathcal{A}}}(1-\mu)^{\left\lceil\frac{m}{\left|{{\mathcal{A}}}\right|}\right\rceil-1}\leq\frac{\left|{{\mathcal{A}}}\right|}{(1-\mu)\cdot\left(1-(1-\mu)^{\frac{1}{\left|{{\mathcal{A}}}\right|}}\right)}\cdot\left((1-\mu)^{\frac{n}{\nu\cdot\left|{{\mathcal{A}}}\right|}}\right)$

The first inequality follows from formulas 2 and 3, while the second is
obtained through algebraic techniques. Define ${\mathcal{E}}^{\tt
D}_{{\mathcal{P}}}$ such that
$(1-\mu)^{\frac{1}{\nu\cdot\left|{{\mathcal{A}}}\right|}}<{\mathcal{E}}^{\tt
D}_{{\mathcal{P}}}<1$. Such an ${\mathcal{E}}^{\tt D}_{{\mathcal{P}}}$ is
computable since $\nu$, ${\mathcal{A}}$, $\mu$ are computable. Since
$(1-\mu)^{\frac{1}{\nu\cdot\left|{{\mathcal{A}}}\right|}}<{\mathcal{E}}^{\tt
D}_{{\mathcal{P}}}$ it follows that there is a natural number, denoted by
$\eta^{\tt D}_{{\mathcal{P}}}$, such that
$\frac{\left|{{\mathcal{A}}}\right|}{(1-\mu)\cdot(1-(1-\mu)^{\frac{1}{\left|{{\mathcal{A}}}\right|}})}\cdot\left((1-\mu)^{\frac{1}{\nu\cdot\left|{{\mathcal{A}}}\right|}}\right)^{n}\leq({\mathcal{E}}^{\tt
D}_{{\mathcal{P}}})^{n}$ for all $n\geq\eta^{\tt D}_{{\mathcal{P}}}$. This
gives the following lemma.

######  Lemma 10 (D-Run Bound)

${\it Prob}_{{\mathcal{P}}}\left({\tt
DRuns}\left(\gamma\right)\left(\mathsf{l}\right)\left(n\right)\right)\leq\left({\mathcal{E}}^{\tt
D}_{{\mathcal{P}}}\right)^{n}$, for all $\gamma\in\Gamma^{\tt
small}_{{\mathcal{P}}}$ and all $n\geq\eta^{\tt D}_{{\mathcal{P}}}$.

####  8.2.4 Proof of Lemma 7

We now give a sketch of the proof of the eagerness property.

Choose a value ${\mathcal{E}}^{\tt SD}_{{\mathcal{P}}}$ such that,
$\max({\mathcal{E}}^{\tt S}_{{\mathcal{P}}},{\mathcal{E}}^{\tt
D}_{{\mathcal{P}}})<{\mathcal{E}}^{\tt SD}_{{\mathcal{P}}}<1$. From Lemma 9
and Lemma 10 it follows that for some constant $\eta^{\tt
SD}_{{\mathcal{P}}}>\max(\eta^{\tt D}_{{\mathcal{P}}},300)$, ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!=n}\mathsf{l}\right)\leq({\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}})^{n}$, for all $n>\eta^{\tt SD}_{{\mathcal{P}}}$
(sufficiently large). The final step is to extend the argument to the set of
$\gamma$-runs that reach $\mathsf{l}$ in $n$ or more steps (as required by
Lemma 7).

$\begin{array}[]{l}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\mathsf{l}\right)=\sum_{k=n}^{\infty}{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!=n}\mathsf{l}\right)\leq\sum_{k=n}^{\infty}\left({\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}\right)^{k}=\frac{\left({\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}\right)^{n}}{1-{\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}}\end{array}$

Choose ${\mathcal{E}}_{{\mathcal{P}}}$, (exists since ${\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}<1$) such that ${\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}<{\mathcal{E}}_{{\mathcal{P}}}<1$. There exists an
$\eta_{{\mathcal{P}}}$ such that $\frac{\left({\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}\right)^{n}}{1-{\mathcal{E}}^{\tt
SD}_{{\mathcal{P}}}}\leq\left({\mathcal{E}}_{{\mathcal{P}}}\right)^{n}$ for
all $n\geq\eta_{{\mathcal{P}}}$, and hence ${\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond^{\\!\\!\geq
n}\mathsf{l}\right)\geq\left({\mathcal{E}}_{{\mathcal{P}}}\right)^{n}$ for all
$n\geq\eta_{{\mathcal{P}}}$ (sufficiently large). This gives us the result.

###  8.3 The Algorithm

Now we proceed to describe the algorithm. The goal is to approximate
$E\left(X_{\gamma_{\it init},\mathsf{l},{\tt Cost}}~{}\mid~{}{\gamma_{\it
init}}\models\exists\Diamond{\mathsf{l}}\right)$. The scheme followed by the
algorithm is similar to the quantitative section: it iteratively improves an
approximations until it is $\varepsilon$-precise. However, the implementation
is much more challenging since we need to maintain error margins on both the
cost and the probabilities. It performs forward reachability analysis,
starting from $\gamma_{\it init}$, and generating, successively longer
$\gamma_{\it init}$-paths, in a breadth-first manner.

The variable
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ contains triples of form $\langle\gamma,\psi,\phi\rangle$
corresponding to $\gamma_{\it init}$-paths waiting to be analysed. For such a
path $\pi$, $\gamma$ is the last configuration of $\pi$, $\psi$ is the cost of
$\pi$, and $\phi$ is the probability of taking $\pi$. We initialize
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ to contain a triple corresponding to the empty path from
$\gamma_{\it init}$: $\langle\gamma_{\it init},0,1\rangle$. Prior to the
$i^{\it th}$ iteration loop (line 10),
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ contains triples corresponding to paths of length $i$. At each loop
iteration the triples in
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}$ are analysed and the triples for paths one step deeper are generated
for the next iteration.

Input: ${\mathcal{P}}$: program; $\gamma_{\it init}\in\Gamma_{{\mathcal{P}}}$:
configuration $\mathsf{l}\in\mathsf{Lbl}_{\mathcal{P}}$: label with
$\gamma_{\it init}\models\exists\Diamond\mathsf{l}$;

${{\tt Cost}}\\!:{\mathsf{Instr}_{{\mathcal{P}}}}\rightarrow{\mathbb{R}}$:
cost function; $\varepsilon\in\mathbb{R}^{>0}$: precision;

1 Var

2
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}^{\prime}}\in{(\Gamma_{{\mathcal{P}}}\times\mathbb{R}\times\mathbb{R})}^{*}$:
queues

3
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}\in\mathbb{R}$: approximation of $E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}\right)$

4
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}\in\mathbb{R}$: under-approximation of ${\it
Prob}_{\llbracket{{\mathcal{P}}}\rrbracket^{\tt
MC}}\left(\gamma\models_{{\mathcal{P}}}\Diamond\mathsf{l}\right)$

5
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}\in\mathbb{R}$,
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}\in\mathbb{R}$: over-approximations of errors

6
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}k},{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}n}\in\mathbb{N}$;

7${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}k}:=\tt
MaxCost\left({\tt Cost}\right)$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}n}:=0$

8
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}:=0$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}:=0$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:=\left\langle\gamma_{\it init},0,1\right\rangle$

9
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}:=\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}k}}{\left(1-{\mathcal{E}}_{{\mathcal{P}}}\right)^{2}}$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}:=\frac{1}{1-{\mathcal{E}}_{{\mathcal{P}}}}$

10 repeat

11
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}n}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}n}+1$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}^{\prime}}:=\emptyset$

12 for  _$i=1$ to
$\left|{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}}\right|$_ do

13
$\left\langle\gamma,\psi,\phi\right\rangle:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}[i]$

14 if  _$\mathsf{l}\in\gamma$_ then

15
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}+\psi\cdot\phi$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}+\phi$

16

17 else

18 for  _all
$\gamma^{\prime}:\gamma\xrightarrow{}_{{\mathcal{P}}}\gamma^{\prime}$_ do

19
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}^{\prime}}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}^{\prime}}\boldsymbol{\cdot}\left\langle\gamma^{\prime},\psi+{\tt
Cost}\left(\gamma,\gamma^{\prime}\right),\phi\cdot{\texttt{M}}_{{\mathcal{P}}}\left(\gamma,\gamma^{\prime}\right)\right\rangle$

20

21
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}\cdot{\mathcal{E}}_{{\mathcal{P}}}$;
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}\cdot{\mathcal{E}}_{{\mathcal{P}}}$

22
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}:={\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
waiting}^{\prime}}$

23

24until
_$\left(\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}}-\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}}
<\varepsilon\right)\land({\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}>0)\land(n\geq\eta_{{\mathcal{P}}})$_

return
_$\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}}$_

Algorithm 3 Solving Exp_Ave_Cost

Figure 6: The expected average cost algorithm.

The iterations calculate increasingly precise approximations of
$E\left(X_{\gamma_{\it init},\mathsf{l},{\tt Cost}}\right)$, and of ${\it
Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models_{{\mathcal{P}}}\Diamond\mathsf{l}\right)$, maintained in
variables
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}$, respectively. We maintain two additional variables
(${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}$) that help us to provide an upper bound on the estimation errors.
Defining $\tt MaxCost\left({\tt Cost}\right):=\max\left\\{{\tt
Cost}\left(\mathsf{l}\right)~{}|~{}\;{\mathsf{l}\in\mathsf{Lbl}_{{\mathcal{P}}}}\right\\}$,
we explain the correctness of the algorithm with a number of invariants.

###### Lemma 11

The algorithm maintains the following invariants where invariants (1,2,5,6)
hold for all $i>0$ and invariants (3,4) hold for all
$i\geq\eta_{{\mathcal{P}}}$.

  1. 1.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(i)}}=\sum\limits_{\\{\rho\in{\tt Runs}\left(\gamma_{\it
init}\right)~{}|~{}\rho\models\Diamond^{\\!\\!\leq i}\mathsf{l}\\}}{\tt
Cost}\left(\rho\right)\cdot{\it Prob}_{{\mathcal{P}}}\left(\rho\right)$:

  2. 2.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(i)}}={\it Prob}_{{\mathcal{P}}}\left(\gamma_{\it
init}\models\Diamond^{\\!\\!\leq i}\mathsf{l}\right)$:

  3. 3.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(i)}}\leq E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(i)}}$.

  4. 4.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(i)}}\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond\mathsf{l}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(i)}}$.

  5. 5.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(i)}}=\tt MaxCost\left({\tt
Cost}\right)\cdot\frac{{\mathcal{E}}_{{\mathcal{P}}}^{i}}{(1-{\mathcal{E}}_{{\mathcal{P}}})^{2}}$.

  6. 6.

${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(i)}}=\frac{{\mathcal{E}}_{{\mathcal{P}}}^{i}}{1-{\mathcal{E}}_{{\mathcal{P}}}}$.

Invariants 5 and 6 imply that as $i\rightarrow\infty$
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(i)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(i)}}$ tend to 0. Hence,
$\lim_{i\rightarrow\infty}\left(\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(i)}}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(i)}}}-\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(i)}}-{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(i)}}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(i)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(i)}}}\right)=0$ implying termination. Since
$n\geq\eta_{{\mathcal{P}}}$ when the algorithm terminates, by invariants 3 and
4 it follows that
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(n)}}\leq E\left(X_{\gamma,\mathsf{l},{\tt
Cost}}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(n)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostError}^{(n)}}$ and
${\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(n)}}\leq{\it
Prob}_{{\mathcal{P}}}\left(\gamma\models_{{\mathcal{P}}}\Diamond\mathsf{l}\right)\leq{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(n)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(n)}}$. Combining these two inequalities and the termination
condition of the algorithm, we get the following:

Hence on termination,
$\theta:=\frac{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
CostApprx}^{(n)}}}{{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbApprx}^{(n)}}+{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}{\color[rgb]{0.140625,0.109375,0.890625}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.109375,0.890625}\tt
ProbError}^{(n)}}}$ is within $\varepsilon$-precision of the true value,
implying correctness of the algorithm. We get the following theorem.

###### Theorem 5

The above algorithm solves Exp_Ave_Cost.

Related Work Only recently there has been an increased interest in the
formulation and verification of liveness properties for weak memory models. In
[31], they factor the system into a process and memory subsystems and define
notions of fairness for either. This is reminiscent of our approach, where we
consider probabilistic policies for process scheduling and memory update.
Their model on the other hand is non-probabilistic and they have weaker
fairness guarantees, which we describe in more detail in Sec. 5.1. The
liveness verification problem for TSO has been considered in [30], where they
show undecidability for various liveness properties. However, once again work
with non-probabilistic notions of fairness. We show in this paper, that with
stronger (probabilistic) fairness, reachability and repeated reachability
problems become decidable.

In [12], they show the undecidability of the repeated reachability problem,
without fairness conditions, for finite-state programs running under the TSO
semantics. In contrast, we show that checking repeated reachability
qualitatively is decidable (Sec. 6.2), and that we can even compute the
measure of runs satisfying the property with arbitrary precision (Sec. 7.2).

There has been a huge amount of work on the verification of finite-state
Markov chains (see, e.g., [20, 32]). Since the buffers in TSO are unbounded,
we however, get an infinite-state Markov chain. There is also a substantial
literature on the verification of infinite-state Markov chains, where
specialized techniques are developed for particular classes of systems.
Several works have considered probabilistic push-down automata and
probabilistic recursive machines [33, 34, 35]. However, these techniques don’t
apply in our case since push-down automata cannot encode the FIFO store-buffer
data-structure.

Works such as [36, 16, 37, 38] develop algorithmic and complexity results for
checking termination and reachability for systems such as probabilistic VASS,
probabilistic Petri nets, probabilistic multi-counter systems. Again, these
models are different from ours and cannot encode FIFO queues.

The works closest to ours are those on probabilistic lossy channel systems
[16, 17]. These works also rely on the frameworks of decisive and eager Markov
chains. However, lossy channel systems and TSO are fundamentally different,
and the manner in which we instantiate the frameworks of decisive/eager Markov
chains differs. The decidability of verification for probabilistic extensions
of lossy channels is sensitive to the definition of the message losses. In the
case of lossy channel systems, if messages are only allowed to be lost at one
end of the channel (a model that is close to our notion of message updates),
then all non-trivial verification problems become undecidable for
probabilistic lossy channel systems [39]. Therefore, although there is a
reduction from TSO to lossy channel systems in the case of non-probabilistic
models [12], we know of no such reduction between the corresponding
probabilistic models.

Finally, the concept of decisiveness has been extended to more general models
such as generalized semi-Markov processes, stochastic timed automata [40], and
lossy channel-based stochastic games [41].

##  9 Conclusions, Discussions, and Perspectives

We presented PTSO, a probabilistic extension of the classical TSO semantics.
We have shown decidability/computability results for a wide a range of
properties such as quantitative and qualitative reachability/repeated
reachability and expected average costs. As far as we know, this is the first
study of probabilistic verification for weak memory models, and opens many
avenues for future work.

Refined Probability Distributions. For ease of presentation, we developed our
results in the context of specific scheduling and update policies. However, we
emphasize that our results carry-over to policies satisfying faithfulness and
left-orientedness, which are fairly weak conditions. Hence we believe that
developing more refined models that better capture behaviours of TSO
implementations, using techniques such as parameter estimation, is interesting
future work.

General Cost Models Similar can be said for cost models: our algorithm works
for all cost functions such that the cost of a path is exponentially bounded
by its length. In particular, developing cost models that closely mimic usage
of processor resources, e.g. cost based on read from local store-buffer vs.
read from memory, can be useful to gain a better understanding of the
implementation.

Other Memory Models Finally, we are interested in extending our approach to
other weak memory models such as RA/SRA, POWER, ARM.

## References

  * [1] L. Lamport.  How to make a multiprocessor that correctly executes multiprocess programs.  IEEE Trans. on Computers, C-28:690–691, 1979.
  * [2] Sarita V. Adve and Kourosh Gharachorloo.  Shared memory consistency models: A tutorial.  IEEE Computer, 29(12):66–76, 1996.