Software Modeling and Verification Group, RWTH Aachen University,
<EMAIL_ADDRESS>aachen.dehttps://orcid.org/0000-0001-7837-2611Software Modeling and
Verification Group, RWTH Aachen University<EMAIL_ADDRESS>aachen.dehttps://orcid.org/0000-0002-6143-1926 Software Modeling and
Verification Group, RWTH Aachen University<EMAIL_ADDRESS>aachen.dehttps://orcid.org/0000-0002-1865-1798 Ira Fesefeldt, Joost-Pieter
Katoen, and Thomas Noll [500]Theory of computation Program verification
[300]Theory of computation Concurrent algorithms [300]Mathematics of computing
Probabilistic reasoning algorithms John Q. Open and Joan R. Access 2 42nd
Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December
24–27, 2016 Little Whinging, United Kingdom 42 23 [name=Theorem,
numberwithin=section, refname=theorem,theorems,
Refname=Theorem,Theorems]retheorem [name=Definition, numberwithin=section,
refname=definition,definitions, Refname=Definition,Definitions]redefinition

# Towards Concurrent Quantitative Separation Logic

Ira Fesefeldt  Joost-Pieter Katoen  Thomas Noll

###### Abstract

In this paper, we develop a novel verification technique to reason about
programs featuring concurrency, pointers and randomization. While the
integration of concurrency and pointers is well studied, little is known about
the combination of all three paradigms. To close this gap, we combine two
kinds of separation logic – Quantitative Separation Logic and Concurrent
Separation Logic – into a new separation logic that enables reasoning about
lower bounds of the probability to realise a postcondition by executing such a
program.

###### keywords:

Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency

##  1 Introduction and Related Work

In this paper, we aim to provide support for formal reasoning about concurrent
imperative programs that are extended by two important features: dynamic data
structures and randomisation. In other words, it deals with the analysis and
verification of concurrent probabilistic pointer programs. This problem is of
practical interest as many concurrent algorithms operating on data structures
use randomisation to reduce the level of interaction between threads. For
example, probabilistic skip lists [47] work well in the concurrent setting
[16] because threads can independently manipulate nodes in the list without
much synchronisation. In contrast, scalability of traditional balanced tree
structures is difficult to achieve, since re-balancing operations may require
locking access to large parts of the data structure. Bloom filters are another
example of a probabilistic data structure supporting parallel access [8]. A
further aspect is that stochastic modelling naturally arises when analysing
faulty behaviour of (concurrent) software systems, as we later demonstrate in
Section 5.

However, the combination of these features poses severe challenges when it
comes to implementing and reasoning about concurrent randomised algorithms
that operate on dynamic data structures. To give a systematic overview of
related approaches, we mention that a number of program logics for reasoning
about concurrent software have been developed [13, 14, 17, 29, 31, 42]. Next,
we will address the programming-language extensions in isolation and then
consider their integration. An overview is shown in Figure 1.

Concurrency Pointers
---
SL [25, 49]
Randomisation
---
Expectations [38]
Prob. rel.-guar.
---
calc. [39]
CSL [44]QSL [5] Polaris [50]
---
CQSL
Figure 1: Overview of programming language features and formal approaches
(CQSL denotes our concurrent extension of QSL)

_Pointers._ Pointers constitute an essential concept in modern programming
languages, and are used for implementing dynamic data structures like lists,
trees etc. However, many software bugs can be traced back to the erroneous use
of pointers by e.g. dereferencing null pointers or accidentally pointing to
wrong parts of the heap, creating the need for computer-aided verification
methods. The most popular formalism for reasoning about such programs is
Separation Logic (SL) [25, 49], which supports Hoare-style verification of
imperative, heap-manipulating and, possibly, concurrent programs. Its
assertion language extends first-order logic with connectives that enable
concise specifications of how program memory, or other resources, can be
split-up and combined. In this way, SL supports local reasoning about the
resources employed by programs. Consequently, program parts can be verified by
considering only those resources they actually access – a crucial property for
building scalable tools including automated verifiers [7, 27, 41, 46], static
analysers [6, 10, 19], and interactive theorem provers [30].

The notion of resources, and in particular their controlled access, becomes
even more important in a concurrent setting. Therefore, SL has been extended
to Concurrent Separation Logic (CSL) [44] to enable reasoning about resource
ownership, where the resource typically is dynamically allocated memory (i.e.,
the heap). The popularity of CSL is evident by the number of its extensions
[9]. Of particular importance to our work is [52], which presents a soundness
result for CSL that is formulated in an inductive manner, matching the ?small-
step? operational style of semantics. Here, we will employ a similar technique
that also takes quantitative aspects (probabilities) into account.

_Randomisation._ Probabilistic programs (i.e., programs with the ability to
sample from probability distributions) are increasingly popular for
implementing efficient randomised algorithms [40] and describing uncertainty
in systems [11, 18], among other similar tasks. In such applications, the
purely qualitative (true vs. false) approach of classical logic is obviously
not sufficient. The method advocated by us is based on weakest precondition
reasoning as established in a classical setting by Dijkstra [12]. It has been
extended to provide semantic foundations for probabilistic programs by Kozen
[33, 34] and McIver & Morgan [38]. The latter also coined the term ?weakest
preexpectation? for random variables that take over the role of logical
formulae when doing quantitative reasoning about probabilistic programs – the
quantitative analogue of weakest preconditions. Their relation to operational
models is studied in [20]. Moreover, weakest preexpectation reasoning has been
shown to be useful for obtaining bounds on the expected resource consumption
[43] and, especially, the expected run-time [32] of probabilistic programs.

However, verification techniques that support reasoning about both
randomisation and dynamic data structures are rare – a surprising situation
given that randomised algorithms typically rely on such data structures. One
notable exception is the extension of SL to Quantitative Separation Logic
(QSL) [4, 5], which marries SL and weakest preexpectations. QSL has
successfully been applied to the verification of randomised algorithms, and
QSL expectations have been formalised in Isabelle/HOL [23]. The present work
builds on these results by additionally taking concurrency into account.

A prior program logic designed for reasoning about programs that are both
concurrent and randomised but do not maintain dynamic data structures is the
probabilistic rely-guarantee calculus developed by McIver et al. [39], which
extends Jones’s original rely-guarantee logic [29] by probabilistic
constructs.

Later, Tassarotti & Harper [50] address the full setting of concurrent
probabilistic pointer programs by combining CSL with probabilistic relational
Hoare logic [3] to obtain Polaris, a Concurrent Separation Logic with support
for probabilistic reasoning. Verification is thus understood as establishing a
relation between a program to be analysed and a program which is known to be
well-behaved. Programs which do not almost surely terminate, however, are
outside the scope of their approach. In contrast, the goal of our method is to
directly measure quantitative program properties on source-code level using
weakest liberal preexpectations defined by a set of proof rules, including
possibly non-almost surely terminating programs. Since the weakest liberal
preexpectation includes non-termination probability, we can use invariants to
bound the weakest liberal preexpectation of loops from below.

The main contributions of this paper are:

  * •

the definition of a concurrent heap-manipulating probabilistic guarded command
language (chpGCL) and its operational semantics in terms of Markov Decision
Processes (MDP);

  * •

a formal framework for reasoning about quantitative properties of chpGCL
programs, which is obtained by extending classical weakest liberal
preexpectations by resource invariants;

  * •

a sound proof system that supports backward reasoning about such
preexpectations; and

  * •

the demonstration of our verification method on a (probabilistic) producer-
consumer example.

The remainder of this paper is organised as follows. Section 2 introduces QSL
as an assertion language for quantitative reasoning about (both sequential and
concurrent) probabilistic pointer programs. In Section 3, we present the
associated programming language (chpGCL) together with an operational
semantics. Next, in Section 4 we develop a calculus for reasoning about lower
bounds of weakest liberal preexpectations. Its usage is demonstrated in
Section 5, and in Section 6 we conclude and explain further research
directions. The main part of the paper is accompanied by an extensive appendix
providing elaborated proofs and additional details about the examples.

##  2 Quantitative Separation Logic

To reason about probability distributions over states of a program, we use
Quantitative Separation Logic (QSL) [5, 36]. QSL is an extension of classical
(or _qualitative_) Separation Logic in the sense that instead of mapping
stack/heap pairs to booleans in order to gain a set characterization of
states, we assign probabilities to stack/heap pairs.

######  Definition 2.1 (Stack).

Let $\mathsf{Vars}$ be a fixed set of variables. A stack
$s\colon\mathsf{Vars}\to\mathbb{Z}$ is a mapping from variable symbols to
values. We denote the set of all stacks by Stacks.

When evaluating an (arithmetic or boolean) expression $e$ with respect to a
stack $s$, we write $e(s)$. In this sense, expressions are mappings from
stacks to values. The stack that agrees with a stack $s$ except for the value
of $x$, which is mapped to $v$, is denoted as $s\left[{x}\coloneqq{v}\right]$.

######  Definition 2.2 (Heaps).

A heap $h\colon L\to\mathbb{Z}$ is a mapping from a finite subset of locations
$L\subset\mathbb{N}_{>0}$ to values. We denote the set of all heaps by Heaps.
We furthermore write $\textsf{{dom}}\left({h}\right)$ for the domain of $h$,
$h_{1}\mathrel{\bot}h_{2}$ if and only if
$\textsf{{dom}}\left({h_{1}}\right)\cap\textsf{{dom}}\left({h_{2}}\right)=\emptyset$,
and for disjoint heaps $h_{1}\mathrel{\bot}h_{2}$ we define the disjoint union
of heaps $h_{1}$ and $h_{2}$ as

$(h_{1}\mathbin{{\star}}h_{2})(\ell)\quad=\quad\begin{cases}h_{1}(\ell)&\text{if}\leavevmode\nobreak\
\ell\in\textsf{{dom}}\left({h_{1}}\right)\\\
h_{2}(\ell)&\text{if}\leavevmode\nobreak\
\ell\in\textsf{{dom}}\left({h_{2}}\right)\\\
\text{undef}&\text{else}\leavevmode\nobreak\ .\end{cases}$

A pair of a _stack_ and a _heap_ is a _state_ of the program. The stack is
used to describe the variables of the program. The heap describes the
addressable memory of the program.

######  Definition 2.3 (Program States).

A program state $\sigma\in\textsf{{Stacks}}\times\textsf{{Heaps}}$ is a pair
consisting of a stack and a heap. The set of all states is denoted by States.

_Expectations_ are _random variables_ that map states to non-negative reals.
In this paper, we only consider one-bounded expectations. These do not map
states to arbitrary non-negative reals, but only to reals between $0$ and $1$.
The nomenclature of calling these expectations rather than random variables is
due to the weakest preexpectation calculus being used to derive expectations.

######  Definition 2.4 (Expectations).

A (one-bounded) expectation $X\colon\textsf{{States}}\to[0,1]$ is a mapping
from program states to probabilities. We write $\mathbb{E}_{\leq 1}$ for the
set of all (one-bounded) expectations. We call an expectation $\varphi$
qualitative if for all $(s,h)\in\textsf{{States}}$ we have that
$\varphi(s,h)\in\\{0,1\\}$. We define the partial order $(\mathbb{E}_{\leq
1},\leq)$ as the pointwise application of less than or equal, i.e., $X\leq Y$
if and only if $\forall(s,h)\in\textsf{{States}}\leavevmode\nobreak\
X(s,h)\leq Y(s,h)$.

We use capital letters for regular (one-bounded) expectations and Greek
letters for qualitative expectations. As in [5], we choose to not give a
specific syntax for QSL since the weakest liberal preexpectation of a given
postexpectation – for which we provide more detail in Section 3 – may not be
expressible in a given syntax. Instead, we prefer to interpret expectations as
_extensional objects_ that can be combined via various connectives. These
connectives include (but are not limited to) the pointwise-applied connectives
of addition, multiplication, exponentiation, maximum and minimum. As it is
common in quantitative logics, the maximum/minimum is the quantitative
extension of disjunction/conjunction, respectively. However, multiplication
can be chosen as the quantitative extension of conjunction as well. We denote
the substitution of a variable $x$ by the expression $e$ in the expectation
$X$ as $X\left[{x}\coloneqq{e}\right]$ and define it as
$X\left[{x}\coloneqq{e}\right](s,h)=X(s\left[{x}\coloneqq{e(s)}\right],h)$.
When dealing with state predicates, we use Iverson brackets [26] to cast
boolean values into integers:

$\left[{b}\right](s,h)=\begin{cases}1&\text{if}\leavevmode\nobreak\ (s,h)\in
b\\\ 0&\text{else}\end{cases}$

Note that we could also define predicates as mappings from states to $0$ or
$1$. We refrain from this, since (1) usage of Iverson brackets is standard in
weakest preexpectation reasoning and (2) we may use QSL inside of Iverson
brackets.

For a state $(s,h)$, the empty heap predicate emp holds if and only if
$\textsf{{dom}}\left({h}\right)=\emptyset$, the points-to predicate $e\mapsto
e_{0},\dots,e_{n}$ holds if and only if
$\textsf{{dom}}\left({h}\right)=\\{e(s)+0,\dots,e(s)+n\\}$ and $\forall
i\in\\{0,\dots,n\\}\leavevmode\nobreak\ h(e(s)+i)=e_{i}(s)$, the allocated
predicate $e\mapsto\,{-}\,$ holds if and only if
$\textsf{{dom}}\left({h}\right)=\\{e(s)\\}$, and the equality predicate
$e=e^{\prime}$ holds if and only if $e(s)=e^{\prime}(s)$.

We also use quantitative extensions of two separation connectives – the
separating conjunction and the magic wand. The quantitative extension of the
separating conjunction, which we call _separating multiplication_ , maximises
the value of the product of its arguments applied to separated heaps:

$(X\mathbin{{\star}}Y)(s,h)=\sup\left\\{\,X(s,h_{1})\cdot
Y(s,h_{2})\,\mid\,h_{1}\mathbin{{\star}}h_{2}=h\,\right\\}$

The definition of separating multiplication is similar to the classical
separating conjunction: the existential quantifier is replaced by a supremum
and the conjunction by a multiplication. Note that the set over which the
supremum ranges is never empty.

The (guarded) quantitative magic wand is defined for a qualitative first
argument and a quantitative second argument. We minimise the value of the
second argument applied to the original heap joined with a heap that evaluates
the first argument to $1$, i.e., for qualitative expectation $\varphi$ and
expectation $Y$ we have:

$(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)(s,h)=\inf\left\\{\,Y(s,h^{\prime\prime})\,\mid\,\varphi(s,h^{\prime})=1,\leavevmode\nobreak\
h^{\prime\prime}=h\mathbin{{\star}}h^{\prime}\,\right\\}$

If the set is empty, the infimum evaluates to the greatest element of all
probabilities, which is $1$. Although it is also possible to allow
expectations in both arguments (cf. [5]), we restrict ourselves to the guarded
version of the magic wand. This restriction allows us to exploit the
superdistributivity of multiplication, i.e.,
$\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\cdot
Y)\geq(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\cdot(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)$.

######  Example 2.5.

To illustrate separating operations and lower bounding in QSL, we consider
$X=\left[{x\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{x\mapsto
y}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(0.5\cdot\left[{x\mapsto\,{-}\,}\right]))$,
$Y=0.5\cdot\left[{x\mapsto\,{-}\,}\right]$ and $Z=0.5\cdot\left[{x\mapsto
y}\right]$. Let us consider the semantics of $X$ in more detail. $X$ is non-
zero only for states that allocate exactly $x$. In this case, after changing
the value pointed to by $x$ to $y$, $0.5$ is returned if $x$ is still
allocated (which obviously holds). Thus, the combination of separating
multiplication and magic wand realises a change of value: First a pointer is
removed from the heap by using separating multiplication, and afterwards we
add it back with a different value using the magic wand. Note that
$\left[{x\mapsto y}\right]$ is qualitative, which is required for our version
of the magic wand. Then we have $X=Y$ and $Z\leq X$.

##  3 Programming Language and Operational Semantics

Our programming language is a concurrent extension of the heap-manipulating
and probabilistic guarded command language [5]. Our language features both
deterministic and probabilistic control flow, atomic regions, concurrent
threads operating on shared memory, variable-based assignments, and heap
manipulations. Although our language allows arbitrary shared memory, we will
later only be able to reason about shared memory in the heap. Conditional
choice without an else branch is considered syntactic sugar. Atomic regions
consist of programs without memory allocation or concurrency. However,
probabilistic choice is admitted. Programs that satisfy this restriction are
called _tame_.

The reason to restrict the program fragment within atomic regions is that non-
tame statements introduce non-determinism (as addresses to be allocated and
schedulings of concurrent programs are chosen non-deterministically), which
would increase the semantics’ complexity while providing only little benefit
(we refer to [1] regarding the handling of non-tame probabilistic programs in
atomic regions). If an atomic region loops with a certain probability $p$, we
instead transition to a non-terminating program with probability $p$.

######  Definition 3.1 (Concurrent Heap-Manipulating Probabilistic Guarded
Command Language).

The concurrent heap-manipulating probabilistic guarded command language chpGCL
is generated by the grammar

$\displaystyle C\leavevmode\nobreak\ \leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ $
$\displaystyle\;\downarrow\;$ (terminated program)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\textnormal{{diverge}}$ (non-terminating program)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
x\mathrel{\textnormal{{:=}}}e$ (assignment)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\left\\{\,{C}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C}\,\right\\}$
(prob. choice) $\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
{C}{\,;}\leavevmode\nobreak\ {C}$ (seq. composition)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\textnormal{{atomic}}\left\\{\,{C}\,\right\\}$ (atomic region)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C}\,\right\\}$
(conditional choice) $\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}$ (loop)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\left.C\;\middle\|\;C\right.$ (concurrency)
$\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
{x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{0},\dots,e_{n}\right)$
(allocation) $\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\mathtt{free}(e),$ (disposal) $\displaystyle|\leavevmode\nobreak\
\leavevmode\nobreak\ x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>}$
(lookup) $\displaystyle|\leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime}$ (mutation)

where $x$ is a variable,
$e,e^{\prime},e_{i}\colon\textsf{{Stacks}}\to\mathbb{Z}$ are arithmetic
expressions, $e_{p}\colon\textsf{{Stacks}}\to[0,1]$ is a probabilistic
arithmetic expression and $b\subseteq\textsf{{Stacks}}$ is a guard.

######  Example 3.2.

We consider as running example a little program with two threads synchronizing
over a randomised value:

$\displaystyle\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}-1\,;\,$
$\displaystyle\left.\begin{aligned}
&\quad\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}0}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}1}\,\right\\}\end{aligned}\;\middle\|\;\begin{aligned}
&y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}\,;\,\\\
&\textnormal{{while}}\left(\,{y=-1}\,\right)\left\\{\,{y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}}\,\right\\}\,;\,\end{aligned}\right.$

We first initialise our resource $r$ with some integer that stands for an
undefined value (here $-1$). The first thread now either assigns $0$ or $1$
with probability $0.5$ to $r$. As soon as $r$ has a new value, the second
thread receives this value and terminates as $r$ is not $-1$ any more.

We define the operational semantics of our programming language chpGCL in the
form of a _Markov Decision Process_ (MDP for short). An MDP allows the use of
both _non-determinism_ , which we need for interleaving multiple threads, and
_probabilities_ , which are used for encoding probabilistic program commands.
A transition between states is thus always annotated with two parameters: (1)
an action that is taken non-deterministically and (2) a probability to
transition to a state given the aforementioned action.

######  Definition 3.3 (Markov Decision Process).

A Markov Decision Process $M=(U,\text{Act},\mathbb{P})$ consists of a
countable set of states $U$, a mapping from states to enabled actions
$\text{Act}\colon U\to 2^{\text{A}}$ for a countable set of actions A, and a
transition probability function $\mathbb{P}\colon(U\times\text{A})\to
U\to[0,1]$ where for all $\sigma\in U$ and $a\in\text{Act}(\sigma)$ we require
$\sum_{\sigma^{\prime}\in U}\mathbb{P}(\sigma,a)(\sigma^{\prime})=1$. We also
use the shorthand notation $\sigma\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\ \sigma^{\prime}$ for
$\mathbb{P}(\sigma,a)(\sigma^{\prime})=p$ in case $p>0$.

We define the operational semantics of chpGCL as an MDP. A state in this MDP
consists of a chpGCL program to be executed and a program state $(s,h)$. The
meaning of basic commands, i.e., assignments, heap mutations, heap lookups,
memory allocation and disposal, is defined by the inference rules shown in
Figure 2. An action is enabled if and only if an inference rule for this
action exists. We use an abort keyword to indicate that a memory access error
happened and terminate at this state. We consider aborted runs as undesired
runs. The condition $\sum_{\sigma^{\prime}\in
U}\mathbb{P}(\sigma,a)(\sigma^{\prime})=1$ holds for all states in a chpGCL
program. States with program $\;\downarrow\;$ or abort have no enabled
actions, thus the condition holds trivially for all enabled actions $a$; non-
probabilistic programs only have actions with trivial distributions; states
with probabilistic choice only have a single action with a biased coin-flip
distribution; and other programs are composed of these.

$\leavevmode\nobreak\ \xrightarrow[s]{p}\leavevmode\nobreak\ $ ASSIGN
$x\mathrel{\textnormal{{:=}}}e,(s,h)\leavevmode\nobreak\
\xrightarrow[\text{assign}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s\left[{x}\coloneqq{e(s)}\right],h)$

$e(s)\in\textsf{{dom}}\left({h}\right)$ LOOKUP
$x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{lookup}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s\left[{x}\coloneqq{h(e(s))}\right],h)$

$e(s)\not\in\textsf{{dom}}\left({h}\right)$ LOOKUP-ABT
$x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{lookup-abt}]{1}\leavevmode\nobreak\ \textnormal{{abort}}$

$e(s)\in\textsf{{dom}}\left({h}\right)$ MUT
$\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{mutation}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h\left[{e(s)}\coloneqq{e^{\prime}(s)}\right])$

$e(s)\not\in\textsf{{dom}}\left({h}\right)$ MUT-ABT
$\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{mutation-abt}]{1}\leavevmode\nobreak\ \textnormal{{abort}}$

$e(s)\in\textsf{{dom}}\left({h}\right)$ $h^{\prime}=h\setminus\\{e(s)\mapsto
h(e(s))\\}$ FREE $\mathtt{free}(e),(s,h)\leavevmode\nobreak\
\xrightarrow[\text{free}]{1}\leavevmode\nobreak\
\;\downarrow\;,(s,h^{\prime})$

$e(s)\not\in\textsf{{dom}}\left({h}\right)$ FREE-ABT
$\mathtt{free}(e),(s,h)\leavevmode\nobreak\ \xrightarrow[\text{free-
abt}]{1}\leavevmode\nobreak\ \textnormal{{abort}}$

$\ell+0,\dots\ell+n\in\mathbb{N}_{>0}\setminus\textsf{{dom}}\left({h}\right)$
$e_{0}(s)=v_{0},\dots,e_{n}(s)=v_{n}$
$h^{\prime}=h\mathbin{{\star}}\\{\ell+0\mapsto
v_{1}\\}\mathbin{{\star}}\dots\mathbin{{\star}}\\{\ell+n\mapsto v_{n}\\}$
ALLOC
${x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{0},\dots,e_{n}\right),(s,h)\leavevmode\nobreak\
\xrightarrow[\text{alloc-}\ell]{1}\leavevmode\nobreak\
\;\downarrow\;,(s\left[{x}\coloneqq{\ell}\right],h^{\prime})$

Figure 2: Operational semantics of basic commands in chpGCL

Control-flow statements include while loops, conditional choice, sequential
composition and probabilistic choice, and we define their operational
semantics in Figure 3. For the sake of brevity, we do not include a command to
sample from a distribution.

$C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})$ SEQ ${C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\ {C_{2}},(s^{\prime},h^{\prime})$

$C_{2},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{2}^{\prime},(s^{\prime},h^{\prime})$ SEQ-END
${\;\downarrow\;}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\ C_{2}^{\prime},(s^{\prime},h^{\prime})$

$C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$ SEQ-ABT ${C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$

$C_{2},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$ SEQ-END-ABT ${\;\downarrow\;}{\,;}\leavevmode\nobreak\
{C_{2}},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$

$s\in b$ IF-T
$\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{if-t}]{1}\leavevmode\nobreak\ C_{1},(s,h)$

$s\not\in b$ IF-F
$\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{if-f}]{1}\leavevmode\nobreak\ C_{2},(s,h)$

$s\in b$ WHILE-T
$\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C_{1}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{loop-t}]{1}\leavevmode\nobreak\
{C_{1}}{\,;}\leavevmode\nobreak\
{\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C_{1}}\,\right\\}},(s,h)$

$s\not\in b$ WHILE-F
$\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C_{1}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{loop-f}]{1}\leavevmode\nobreak\ \;\downarrow\;,(s,h)$

$\leavevmode\nobreak\ \xrightarrow[p]{s}\leavevmode\nobreak\ $ DIV
$\textnormal{{diverge}},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{div}]{1}\leavevmode\nobreak\ \textnormal{{diverge}},(s,h)$

$e_{p}(s)=p$ PROB-L
$\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{prob}]{p}\leavevmode\nobreak\ C_{1},(s,h)$

$e_{p}(s)=p$ PROB-R
$\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{prob}]{1-p}\leavevmode\nobreak\ C_{2},(s,h)$

Figure 3: Operational semantics of non-concurrent control-flow operations in
chpGCL

The remaining control-flow statements handle concurrency, i.e., the concurrent
execution of two threads and the atomic execution of regions. An atomic region
may only terminate with a certain probability. The notation
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots$ denotes that program $C$ does not
terminate on state $(s,h)$ with probability $p$. As mentioned before, we will
only allow tame programs inside atomic regions. A tame program does not
require any (scheduling) actions since its Markov model is fully
probabilistic. To formally define the syntax used in the inference rules for
atomic regions, we first need to introduce _schedulers_ , which are used to
resolve non-determinism in an MDP. There are various classes of schedulers,
and indeed we will later allow the use of different classes. However, we do
require that all schedulers are deterministic and may have a history. This
especially rules out any randomised scheduler, which would be an interesting
topic, but is out of scope for the results presented here. Our schedulers use
finite sequences of MDP states as histories.

######  Definition 3.4 (Scheduler).

A scheduler is a mapping $\mathfrak{s}\colon U^{+}\to\text{A}$ from histories
of states to enabled actions, i.e.,
$\mathfrak{s}(\sigma_{1}\dots\sigma_{n})\in\text{Act}(\sigma_{n})$. We denote
the set of all schedulers by $\mathbb{S}$.

For final states $\sigma^{\prime}$ (i.e., with program $\;\downarrow\;$ or
abort) and an MDP $(U,\text{Act},\mathbb{P})$, we define

$\displaystyle\text{reach}(n,\sigma_{1},\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\
=$ $\displaystyle\leavevmode\nobreak\
\sum\bigg{[}\prod_{i=1}^{m-1}\leavevmode\nobreak\ \leavevmode\nobreak\
\mathbb{P}(\sigma_{i},\mathfrak{s}(\sigma_{1}\dots\sigma_{i}))(\sigma_{i+1})$
$\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\;\sigma_{1}\dots\sigma_{m}\in
U^{m},\sigma_{m}=\sigma^{\prime},m\leq n\bigg{]}\leavevmode\nobreak\ ,$ (1)
$\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\sigma^{\prime}\quad\text{iff}$ $\displaystyle\quad p\leavevmode\nobreak\
=\leavevmode\nobreak\
\lim_{n\rightarrow\infty}\text{reach}(n,\sigma,\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\
,$ (2) $\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{1-p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\dots\quad\text{iff}$ $\displaystyle\quad p\leavevmode\nobreak\
=\leavevmode\nobreak\ \sum_{\sigma^{\prime}\leavevmode\nobreak\
\text{final}}\lim_{n\rightarrow\infty}\text{reach}(n,\sigma,\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\
.$ (3)

For a function $f$ and a predicate $b$, we write $[f(x)\mid x\in b]$ for the
bag consisting of the values $f(x)$ with $x\in b$. We use notation (1) to
calculate the probability to reach the final state $\sigma^{\prime}$ from
$\sigma_{1}$ in at most $n$ steps w.r.t $\mathfrak{s}$. We unroll the MDP here
into the Markov Chain induced by $\mathfrak{s}$ after at most $n$ steps (cf.
[2, Definition 10.92]). With notation (2), we define the reachability
probability of a final state and with notation (3), we define the probability
of non-termination. We avoid reasoning about uncountable sets of paths in case
of non-termination by taking the probability to not reach a final state, i.e.,
a state with program $\;\downarrow\;$ or abort. A scheduler $\mathfrak{s}$ is
unique if for every state $\sigma\in U$ there is at most one enabled action
$\mathfrak{s}$ can map to, i.e., $|\text{Act}(\sigma)|\leq 1$. In that case,
we usually omit the corresponding transition label.

$C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \;\downarrow\;,(s^{\prime},h^{\prime})$ $C$ is
tame ATOM-END
$\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$

$C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \textnormal{{abort}}$ $C$ is tame ATOM-ABT
$\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\ \textnormal{{abort}}$

$C,(s,h)\leavevmode\nobreak\ \xrightarrow[]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots$ $C$ is tame ATOM-LOOP
$\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[\text{atomic}]{p}\leavevmode\nobreak\
\textnormal{{diverge}},(s,h)$

$C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{1}^{\prime},(s^{\prime},h^{\prime})$ CON-L
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C1,a]{p}\leavevmode\nobreak\
\left.C_{1}^{\prime}\;\middle\|\;C_{2}\right.,(s^{\prime},h^{\prime})$

$C_{2},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{2}^{\prime},(s^{\prime},h^{\prime})$ CON-R
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C2,a]{p}\leavevmode\nobreak\
\left.C_{1}\;\middle\|\;C_{2}^{\prime}\right.,(s^{\prime},h^{\prime})$

$C_{1},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$ CON-L-ABT
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C1,a]{p}\leavevmode\nobreak\ \textnormal{{abort}}$

$C_{2},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
\textnormal{{abort}}$ CON-R-ABT
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[C2,a]{p}\leavevmode\nobreak\ \textnormal{{abort}}$

$\leavevmode\nobreak\ \xrightarrow[s]{p}\leavevmode\nobreak\ $ CON-END
$\left.\;\downarrow\;\;\middle\|\;\;\downarrow\;\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[\text{con-end}]{1}\leavevmode\nobreak\ \;\downarrow\;,(s,h)$

Figure 4: Operational semantics of concurrent control-flow operations in
chpGCL

To reason about the operational semantics using QSL, we use weakest _liberal_
preexpectations [5, 37], which take the greatest lower bound of the expected
value with respect to a postexpectation together with the probability of non-
termination for all schedulers that we want to consider. We allow subsets of
schedulers $S\subseteq\mathbb{S}$ in order to apply fairness conditions.
Later, we only consider the complete set of schedulers. In that case, we omit
the superscript from the function wlp, which is defined in the following.

######  Definition 3.5 (Weakest Liberal Preexpectation).

For a program $C$ and an expectation $X$, we define the weakest liberal
preexpectation with respect to a set of schedulers $\emptyset\neq
S\subseteq\mathbb{S}$ as

$\displaystyle\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(X\right)(s,h)\quad=$
$\displaystyle\quad\inf\bigg{\\{}\sum\left[p\cdot X(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]+p_{div}$
$\displaystyle\quad\qquad\bigg{|}\leavevmode\nobreak\ \mathfrak{s}\in
S\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\ \xrightarrow[\mathfrak{s}]{p_{div}}{}^{*}\hskip
3.01125pt\leavevmode\nobreak\ \dots\bigg{\\}}\leavevmode\nobreak\ .$

######  Example 3.6.

For program $C$ in Example 3.2, we evaluate (without proof)
$\textsf{{wlp}}\llbracket
C\rrbracket\left(\left[{y=0}\right]\right)=\textsf{{wlp}}^{\mathbb{S}}\llbracket
C\rrbracket\left(\left[{y=0}\right]\right)=0.5\mathbin{{\star}}\left[{r\mapsto\,{-}\,}\right]$.
That is, if $r$ is allocated, then the likelihood of $C$ terminating without
aborting in a state in which $y$ equals $0$ is 0.5, and zero otherwise. We
will prove that this is a lower bound in Example 4.6.

##  4 Weakest Safe Liberal Preexpectations

For sequential probabilistic programs, a backwards expectation transformer can
be defined to compute wlp [5]. This is not feasible for concurrent programs
due to the non-locality of shared memory. Instead, we drop exact computation
in our approach and reason about lower bounds of wlp by using inference rules
similar to Hoare triples. To support shared memory, we furthermore introduce a
modified version of wlp – the weakest _resource-safe_ liberal preexpectation.
The general idea as inspired by [52] is to prove that the shared memory is
invariant with respect to a qualitative expectation, which we call a _resource
invariant_. In other words, the shared memory is proven to be _safe_ with
respect to the resource invariant. We archive this by enforcing that at every
point in the program’s execution (except for executions in atom regions), some
part of the heap is satisfied by the resource invariant. In Example 4.6 we use
the resource invariant $\max\left\\{\,{\left[{r\mapsto
0}\right]},\>{\left[{r\mapsto-1}\right]}\,\right\\}$ to prove the lower bound
from Example 3.6. We enforce that the program states do not include the shared
memory any more, the transitions however are taken with any possible shared
memory.

######  Definition 4.1 (Weakest Resource-Safe Liberal Preexpectation).

We first consider the expectation after one step with respect to a mapping
from programs to expectations, that is, for a program $C$ and a mapping
$t\colon\textnormal{{{chpGCL}}}\to\mathbb{E}_{\leq 1}$, we define

$\displaystyle\quad\inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}\leavevmode\nobreak\ .$

We define the weakest resource-safe liberal preexpectation after $n$ steps for
a program $C$, a postexpectation $X$ and a (qualitative) resource invariant
$\xi$ as

$\displaystyle\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)=\begin{cases}1&\text{if}\leavevmode\nobreak\
n=0\\\ X&\text{if}\leavevmode\nobreak\ n\neq 0\leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ C=\;\downarrow\\\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\step{C}{\lambda
C^{\prime}.\leavevmode\nobreak\ \textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(X\mid\xi\right)\mathbin{{\star}}\xi}&\text{otherwise}.\end{cases}$

Finally, we define the weakest resource-safe liberal preexpectation for
arbitrarily many steps as

$\displaystyle\textsf{{wrlp}}\llbracket
C\rrbracket\left(X\mid\xi\right)=\lim_{n\rightarrow\infty}\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\leavevmode\nobreak\ .$

An important observation is that for the special resource invariant
$\left[{\textsf{{{emp}}}}\right]$, wlp and wrlp coincide (cf. Theorem
B.23).This enables us to reason about lower bounds for probabilities of
qualitative preconditions (and in general lower bounds for the expected value
of one-bounded random variables). When reasoning about such probabilities, we
first express a property for which we aim to prove a lower bound on wlp,
afterwards we can transform it into wrlp with the resource invariant
$\left[{\textsf{{{emp}}}}\right]$ and use special rules to enrich the resource
invariant with more information. The resource invariant should always cover
all possible states that the shared memory may be in at any time during the
program’s execution. It is fine if the resource invariant is violated during
executions of atomic regions, since we only care about safeness during
executions with inferences between threads.

We mention that wrlp is heavily inspired by [52]. We formalise the connection
between Vafeiadis’ Concurrent Separation Logic and our weakest resource-safe
liberal preexpectation below. In [52] a judgement is defined by a safe
predicate that is similar to how we defined wrlp. [Safe Judgements [52]] The
predicate $\text{safe}_{n}(C,s,h,\xi,\varphi)$ holds for qualitative $\varphi$
and $\xi$ and non-probabilistic program $C$ if and only if

  1. 1.

if $n=0$, then it holds always; and

  2. 2.

if $n>0$ and $C=\;\downarrow\;$, then $\varphi(s,h)=1$; and

  3. 3.

if $n>0$ and for all $h_{\xi}$ and $h_{F}$ with $\xi(s,h_{\xi})=1$ and
$h\mathrel{\bot}h_{\xi}\mathrel{\bot}h_{F}$, then for all enabled actions
$a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{\xi}\mathbin{{\star}}h_{F}))$ we do
not have
$C,(s,h\mathbin{{\star}}h_{\xi}\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ \textnormal{{abort}}$; and

  4. 4.

if $n>0$ and for all $h_{\xi},h_{F},C^{\prime},s$ and $h$, with
$\xi(s,h_{\xi})=1$, and $h\mathrel{\bot}h_{\xi}\mathrel{\bot}h_{F}$, and
$C,(s,h\mathbin{{\star}}h_{\xi}\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\ C^{\prime},(s^{\prime},h^{\prime})$,
then there exists $h^{\prime\prime}$ and $h^{\prime}_{\xi}$ such that
$h^{\prime}=h^{\prime\prime}\mathbin{{\star}}h^{\prime}_{\xi}\mathbin{{\star}}h_{F}$
and $\xi(s^{\prime},h_{\xi}^{\prime})=1$ and
$\text{safe}_{n-1}(C^{\prime},s^{\prime},h^{\prime\prime},\xi,\varphi)$.

For qualitative $\varphi$, $\psi$ and $\xi$, we say that
$\xi\models\\{\psi\\}\;C\;\\{\varphi\\}$ holds if and only if for all
stack/heap pairs $s,h$ the statement $\psi(s,h)=1\Rightarrow\forall
n\in\mathbb{N}.\leavevmode\nobreak\ \text{safe}_{n}(C,s,h,\xi,\varphi)$ holds.
A program $C$ is framing enabled222Indeed every non-probabilistic chpGCL
program is framing enabled (cf. Theorem D.4). if we can always extend the heap
without changing the behaviour of $C$. [Framing Enabledness] A non-
probabilistic program $C$ is framing enabled if for all heaps $h_{F}$ with
$h\mathrel{\bot}h_{F}$ and all enabled actions
$a\in\text{Act}(C,(s,h\mathbin{{\star}}h_{F}))$, it holds: if
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})$, then also
$C,(s,h\mathbin{{\star}}h_{F})\leavevmode\nobreak\
\xrightarrow[a]{1}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime}\mathbin{{\star}}h_{F})$. The next theorem
states that wrlp is a conservative extension of safe. [Conservative Extension
of Concurrent Separation Logic] For a framing-enabled non-probabilistic
program $C$ and qualitative expectations $\varphi$, $\psi$ and $\xi$, we have

$\varphi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(\psi\mid\xi\right)\quad\text{iff}\quad\xi\models\\{\varphi\\}\leavevmode\nobreak\
C\leavevmode\nobreak\ \\{\psi\\}\leavevmode\nobreak\ .$

######  Proof 4.4.

See Appendix B.

term $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)$

$Y\leq\sup_{v\in\mathbb{Z}}\left[{e\mapsto
v}\right]\mathbin{{\star}}(\left[{e\mapsto
v}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\left[{x}\coloneqq{v}\right])$
look $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
x\mathrel{\textnormal{{:=}}}\texttt{<}\,e\,\texttt{>}\rrbracket\left(X\mid\xi\right)$

$Y\leq\inf_{v\in\mathbb{Z}}\left[{v\mapsto
e_{1},\dots,e_{n}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\left[{x}\coloneqq{v}\right]$
alloc $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket{x}\mathrel{\textnormal{{:=}}}\mathtt{new}\left(e_{1},\dots,e_{n}\right)\rrbracket\left(X\mid\xi\right)$

$Y\leq X\left[{x}\coloneqq{e}\right]$ assign $Y\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
x\mathrel{\textnormal{{:=}}}e\rrbracket\left(X\mid\xi\right)$

$Y\leq\left[{e\mapsto\,{-}\,}\right]\mathbin{{\star}}(\left[{e\mapsto
e^{\prime}}\right]\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)$
mut $Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\texttt{<}\,e\,\texttt{>}\mathrel{\textnormal{{:=}}}e^{\prime}\rrbracket\left(X\mid\xi\right)$

$Y\leq X\mathbin{{\star}}\left[{x\mapsto\,{-}\,}\right]$ disp
$Y\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\mathtt{free}(x)\rrbracket\left(X\mid\xi\right)$

Figure 5: Proof rules for wrlp for basic commands

We define wrlp inductively by means of a number of inference rules. We do not
use classic Hoare triples due to difficulties arising when interpreting a wrlp
statement forward. These difficulties are due to Jones’s counterexample [28,
p. 135]: Given the constant preexpectation $0.5$ and the program
$C\colon\left\\{\,{x\mathrel{\textnormal{{:=}}}0}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{x\mathrel{\textnormal{{:=}}}1}\,\right\\}$,
what is the postexpectation? Two possible answers are
$0.5=\textsf{{wlp}}\llbracket C\rrbracket\left(\left[{x=0}\right]\right)$ and
$0.5=\textsf{{wlp}}\llbracket C\rrbracket\left(\left[{x=1}\right]\right)$, but
a combination of both is not possible. For this reason, we highlight the
backwards interpretation of our judgements by writing them as
$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$, where $X$ is a (lower bound for the weakest
liberal) preexpectation, $C$ is the program, $Y$ is the postexpectation and
$\xi$ is the resource invariant.

For basic commands, as shown in Figure 5, we can just re-use the QSL proof
rules for weakest liberal preexpectations (wlp) of non-concurrent programs, as
given in [5]. However, for wrlp these proof rules only allow lower bounding
the preexpectation since we do not want to reason about the resource invariant
if not necessary.

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ $Y\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Z\mid\xi\right)$ seq $X\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket{C_{1}}{\,;}\leavevmode\nobreak\
{C_{2}}\rrbracket\left(Z\mid\xi\right)$

$X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ $X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$ if $\left[{b}\right]\cdot
X_{1}+\left[{\neg b}\right]\cdot X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{if}}\,\left(\,{b}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

$I\leq\left[{b}\right]\cdot X+\left[{\neg b}\right]\cdot Y$
$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(I\mid\xi\right)$ while $I\leavevmode\nobreak\
\leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{while}}\left(\,{b}\,\right)\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

div $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{diverge}}\rrbracket\left(Y\mid\xi\right)$

$X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y\mid\xi\right)$ $X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y\mid\xi\right)$ p-choice $e_{p}\cdot
X_{1}+(1-e_{p})\cdot X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,e_{p}\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$
atomic $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\textnormal{{atomic}}\left\\{\,{C}\,\right\\}\rrbracket\left(Y\mid\xi\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\mathbin{{\star}}\pi\right)$ share
$X\mathbin{{\star}}\pi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\pi\mid\xi\right)$

$X_{1}\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{1}\rrbracket\left(Y_{1}\mid\xi\right)$ $X_{2}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C_{2}\rrbracket\left(Y_{2}\mid\xi\right)$ $\forall
i\in\\{1,2\\}\leavevmode\nobreak\
\text{Write}(C_{i})\cap\text{Vars}\,(C_{3-i},Y_{3-i},\xi)=\emptyset$ concur
$X_{1}\mathbin{{\star}}X_{2}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket\left.C_{1}\;\middle\|\;C_{2}\right.\rrbracket\left(Y_{1}\mathbin{{\star}}Y_{2}\mid\xi\right)$

Figure 6: Proof rules for wrlp for control-flow commands

For commands handling control flow, as shown in Figure 6, we use mostly
standard rules. Atomic regions regain access to the resource invariant. The
share rule allows us to enrich the resource invariant. The rule for
concurrency enforces that only local variables or read-only variables are used
in each thread. One could as well allow shared variables that are owned by the
resource invariant. However, for the sake of brevity we do not include this
here.

$X^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(X\right)$
$Y^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y\right)$ $C$ is
AST w.r.t. $S$ $a\in\mathbb{R}_{\geq 0}$ superlin $a\cdot
X^{\prime}+Y^{\prime}\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(a\cdot
X+Y\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\left[{\textsf{{{emp}}}}\right]\right)$ wlp-wrlp
$X\leq\textsf{{wlp}}^{S}\llbracket C\rrbracket\left(Y\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$
$\text{Write}(C)\cap\text{Vars}\,(Z)=\emptyset$ frame
$X\mathbin{{\star}}Z\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mathbin{{\star}}Z\mid\xi\right)$

$X\mathbin{{\star}}\xi\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$
$C$ is a terminating atom atom $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mid\xi\right)$

$X\leq X^{\prime}$ $X^{\prime}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y^{\prime}\mid\xi\right)$
$Y^{\prime}\leq Y$ monotonic $X\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(Y\mid\xi\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ max
$\max\left\\{\,{X},\>{X^{\prime}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\max\left\\{\,{Y},\>{Y^{\prime}}\,\right\\}\mid\xi\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ $\xi$ precise min
$\min\left\\{\,{X},\>{X^{\prime}}\,\right\\}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\min\left\\{\,{Y},\>{Y^{\prime}}\,\right\\}\mid\xi\right)$

$X\leavevmode\nobreak\ \leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$ $X^{\prime}\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y^{\prime}\mid\xi\right)$ $\xi$ precise
$\text{Write}(C)\cap\text{Vars}\,(e)=\emptyset$ convex $e\cdot X+(1-e)\cdot
X^{\prime}\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\textsf{{wrlp}}\llbracket C\rrbracket\left(e\cdot Y+(1-E)\cdot
Y^{\prime}\mid\xi\right)$

Figure 7: Auxiliary proof rules for wrlp

We also introduce several proof rules that make reasoning easier, see Figure
7. A program is _almost surely terminating_ with respect to a set of
schedulers if the program terminates with probability one for every initial
state and every scheduler in this set. Even though there is a plethora of work
on almost-sure termination for (sequential) probabilistic programs (cf. [24]
for an overview), techniques for checking almost-sure termination in a
concurrent setting are sparse [21, 22, 35, 51]. Here, interpreting
probabilistic choice as non-determinism and proving sure termination instead
using techniques such as [15, 48] is an alternative.

The first rule in Figure 7 uses superlinearity for wlp to split a given
postexpectation into a sum of smaller postexpectations, for which proving a
lower bound on the preexpectation might be easier. Here we use addition
instead of maximum since addition is usually more precise. We only allow the
use of superlinearity for wlp (and not for wrlp) because we need a restricted
set of schedulers to enforce fairness conditions. Fairness conditions are
required to reason about termination for concurrent programs with some sort of
blocking behaviour. We are then able to transform wlp into wrlp by using the
wlp-wrlp rule. Whether wrlp can also be defined with fairness conditions in
mind and thus applying superlinearity directly on wrlp, is an open question.
The frame rule is of central importance to the Separation Logic approach, as
it supports local reasoning about only the relevant part of the heap [45]. The
atom rule can be used similarly to the rule for atomic regions. Monotonicity
is the quantitative version of the rule of consequence and is used to reduce
and increase the post- and preexpectation respectively. The max, min and
convex rules eliminate max, min and convex sum operations, respectively. The
min and convex rule require preciseness of the resource invariant – similarly
to how [52] required preciseness for the conjunction rule. An expectation is
_precise_ if for any stack there is at most one heap for which the expectation
is not zero. For the min rule, this is not surprising as the minimum behaves
like conjunction in case of qualitative expectations. Requiring preciseness
also for the convex rule is due to the missing superlinearity of the
separating multiplication for non-precise expectations. [Soundness of proof
rules] For every proof rule in Figures 5, 6 and 7 it holds that if their
premises hold, the conclusion holds as well.

######  Proof 4.5.

See Appendix E.

######  Example 4.6.

We are now able to establish the lower bound computed in Example 3.6 using the
proof rules. Instead of constructing a proof tree by composing inference
rules, we annotate program locations with their respective pre- and
postexpectations. The interpretation is standard; for preexpectation $X$,
postexpectation $Y$, resource invariant $\xi$ and program $C$:

$\begin{aligned} &\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{X\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\ &C\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{Y\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}\qquad\text{iff}\qquad X\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(Y\mid\xi\right)$

Proofs in this style should only be read backwards from bottom to top. They
will not include applications of the proof rules for atomic programs and of
the share rule as this may lead to incorrect interpretations. For our example,
we use the resource invariant $\xi=\max\left\\{\,{\left[{r\mapsto
0}\right]},\>{\left[{r\mapsto-1}\right]}\,\right\\}$, which we guessed by
collecting all possible values stored in location $r$ during executions
yielding our postexpectation. We assume that the memory of the initial heap
$h$ only contains a single location $r$ with value $-1$. This assumption is
reflected by the resource invariant and will only allow us to reason about
executions with such an initial heap. The other possible value for the
location $r$ is $0$, since the left program may mutate the heap. Indeed, there
are also executions where the value of location $r$ is $1$. For these, the
program only terminates in states violating the postexpectation
$\left[{y=0}\right]$. We can further show:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{0.5\mathbin{{\star}}1\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$
$\displaystyle\left.\begin{aligned} &\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\ \vphantom{G^{\prime}}{0.5\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}0}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{\texttt{<}\,r\,\texttt{>}\mathrel{\textnormal{{:=}}}1}\,\right\\}\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}\quad\middle\|\quad\begin{aligned}
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}\,;\,\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\max\left\\{\,{\left[{y=0}\right]},\>{\left[{y=-1}\right]}\,\right\\}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}\\\
&\textnormal{{while}}\left(\,{y=-1}\,\right)\left\\{\,{y\mathrel{\textnormal{{:=}}}\texttt{<}\,r\,\texttt{>}}\,\right\\}\,;\,\\\
&\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{y=0}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\xi}\end{aligned}\right.$ $\displaystyle\fatslash\leavevmode\nobreak\
\leavevmode\nobreak\
\vphantom{G^{\prime}}{1\mathbin{{\star}}\left[{y=0}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi}$

To handle concurrency, we separate our postexpectation into the expectation
$1$ for the left program and the expectation $\left[{y=0}\right]$ for the
right program. The left program includes a probabilistic choice, for which we
use the atom rule to infer that the preexpectation is $1$ in the left branch
of the probabilistic choice, as the resource invariant allows mutating the
value of location $r$ to $1$ and the resource invariant can be re-established
since we can lower bound all possible values for the location $r$ that are not
$-1$ or $0$ to zero. Moreover, we lower bound the right branch of the
probabilistic choice by zero, because zero is a lower bound of any
expectation. The right program iterates until the value of location $r$ has
been mutated. Our resource invariant contains all possible values that the
program can expect here. For the loop invariant, we connect all possible
values of $y$ using a disjunction over $0$ and $-1$, as we disregard
executions where $y=1$. Lastly, we can apply the loop invariant to the lookup
of $r$ and since this matches our resource invariant, the resulting
preexpectation is one.

Thus, we have established that $0.5\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\left[{y=0}\right]\mid\xi\right)$. Using the share rule we
can further infer that $0.5\mathbin{{\star}}\xi\leavevmode\nobreak\
\leq\leavevmode\nobreak\ \textsf{{wrlp}}\llbracket
C\rrbracket\left(\left[{y=0}\right]\mathbin{{\star}}\xi\mid\left[{\textsf{{{emp}}}}\right]\right)$.
Lastly, we can clean up the statement using monotonicity and the wlp-wrlp rule
to obtain $0.5\mathbin{{\star}}\xi\leq\textsf{{wlp}}\llbracket
C\rrbracket\left(\left[{y=0}\right]\right)$. For details on the probabilistic
choice and the loop invariant, we refer to Section F.1.

##  5 Example: A Producer, a Consumer and a Lossy Channel

A producer-consumer system is often used when presenting verification
techniques for concurrent programs. We continue this tradition, extending this
example by probabilistic elements, see Figure 8. Video and audio streaming is
an example for such a system, where data losses are acceptable if they do not
exceed a certain limit. Moreover, by enriching the resource invariant with a
predicate defining an appropriate data structure, this example can be used as
a template to reason about systems communicating using a shared data
structure. We consider a producer that randomly generates data ($1$ or $2$)
and stores it in an array of size $k$ indexed by $z_{1}$. The data has to be
transferred to a consumer. However, the consumer does not have direct access
to the array maintained by the producer. Instead a third party, the lossy
channel, transfers data from the array maintained by the producer to a
different $k$-sized array that is indexed by $z_{2}$, and that can be accessed
by the consumer. However, the channel is not reliable. With a probability of
$1-p$, it loses a value and instead stores invalid data (encoded as $-1$) at
the respective array position. The consumer discards invalid data and counts
in $l$ how many valid elements it received until all array elements have been
attempted to be transmitted once. For the sake of brevity, we leave out the
allocation of the array index $z_{1}$ and $z_{2}$. Instead, we assume already
allocated arrays as input.

$\displaystyle l\mathrel{\textnormal{{:=}}}0\,;\,$ $\displaystyle
y_{1},y_{2},y_{3}\mathrel{\textnormal{{:=}}}k\,;\,$
$\displaystyle\left.\begin{aligned} &\textnormal{{while}}\left(\,{y_{1}\geq
0}\,\right)\left\\{\right.\\\
&\quad\left\\{\,{x_{1}\mathrel{\textnormal{{:=}}}1}\,\right\\}\mathrel{\left[\,0.5\,\right]}\left\\{\,{x_{1}\mathrel{\textnormal{{:=}}}2}\,\right\\}\,;\,\\\
&\quad\texttt{<}\,z_{1}+y_{1}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{1}\,;\,\\\
&\quad y_{1}\mathrel{\textnormal{{:=}}}y_{1}-1\\\
&\\}\end{aligned}\quad\middle\|\quad\left.\begin{aligned} &\\\\[-10.00002pt]
&\textnormal{{while}}\left(\,{y_{2}\geq 0}\,\right)\left\\{\right.\\\ &\quad
x_{2}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{1}+y_{2}\,\texttt{>}\,;\,\\\
&\quad\textnormal{{if}}\,\left(\,{x_{2}\neq 0}\,\right)\,\\{\\\
&\quad\quad\quad\\{\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}x_{2}\\}\\\
&\quad\quad\mathrel{\left[\,p\,\right]}\\\
&\quad\quad\quad\\{\texttt{<}\,z_{2}+y_{2}\,\texttt{>}\mathrel{\textnormal{{:=}}}-1\\}\,;\,\\\
&\quad\quad y_{2}\mathrel{\textnormal{{:=}}}y_{2}-1\\\ &\quad\\}\\\ &\\}\\\
&\\\\[-10.00002pt] \end{aligned}\quad\middle\|\quad\begin{aligned}
&\textnormal{{while}}\left(\,{y_{3}\geq 0}\,\right)\left\\{\right.\\\ &\quad
x_{3}\mathrel{\textnormal{{:=}}}\texttt{<}\,z_{2}+y_{3}\,\texttt{>}\,;\,\\\
&\quad\textnormal{{if}}\,\left(\,{x_{3}\neq 0}\,\right)\,\\{\\\
&\quad\quad\textnormal{{if}}\,\left(\,{x_{3}\neq-1}\,\right)\,\\{l\mathrel{\textnormal{{:=}}}l+1\\}\,;\,\\\
&\quad\quad y_{3}\mathrel{\textnormal{{:=}}}y_{3}-1\\\ &\quad\\}\\\
&\\}\end{aligned}\right.\right.$

Figure 8: A program consisting of the tree threads: a producer (left), a
consumer (right) and lossy channel (middle) for communication between the
prior threads.

We are interested in the probability that the data of a certain set of
locations has been successfully transmitted. If we additionally prove that the
program is almost surely terminating for some reasonable set of fair
schedulers, we can use superlinearity to prove lower bounds of probabilities
for even more complex postconditions, e.g. the probability that at least half
of the data have been transmitted successfully. Indeed, the program is almost
surely terminating under a fairness condition. We denote the set of locations
that we want to be successfully transmitted as $J$. For the resource
invariant, we use a big separating multiplication. Its semantics is as
expected: for a stack $s$, we connect all choices for the index variable with
regular separating multiplications. The resource invariant describes the
values we want to tolerate for every entry in both arrays. We join the
tolerated values by a disjunction (which is the maximum in our case). We now
use the resource invariant, parametrised on the set $J$ as

$\displaystyle\xi_{J}\quad=$
$\displaystyle\quad\left(\underset{i\in\\{0,\dots,k\\}}{\bigstar}\leavevmode\nobreak\
\leavevmode\nobreak\ \max\left\\{\,{\left[{z_{1}+i\mapsto
0}\right],\>\left[{z_{1}+i\mapsto 1}\right],\>\left[{z_{1}+i\mapsto
2}\right]}\,\right\\}\right)$ $\displaystyle\leavevmode\nobreak\
\mathbin{{\star}}\left(\underset{i\in\\{0,\dots,k\\}\cap
J}{\bigstar}\max\left\\{\,{\left[{z_{2}+i\mapsto
0}\right],\>\left[{z_{2}+i\mapsto 1}\right],\>\left[{z_{2}+i\mapsto
2}\right]}\,\right\\}\right)$ $\displaystyle\leavevmode\nobreak\
\mathbin{{\star}}\left(\underset{i\in\\{0,\dots,k\\}\setminus
J}{\bigstar}\max\left\\{\,{\left[{z_{2}+i\mapsto
0}\right],\>\left[{z_{2}+i\mapsto-1}\right]}\,\right\\}\right)\leavevmode\nobreak\
.$

Next, we can use the resource invariant to prove an invariant for each of the
three concurrent programs. The corresponding calculations can be found in
Section F.2. Let $C_{1}$ be the producer, $C_{2}$ the channel and $C_{3}$ the
consumer. For the producer program $C_{1}$ we can prove the invariant
$I_{1}=1$ with respect to the postexpectation $1$, for the channel $C_{2}$ we
can prove the invariant $I_{2}=\left[{0\leq y_{2}\leq k}\right]\cdot
p^{|\\{0,\dots,y_{2}\\}\cap J|}\cdot(1-p)^{|\\{0,\dots,y_{2}\\}\setminus
J|}+\left[{y_{2}<0}\right]$ with respect to the postexpectation $1$, and for
the consumer program $C_{3}$ we can prove the invariant $I_{3}=\left[{0\leq
y_{3}\leq
k}\right]\cdot\left[{l=|J\cap\\{0,\dots,y_{3}\\}|}\right]+\left[{y_{3}<0}\right]\cdot\left[{l=|J|}\right]$
with respect to the postexpectation $\left[{l=|J|}\right]$. Using all three
invariants, we can now lower bound the probability that $l=|J|$ holds after
the execution of the whole program $C$ in Figure 8:

$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{\left[{0\leq k}\right]\cdot p^{|\\{0,\dots,k\\}\cap
J|}\cdot(1-p)^{|\\{0,\dots,k\\}\setminus J|}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle l\mathrel{\textnormal{{:=}}}0\,;\,$ $\displaystyle
y_{1},y_{2},y_{3}\mathrel{\textnormal{{:=}}}k\,;\,$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{I_{1}\mathbin{{\star}}I_{2}\mathbin{{\star}}I_{3}\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$
$\displaystyle\left.C_{1}\;\middle\|\;\left.C_{2}\;\middle\|\;C_{3}\right.\right.$
$\displaystyle\fatslash\leavevmode\nobreak\ \leavevmode\nobreak\
\vphantom{G^{\prime}}{1\mathbin{{\star}}1\mathbin{{\star}}\left[{l=|J|}\right]\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\ \xi_{J}}$

Here, we first use the concurrency rule to place the postexpectation
$\left[{l=|J|}\right]$ into a separating context, thus covering all three
programs. The resulting preexpectation is indeed the separating multiplication
of the respective invariants. By applying the assignment rules to the first
two rows, we finally get the result for a lower bound of the weakest resource-
safe preexpectation with respect to resource invariant $\xi_{J}$. Thus, the
lower bound $(\left[{0\leq k}\right]\cdot p^{|\\{0,\dots,k\\}\cap
J|}\cdot(1-p)^{|\\{0,\dots,k\\}\setminus
J|})\mathbin{{\star}}\xi_{J}\leq\textsf{{wlp}}^{S}\llbracket
C\rrbracket\left(\left[{l=|J|}\right]\mathbin{{\star}}\xi_{J}\right)$ also
holds. We also show in Section F.2 how to prove the lower bound of more
difficult postexpectations using superlinearity.

##  6 Conclusion and Future Work

Using resource invariants from Concurrent Separation Logic [52] together with
quantitative reasoning from Quantitative Separation Logic [5] allows us to
reason about lower-bound probabilities of realizing a postcondition. In our
technique, probability mass is local to the thread. This insight gave rise to
only allow qualitative expectations in the model of the environment. By this,
the resource invariant only describes shared memory and lacks semantics for
global probability mass.

However, we may favour a probabilistic model of the environment – for example,
if the environment is a black box and only statistic information about its
possible behaviours is available. More research is required for logics
allowing probabilistic specifications in the environment description,
especially logics allowing quantitative resource invariants. Moreover, we are
only able to verify lower bounds due to the concurrent rule. We conjecture
that a logic for upper bounds requires different, unknown separation
connectives.

## References

  * [1] Christel Baier, Frank Ciesinski, and Markus Grosser.  PROBMELA: a modeling language for communicating probabilistic processes.  In MEMOCODE, pages 57–66. IEEE, 2004.
  * [2] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  The MIT Press, 2008.
  * [3] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin.  Probabilistic relational Hoare logics for computer-aided security proofs.  In MPC, pages 1–6. Springer, 2012.
  * [4] Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, and Thomas Noll.  Foundations for entailment checking in quantitative separation logic.  In ESOP, pages 57–84. Springer, 2022.
  * [5] Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.  Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.  Proc. ACM Program. Lang., 3(POPL):34:1–34:29, 2019.
  * [6] Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O’Hearn, Thomas Wies, and Hongseok Yang.  Shape analysis for composite data structures.  In CAV, pages 178–192. Springer, 2007.
  * [7] Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn.  Smallfoot: Modular automatic assertion checking with separation logic.  In FMCO, pages 115–137. Springer, 2005.
  * [8] Burton H. Bloom.  Space/time trade-offs in hash coding with allowable errors.  Commun. ACM, 13(7):422–426, 1970.
  * [9] Stephen Brookes and Peter W. O’Hearn.  Concurrent separation logic.  ACM SIGLOG News, 3(3):47–65, 2016.
  * [10] Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang.  Compositional shape analysis by means of bi-abduction.  J. ACM, 58(6):26:1–26:66, 2011.
  * [11] Michael Carbin, Sasa Misailovic, and Martin C. Rinard.  Verifying quantitative reliability for programs that execute on unreliable hardware.  Commun. ACM, 59(8):83–91, 2016.
  * [12] Edsger W. Dijkstra.  A Discipline of Programming.  Prentice-Hall, 1976.
  * [13] Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang.  Views: Compositional reasoning for concurrent programs.  In POPL, pages 287–300. ACM, 2013.
  * [14] Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis.  Concurrent abstract predicates.  In ECOOP, pages 504–528. Springer, 2010.
  * [15] Emanuele D’Osualdo, Julian Sutherland, Azadeh Farzan, and Philippa Gardner.  TaDA live: Compositional reasoning for termination of fine-grained concurrent programs.  ACM Trans. Program. Lang. Syst., 43(4), 2021.
  * [16] Keir Fraser.  Practical lock-freedom.  Technical Report UCAM-CL-TR-579, University of Cambridge, Computer Laboratory, 2004.
  * [17] Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang.  Reasoning about optimistic concurrency using a program logic for history.  In CONCUR, pages 388–402. Springer, 2010.
  * [18] Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani.  Probabilistic programming.  In FOSE, pages 167–181. ACM, 2014.
  * [19] Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv.  Thread-modular shape analysis.  In PLDI, pages 266–277. ACM, 2007.
  * [20] Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver.  Operational versus weakest pre-expectation semantics for the probabilistic guarded command language.  Performance Evaluation, 73:110–132, 2014.
  * [21] Sergiu Hart and Micha Sharir.  Concurrent probabilistic programs, or: How to schedule if you must.  SIAM J. Comput., 14(4):991–1012, 1985.
  * [22] Sergiu Hart, Micha Sharir, and Amir Pnueli.  Termination of probabilistic concurrent programs.  ACM Trans. Program. Lang. Syst., 5(3):356–380, 1983.
  * [23] Max P. L. Haslbeck.  Verified Quantitative Analysis of Imperative Algorithms.  PhD thesis, Technical University of Munich, Germany, 2021.
  * [24] Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady.  Modular verification for almost-sure termination of probabilistic programs.  Proc. ACM Program. Lang., 3(OOPSLA):129:1–129:29, 2019.
  * [25] Samin S. Ishtiaq and Peter W. O’Hearn.  BI as an assertion language for mutable data structures.  In POPL, pages 14–26. ACM, 2001.
  * [26] Kenneth E. Iverson.  A Programming Language.  John Wiley & Sons, Inc., USA, 1962.
  * [27] Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens.  Verifast: A powerful, sound, predictable, fast verifier for C and Java.  In NFM, pages 41–55. Springer, 2011.
  * [28] Claire Jones.  Probabilistic Non-Determinism.  PhD thesis, University of Edinburgh, 1992.
  * [29] Cliff B. Jones.  Tentative steps toward a development method for interfering programs.  ACM Trans. Program. Lang. Syst., 5(4):596–619, 1983.
  * [30] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer.  Iris from the ground up: A modular foundation for higher-order concurrent separation logic.  J. Funct. Program., 28:e20, 2018.
  * [31] Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer.  Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning.  In POPL, pages 637–650. ACM, 2015.
  * [32] Benjamin L. Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo.  Weakest precondition reasoning for expected runtimes of randomized algorithms.  J. ACM, 65(5), 2018.
  * [33] Dexter Kozen.  Semantics of probabilistic programs.  In FOCS, pages 101–114. IEEE Computer Society, 1979.
  * [34] Dexter Kozen.  A probabilistic PDL.  In STOC, pages 291–297. ACM, 1983.
  * [35] Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer.  Fair termination for parameterized probabilistic concurrent systems.  In TACAS, pages 499–517. Springer, 2017.
  * [36] Christoph Matheja.  Automated Reasoning and Randomization in Separation Logic.  PhD thesis, RWTH Aachen University, Germany, 2020.
  * [37] Annabelle McIver and Carroll Morgan.  Partial correctness for probabilistic demonic programs.  Theoretical Computer Science, 266(1):513–541, 2001.
  * [38] Annabelle McIver and Carroll Morgan.  Abstraction, Refinement and Proof for Probabilistic Systems.  Monographs in Computer Science. Springer, 2005.
  * [39] Annabelle McIver, Tahiry Rabehaja, and Georg Struth.  Probabilistic rely-guarantee calculus.  Theoretical Computer Science, 655:120–134, 2016.
  * [40] Michael Mitzenmacher and Eli Upfal.  Probability and Computing: Randomized Algorithms and Probabilistic Analysis.  Cambridge University Press, 2005.
  * [41] Peter Müller, Malte Schwerhoff, and Alexander J. Summers.  Viper: A verification infrastructure for permission-based reasoning.  In Dependable Software Systems Engineering, volume 50 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 104–125. IOS Press, 2017.
  * [42] Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco.  Communicating state transition systems for fine-grained concurrent resources.  In ESOP, pages 290–310. Springer, 2014.
  * [43] Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann.  Bounded expectations: Resource analysis for probabilistic programs.  SIGPLAN Not., 53(4):496–512, 2018.
  * [44] Peter W. O’Hearn.  Resources, concurrency, and local reasoning.  Theoretical Computer Science, 375(1):271–307, 2007.
  * [45] Peter W. O’Hearn.  Separation logic.  Commun. ACM, 62(2):86–95, 2019.
  * [46] Ruzica Piskac, Thomas Wies, and Damien Zufferey.  Automating separation logic using SMT.  In CAV, pages 773–789. Springer, 2013.
  * [47] William Pugh.  Skip lists: A probabilistic alternative to balanced trees.  Commun. ACM, 33(6):668–676, 1990.
  * [48] Tobias Reinhard and Bart Jacobs.  Ghost signals: Verifying termination of busy waiting.  In CAV, pages 27–50. Springer, 2021.
  * [49] John C. Reynolds.  Separation logic: A logic for shared mutable data structures.  In LICS, pages 55–74. IEEE Computer Society, 2002.
  * [50] Joseph Tassarotti and Robert Harper.  A separation logic for concurrent randomized programs.  Proc. ACM Program. Lang., 3(POPL):64:1–64:30, 2019.
  * [51] Michael L. Tiomkin.  Probabilistic termination versus fair termination.  Theor. Comput. Sci., 66(3):333–340, 1989.
  * [52] Viktor Vafeiadis.  Concurrent separation logic and operational semantics.  Electronic Notes in Theoretical Computer Science, 276:335–351, 2011\.

##  Appendix A Quantitative Separation Logic

######  Lemma A.1 (Various Analysis Statements).

For sets $A\subseteq A^{\prime}$, $B\subseteq B^{\prime}$, countable set
$C\subseteq C^{\prime}$, non-empty set $D\subseteq D^{\prime}$ and real-valued
functions $f\colon A^{\prime}\times B^{\prime}\to[0,1]$, $g\colon
C^{\prime}\times D^{\prime}\to[0,1]$ we have

$\displaystyle\inf\left\\{\inf A_{b}\mid b\in
B\right\\}=\inf\bigcup\left\\{A_{b}\mid b\in B\right\\}$ (4)
$\displaystyle\inf\left\\{\inf\left\\{f(a,b)\mid a\in A\right\\}\mid b\in
B\right\\}=\inf\left\\{\inf\left\\{f(a,b)\mid b\in B\right\\}a\in A\right\\}$
(5) $\displaystyle\sup\left\\{\inf\left\\{f(a,b)\mid a\in A\right\\}\mid b\in
B\right\\}\leq\inf\left\\{\sup\left\\{f(a,b)\mid b\in B\right\\}\mid a\in
A\right\\}$ (6) $\displaystyle\sum\left[\inf\left\\{g(c,d)\mid d\in
D\right\\}\mid c\in C\right]\leq\inf\left\\{\sum\left[g(c,d)\mid c\in
C\right]\mid d\in D\right\\}$ (7)

######  Proof A.2.

Straightforward using real-valued analysis.

######  Lemma A.3 (Properties of Separating Multiplication).

For expectations $X,Y,Z$ and qualitative expectations $\varphi$:

$\displaystyle
X\mathbin{{\star}}(Y\mathbin{{\star}}Z)\quad=\quad(X\mathbin{{\star}}Y)\mathbin{{\star}}Z$
(Associativity) (8) $\displaystyle
X\mathbin{{\star}}\left[{\textsf{{{emp}}}}\right]\quad=\quad\left[{\textsf{{{emp}}}}\right]\mathbin{{\star}}X=X$
(Neutrality) (9) $\displaystyle X\mathbin{{\star}}Y\quad=\quad
Y\mathbin{{\star}}X$ (Commutativity) (10) $\displaystyle X\leq
Y\quad\text{implies}\quad X\mathbin{{\star}}Z\leq Y\mathbin{{\star}}Z$
(Monotonicity) (11) $\displaystyle
X\mathbin{{\star}}\max\left\\{\,{Y},\>{Z}\,\right\\}\quad=\quad\max\left\\{\,{X\mathbin{{\star}}Y},\>{X\mathbin{{\star}}Z}\,\right\\}$
(Dist. with max) (12) $\displaystyle\varphi\mathbin{{\star}}(Y\cdot
Z)\quad\leq\quad(\varphi\mathbin{{\star}}Y)\cdot(\varphi\mathbin{{\star}}Z)$
(Subdist. with mult.) (13) $\displaystyle
X\mathbin{{\star}}(Y+Z)\quad\leq(X\mathbin{{\star}}Y)+(X\mathbin{{\star}}Z)$
(Subdist. with plus) (14)

######  Proof A.4.

See [36, Theorem 6.14, Theorem 6.15, Theorem 6.16].

######  Lemma A.5 (Properties of (Guarded) Magic Wand).

For expectations $X,Y,Z$ and qualitative expectations $\varphi$:

$\displaystyle X\mathbin{{\star}}\varphi\leq Y\quad\text{iff}\quad
X\leq\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y$
(Adjointness) (15)
$\displaystyle\varphi\mathbin{{\star}}(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\quad\leq\quad
X$ (Modus Ponens) (16) $\displaystyle
X\quad\leq\quad\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\varphi\mathbin{{\star}}X)$
(17) $\displaystyle X\leq
Y\quad\text{implies}\quad\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\leq\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y$
(Monotonicity) (18)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\max\left\\{\,{X},\>{Y}\,\right\\}\quad\geq\quad\max\left\\{\,{\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X},\>{\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y}\,\right\\}$
(Superdist. with max) (19)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\min\left\\{\,{X},\>{Y}\,\right\\}\quad=\quad\min\left\\{\,{\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X},\>{\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y}\,\right\\}$
(Dist. with min) (20)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X+Y)\quad\geq\quad(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)+(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)$
(Superdist. with plus) (21)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\cdot
Y)\quad\geq\quad(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\cdot(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)$
(Superdist. with mult.) (22)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(\psi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\quad=\quad(\varphi\mathbin{{\star}}\psi)\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X$
(Combining magic wands) (23)
$\displaystyle\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\mathbin{{\star}}Y)\geq(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\mathbin{{\star}}Y$
(24)

######  Proof A.6.

See [36, Theorem 6.18, Theorem 6.19, Theorem 6.20, Theorem 6.21]. Theorem 6.21
in [36] has a small typo for Statement 22. We give a small proof for this here
instead:

$\displaystyle\varphi\mathbin{{\star}}(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\leq
X\quad\text{and}\quad\varphi\mathbin{{\star}}(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)\leq
Y$ (Statement 16) implies
$\displaystyle(\varphi\mathbin{{\star}}(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X))\cdot(\varphi\mathbin{{\star}}(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y))\leq
X\cdot Y$ (Monotoncitiy of multiplication) implies
$\displaystyle\varphi\mathbin{{\star}}((\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\cdot(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y))\leq
X\cdot Y$ (Statement 13) implies
$\displaystyle(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X)\cdot(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}Y)\leq\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\cdot
Y)$ (Statement 15)

For Statement 17 we give the proof:

$\displaystyle X\leq X$ implies $\displaystyle X\mathbin{{\star}}\xi\leq
X\mathbin{{\star}}\xi$ (Statement 11) implies $\displaystyle
X\leq\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\mathbin{{\star}}\xi)$
(Statement 15)

For Statement 23 we give the proof:

$\displaystyle\leavevmode\nobreak\
\left(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\left(\psi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\right)\right)(s,h)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\left\\{\inf\left\\{X(s,h^{\prime\prime})\mid\psi(s,h_{\psi})=1,h^{\prime\prime}=h^{\prime}\mathbin{{\star}}h_{\psi}\right\\}\mid\varphi(s,h_{\varphi})=1,h^{\prime}=h\mathbin{{\star}}h_{\varphi}\right\\}$
(Definition of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\left\\{X(s,h^{\prime\prime})\mid\psi(s,h_{\psi})=1,\varphi(s,h_{\varphi})=1,h^{\prime\prime}=h\mathbin{{\star}}h_{\varphi}\mathbin{{\star}}h_{\psi}\right\\}$
(Statement 4) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\left\\{X(s,h^{\prime\prime})\mid(\psi\mathbin{{\star}}\varphi)(s,h_{\psi}\mathbin{{\star}}h_{\varphi})=1,h^{\prime\prime}=h\mathbin{{\star}}h_{\varphi}\mathbin{{\star}}h_{\psi}\right\\}$
(Definition of separation conjunction) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\left(\left(\varphi\mathbin{{\star}}\psi\right)\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\right)(s,h)$
(Definition of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$)

For Statement 24 we give the proof:

$\displaystyle\leavevmode\nobreak\
\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}(X\mathbin{{\star}}Y)$
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\\{\sup\\{X(s,h_{1})\cdot Y(s,h_{2})\mid
h_{1}\mathbin{{\star}}h_{2}=h\mathbin{{\star}}h_{\varphi}\\}\mid\varphi(s,h_{\varphi})=1,h_{\varphi}\mathrel{\bot}h\\}$
(Definition of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and $\mathbin{{\star}}$) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\inf\\{\sup\\{X(s,h_{1}\mathbin{{\star}}h_{\varphi})\cdot Y(s,h_{2})\mid
h_{1}\mathbin{{\star}}h_{2}=h,h_{\varphi}\mathrel{\bot}h_{1}\\}\mid\varphi(s,h_{\varphi})=1,h_{\varphi}\mathrel{\bot}h\\}$
(Decreasing the supremum) $\displaystyle\geq$
$\displaystyle\leavevmode\nobreak\
\sup\\{\inf\\{X(s,h_{1}\mathbin{{\star}}h_{\varphi})\cdot
Y(s,h_{2})\mid\varphi(s,h_{\varphi}),h_{\varphi}\mathrel{\bot}h_{1}\\}\mid
h_{1}\mathbin{{\star}}h_{2}=h\\}$ (Statement 6 and decreasing the infimum)
$\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\sup\\{\inf\\{X(s,h_{1}\mathbin{{\star}}h_{\varphi})\mid\varphi(s,h_{\varphi}),h_{\varphi}\mathrel{\bot}h_{1}\\}\cdot
Y(s,h_{2})\mid h_{1}\mathbin{{\star}}h_{2}=h\\}$ (Factorisation with
constants) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(\varphi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}X\right)\mathbin{{\star}}Y$
(Definition of
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and $\mathbin{{\star}}$)

######  Definition A.7.

An expectation $X$ is precise iff

$\forall(s,h).\leavevmode\nobreak\
\left|\left\\{h^{\prime}\in\textsf{{Heaps}}\mid\exists
h^{\prime\prime}:h^{\prime}\mathbin{{\star}}h^{\prime\prime}=h\leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ X(s,h^{\prime})>0\right\\}\right|\leq
1\leavevmode\nobreak\ .$

######  Lemma A.8 (Properties for Precise Expectations).

For a precise expectation $X$ and a precise qualitative expectation $\varphi$:

$\displaystyle
X\mathbin{{\star}}\min\left\\{\,{Y},\>{Z}\,\right\\}\quad=\quad\min\left\\{\,{X\mathbin{{\star}}Y},\>{X\mathbin{{\star}}Z}\,\right\\}$
(Dist. with min) (25) $\displaystyle
X\mathbin{{\star}}(Y+Z)\quad=\quad(X\mathbin{{\star}}Y)+(X\mathbin{{\star}}Z)$
(Dist. with plus) (26) $\displaystyle\varphi\mathbin{{\star}}(Y\cdot
Z)\quad=\quad(\varphi\mathbin{{\star}}Y)\cdot(\varphi\mathbin{{\star}}Z)$
(Dist. with mult.) (27)

######  Proof A.9.

See [36, Theorem 6.25]

##  Appendix B Proofs for the Weakest Safe Liberal Preexpectation

######  Lemma B.1 (Monotonicity of step).

For all programs $C$ and $t,t^{\prime}\colon C\to\mathbb{E}_{\leq 1}$ we have

$t(C)\leq t^{\prime}(C)\quad\text{implies}\quad$ Step B.2

######  Proof B.4.

This follows directly by monotonicity of multiplication with probabilities,
countable sums and infima.

######  Lemma B.5 ($0-1$ Bounds on wrlp).

For all programs $C$, expectation $X$ and qualitative expectation $\xi$ we
have

$0\leq\textsf{{wrlp}}\llbracket C\rrbracket\left(X\mid\xi\right)\leq
1\leavevmode\nobreak\ .$

######  Proof B.6.

If $0\leq\textsf{{wrlp}}_{n}\llbracket C\rrbracket\left(X\mid\xi\right)\leq
1$, then the statement holds as well. We prove this new statement by induction
on $n$.

For the base case $n=0$ we have $0\leq\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(X\mid\xi\right)=1$.

Now we assume an arbitrary but fixed $n$ such that
$0\leq\textsf{{wrlp}}_{n}\llbracket C\rrbracket\left(X\mid\xi\right)\leq 1$
for all $C$, $X$ and $\xi$.

For the induction step, if $C=\;\downarrow\;$ the statement holds again
trivially since expectations are also $0-1$ bounded. Thus, we assume that
$C\neq\;\downarrow\;$. By the induction hypothesis
$0\leq\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(X\mid\xi\right)\leq 1$, thus also
$0\leq\textsf{{wrlp}}_{n}\llbracket
C^{\prime}\rrbracket\left(X\mid\xi\right)\mathbin{{\star}}\xi\leq 1$ for all
$C^{\prime}$. If $t$ is $0-1$ bounded, then the step function is also $0-1$
bounded:

$\displaystyle\inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime},(s^{\prime},h^{\prime}))\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ $\displaystyle\leq$
$\displaystyle\inf\bigg{\\{}\sum\left[p\cdot 1\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Lemma B.1) $\displaystyle\leq$
$\displaystyle\inf\left\\{1\mid a\in\text{Act}(C,(s,h))\right\\}$ (MDP
property) $\displaystyle=$ $\displaystyle 1$

$\displaystyle\inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime},(s^{\prime},h^{\prime}))\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ $\displaystyle\geq$
$\displaystyle\inf\bigg{\\{}\sum\left[p\cdot 0\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Lemma B.1) $\displaystyle\geq$
$\displaystyle\inf\left\\{0\mid a\in\text{Act}(C,(s,h))\right\\}$ (0 is zero
element) $\displaystyle=$ $\displaystyle 0$

Lastly, the quantitative magic wand is the infimum of all applicable values
for the second argument, thus also $0-1$ bounded if their second argument is
$0-1$ bounded.

######  Lemma B.9 (Antitonicity of $\textsf{{wrlp}}_{n}$ w.r.t. $n$).

For natural numbers $n\leq m$ we have

$\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\geq\textsf{{wrlp}}_{m}\llbracket
C\rrbracket\left(X\mid\xi\right)\leavevmode\nobreak\ .$

######  Proof B.10.

We instead prove by induction on $n$ the equivalent statement that

$\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\geq\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\xi\right)\leavevmode\nobreak\ .$

For the base case $n=0$ we have $\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(X\mid\xi\right)=1$, thus the statement holds trivially by
Lemma B.5.

Now for the induction hypothesis, we assume that for some fixed but arbitrary
$n$ we have $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\geq\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\xi\right)$ for all $C$.

For the induction step, if $C=\;\downarrow\;$ the statement holds trivially,
since
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)=X=\textsf{{wrlp}}_{n+2}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)$.
For $C\neq\;\downarrow\;$ we have

$\displaystyle\textsf{{wrlp}}_{n+2}\llbracket
C\rrbracket\left(X\mid\xi\right)=$
$\displaystyle\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
$\displaystyle\leq$
$\displaystyle\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Monotonicity of step, $\mathbin{{\star}}$,
$\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
and induction hypothesis) $\displaystyle=$
$\displaystyle\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\xi\right)$

######  Lemma B.13 (Alternative description of wrlp).

$\lim_{n\rightarrow\infty}\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)=\inf\left\\{\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\mid n\in\mathbb{N}\right\\}$

######  Proof B.14.

This follows from Lemma B.9 and real-valued analysis.

######  Definition B.15.

Recall that

$\displaystyle\text{reach}(n,\sigma_{1},\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\
=$ $\displaystyle\leavevmode\nobreak\
\sum\bigg{[}\prod_{i=1}^{m-1}\leavevmode\nobreak\ \leavevmode\nobreak\
\mathbb{P}(\sigma_{i},\mathfrak{s}(\sigma_{1}\dots\sigma_{i}))(\sigma_{i+1})$
$\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\;\sigma_{1}\dots\sigma_{m}\in
U^{m},\sigma_{m}=\sigma^{\prime},m\leq n\bigg{]}\leavevmode\nobreak\ .$

For final states $\sigma^{\prime}$

$\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\sigma^{\prime}\quad\text{iff}$ $\displaystyle\quad p\leavevmode\nobreak\
=\leavevmode\nobreak\
\text{reach}(n,\sigma,\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\ ,$
(28) $\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{1-p}^{n}\leavevmode\nobreak\ \dots\quad\text{iff}$
$\displaystyle\quad p\leavevmode\nobreak\ =\leavevmode\nobreak\
\sum_{\sigma^{\prime}\leavevmode\nobreak\
\text{final}}\text{reach}(n,\sigma,\mathfrak{s},\sigma^{\prime})\leavevmode\nobreak\
.$ (29)

######  Lemma B.16.

For a scheduler $\mathfrak{s}$, a state $\sigma$ and a final state
$\sigma^{\prime}$

$\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\sigma^{\prime}\quad\text{iff}$ $\displaystyle\quad p\leavevmode\nobreak\
=\leavevmode\nobreak\ \lim_{n\rightarrow\infty}q_{n}\leavevmode\nobreak\
\text{with}\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{q_{n}}^{n}\leavevmode\nobreak\ \sigma^{\prime}$
$\displaystyle\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\dots\quad\text{iff}$ $\displaystyle\quad p\leavevmode\nobreak\
=\leavevmode\nobreak\ \lim_{n\rightarrow\infty}q_{n}\leavevmode\nobreak\
\text{with}\leavevmode\nobreak\ \sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{q_{n}}^{n}\leavevmode\nobreak\ \dots$

######  Proof B.17.

Both follow by using real-valued analysis.

######  Lemma B.18.

For a scheduler $\mathfrak{s}$, a state $\sigma$ and a final state
$\sigma^{\prime\prime}$ with $\sigma\neq\sigma^{\prime\prime}$ and where
$\lambda\pi.\leavevmode\nobreak\ \mathfrak{s}(\sigma\pi)$ behaves as
$\mathfrak{s}$ with the difference that we always append $\sigma$ to its
argument, we have

$\text{reach}(n+1,\sigma,\mathfrak{s},\sigma^{\prime\prime})=\sum\left[\;\mathbb{P}(\sigma,\mathfrak{s}(\sigma))(\sigma^{\prime})\cdot\text{reach}(n,\sigma^{\prime},\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(\sigma\pi),\sigma^{\prime\prime})\mid\sigma^{\prime}\in
U\;\right]$

######  Proof B.19.

$\displaystyle\text{reach}(n+1,\sigma,\mathfrak{s},\sigma^{\prime\prime})$
$\displaystyle=\leavevmode\nobreak\ $
$\displaystyle\sum\left[\prod_{i=1}^{m-1}\mathbb{P}(\pi_{i},\mathfrak{s}(\pi_{1}\dots\pi_{i}))(\pi_{i+1})\middle|\pi\in
U^{m},\pi_{1}=\sigma,\pi_{m}=\sigma^{\prime\prime},m\leq n+1\right]$ (by
definition) $\displaystyle=\leavevmode\nobreak\ $
$\displaystyle\sum\left[\prod_{i=1}^{m-1}\mathbb{P}(\pi_{i},\mathfrak{s}(\pi_{1}\dots\pi_{i}))(\pi_{i+1})\middle|\pi\in
U^{m},\pi_{1}=\sigma,\pi_{m}=\sigma^{\prime\prime},2\leq m\leq n+1\right]$
(since $\sigma\neq\sigma^{\prime\prime}$) $\displaystyle=\leavevmode\nobreak\
$
$\displaystyle\sum\bigg{[}\mathbb{P}(\pi_{1},\mathfrak{s}(\pi_{1}))(\pi_{2})\cdot\prod_{i=2}^{m-1}\mathbb{P}(\pi_{i},\mathfrak{s}(\pi_{1}\pi_{2}\dots\pi_{i}))(\pi_{i+1})$
$\displaystyle\qquad\bigg{|}\pi\in
U^{m},\pi_{1}=\sigma,\pi_{m}=\sigma^{\prime\prime},2\leq m\leq n+1\bigg{]}$
(by commutativity) $\displaystyle=\leavevmode\nobreak\ $
$\displaystyle\sum\bigg{[}\mathbb{P}(\sigma,\mathfrak{s}(\sigma))(\pi_{1})\cdot\prod_{i=1}^{m-1}\mathbb{P}(\pi_{i},\mathfrak{s}(\sigma\pi_{1}\dots\pi_{i}))(\pi_{i+1})$
$\displaystyle\qquad\bigg{|}\pi\in U^{m},\pi_{m}=\sigma^{\prime\prime},1\leq
m\leq n\bigg{]}$ (renaming) $\displaystyle=\leavevmode\nobreak\ $
$\displaystyle\sum\bigg{[}\mathbb{P}(\sigma,\mathfrak{s}(\sigma))(\sigma^{\prime})\cdot\sum\big{[}\prod_{i=1}^{m-1}\mathbb{P}(\pi_{i},\mathfrak{s}(\sigma\pi_{1}\dots\pi_{i}))(\pi_{i+1})$
$\displaystyle\qquad\qquad\qquad\qquad\qquad\leavevmode\nobreak\ \big{|}\pi\in
U^{m},\pi_{1}=\sigma^{\prime},\pi_{m}=\sigma^{\prime\prime},1\leq m\leq
n\big{]}$ $\displaystyle\qquad\bigg{|}\sigma^{\prime}\in U\bigg{]}$ (by
distributivity) $\displaystyle=\leavevmode\nobreak\ $
$\displaystyle\sum[\mathbb{P}(\sigma,\mathfrak{s}(\sigma))(\pi_{1})\cdot\text{reach}(n,\sigma,\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(\sigma\pi),\sigma^{\prime})\mid\sigma^{\prime}\in U]$ (by
definition)

######  Definition B.20 (Weakest Liberal Preexpectation after $n$ steps).

$\displaystyle\textsf{{wlp}}_{n}\llbracket C\rrbracket\left(X\right)\quad=$
$\displaystyle\quad\inf\bigg{\\{}\sum\left[p\cdot X(s^{\prime},h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]+p_{div}$
$\displaystyle\quad\qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p_{div}}^{n}\leavevmode\nobreak\ \dots\bigg{\\}}$

######  Lemma B.21.

$\textsf{{wlp}}\llbracket
C\rrbracket\left(X\right)\quad=\quad\lim_{n\rightarrow\infty}\textsf{{wlp}}_{n}\llbracket
C\rrbracket\left(X\right)$

######  Proof B.22.

Follows directly from Lemma B.16.

######  Theorem B.23 (Equality between wlp and wlp).

$\textsf{{wrlp}}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)\quad=\quad\textsf{{wlp}}\llbracket
C\rrbracket\left(X\right)$

######  Proof B.24.

We first observe, that $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)$ simplifies to

$\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)=\begin{cases}1&\text{if}\leavevmode\nobreak\
n=0\\\ X&\text{if}\leavevmode\nobreak\ n\neq 0,C=\;\downarrow\\\
\step{C}{\lambda C^{\prime}.\leavevmode\nobreak\
\textsf{{wrlp}}_{n-1}\llbracket
C^{\prime}\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)}&\text{else.}\end{cases}$

We now prove by induction on $n$ that $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)=\textsf{{wlp}}_{n}\llbracket
C\rrbracket\left(X\right)$, which by Lemma B.21 also proofs the claim.

For the induction basis, we have that $n=0$, $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)(s,h)=1$ and that
$\textsf{{wlp}}_{n}\llbracket C\rrbracket\left(X\right)=1$ because of
$\text{reach}(0,\sigma,\mathfrak{s},\sigma^{\prime})=0$ and thus the
probability of non-termination is $1$.

Now we assume that for some fixed but arbitrary $n$ the claim holds.

For the induction step, we have two cases. If $C=\;\downarrow\;$, then
$\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)(s,h)=X(s,h)$; and
$\text{reach}(n+1,(C,(s,h)),\mathfrak{s},(\;\downarrow\;,(s,h)))=1$, thus
$\textsf{{wlp}}_{n+1}\llbracket C\rrbracket\left(X\right)(s,h)=X(s,h)$ as
well.

We will use lambda expressions to create anonymous functions. That is we
define for a sequence of states $\pi$ and a state $\sigma$ the notation
$(\lambda\pi^{\prime}.\leavevmode\nobreak\
\mathfrak{s}(\sigma.\pi^{\prime}))(\pi)=\mathfrak{s}(\sigma.\pi)$, where
$\sigma.\pi$ is the string concatenation of $\sigma$ with $\pi$. We can split
the first step apart from $\sigma\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}\leavevmode\nobreak\ \sigma^{\prime}$ due to
Lemma B.18. Thus, for $C\neq\downarrow$ we have:

$\displaystyle\textsf{{wlp}}_{n+1}\llbracket C\rrbracket\left(X\right)(s,h)$
$\displaystyle=$ $\displaystyle\inf\bigg{\\{}\sum\left[p\cdot
X(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n+1}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]+p_{div}$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p_{div}}^{n+1}\leavevmode\nobreak\ \dots\bigg{\\}}$
$\displaystyle=$ $\displaystyle\inf\bigg{\\{}\sum\left[p\cdot
X(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n+1}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\leavevmode\nobreak\ +\sum\left[p_{div}\mid
C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p_{div}}^{n+1}\leavevmode\nobreak\
\dots\right]\leavevmode\nobreak\ \bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\bigg{\\}}$ ($p_{div}$ is unique) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\left[p^{\prime\prime}\cdot p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\leavevmode\nobreak\ +\sum\left[p_{div}^{\prime\prime}\cdot
p_{div}^{\prime}\mid C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p_{div}^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]$ $\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (By Lemma B.18 and since $C\neq\downarrow$)
$\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}p^{\prime\prime}\cdot\sum\left[p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\qquad\qquad+p^{\prime\prime}\cdot\sum\left[p_{div}^{\prime}\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]$ $\displaystyle\qquad\qquad\bigg{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Distributivity) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\inf\bigg{\\{}\sum\bigg{[}p^{\prime\prime}\cdot\sum\left[p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\qquad\qquad\quad\leavevmode\nobreak\
+p^{\prime\prime}\cdot\sum\left[p_{div}^{\prime}\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]$ $\displaystyle\qquad\qquad\qquad\bigg{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\bigg{\\}}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Statement 4) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}\inf\bigg{\\{}p^{\prime\prime}\cdot\sum\left[p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\qquad\qquad\quad+p^{\prime\prime}\cdot\sum\left[p_{div}^{\prime}\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}(C,(s,h).\pi)]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]$ $\displaystyle\qquad\qquad\qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\bigg{\\}}\bigg{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Expressiveness of Schedulers, see
$\dagger$ below) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}\inf\bigg{\\{}p^{\prime\prime}\cdot\sum\left[p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\qquad\qquad\quad+p^{\prime\prime}\cdot\sum\left[p_{div}^{\prime}\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]$ $\displaystyle\qquad\qquad\qquad\bigg{|}\leavevmode\nobreak\
\mathfrak{s}\in\mathbb{S}\bigg{\\}}\bigg{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Set of schedulers where $C,(s,h)$ has been
taken and where it has not been taken is the same) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}p^{\prime\prime}\cdot\inf\bigg{\\{}\sum\left[p^{\prime}\cdot
X(s^{\prime},h^{\prime})\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})\right]$
$\displaystyle\quad\qquad\qquad\qquad\leavevmode\nobreak\ \leavevmode\nobreak\
+\sum\left[p_{div}^{\prime}\mid
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p_{div}^{\prime}}^{n}\leavevmode\nobreak\
\dots\right]\bigg{|}\leavevmode\nobreak\ \mathfrak{s}\in\mathbb{S}\bigg{\\}}$
$\displaystyle\qquad\qquad\bigg{|}\leavevmode\nobreak\
C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Infimum of multiplication with constants)
$\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}p^{\prime\prime}\cdot\textsf{{wlp}}_{n}\llbracket
C^{\prime\prime}\rrbracket\left(X\right)(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\bigg{|}\leavevmode\nobreak\ C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Rephrasing as wlp) $\displaystyle=$
$\displaystyle\inf\bigg{\\{}\sum\bigg{[}p^{\prime\prime}\cdot\textsf{{wrlp}}_{n}\llbracket
C^{\prime\prime}\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)(s^{\prime\prime},h^{\prime\prime})\leavevmode\nobreak\
\bigg{|}\leavevmode\nobreak\ C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p^{\prime\prime}}\leavevmode\nobreak\
C^{\prime\prime},(s^{\prime\prime},h^{\prime\prime})\bigg{]}$
$\displaystyle\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s,h))\bigg{\\}}$ (Induction hypothesis) $\displaystyle=$
(Rephrasing as step) $\displaystyle=$
$\displaystyle\;\textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\left[{\textsf{{{emp}}}}\right]\right)(s,h)$ (Rephrasing
as wrlp)

The step in $\dagger$ is the most difficult part here. We will not go into all
details and instead give a proof sketch. The first direction (which is the
same as in Statement 7), i.e.,

$\inf\left\\{\sum_{\sigma^{\prime}\in
A}f(\mathfrak{s},\sigma^{\prime})\,\middle|\,\mathfrak{s}\in\mathbb{S}\right\\}\geq\sum_{\sigma^{\prime}\in
A}\inf\left\\{f(\mathfrak{s},\sigma^{\prime})\mid\mathfrak{s}\in\mathbb{S}\right\\}\leavevmode\nobreak\
,$

it is easy (but technical) to proof: the value for choosing only one scheduler
for all summands will always be at least as high as if we choose one scheduler
each for every summand. The other direction, i.e.,

$\inf\left\\{\sum_{\sigma^{\prime}\in
A}f(\mathfrak{s},\sigma^{\prime})\middle|\mathfrak{s}\in\mathbb{S}\right\\}\leq\sum_{\sigma^{\prime}\in
A}\inf\left\\{f(\mathfrak{s},\sigma^{\prime})\mid\mathfrak{s}\in\mathbb{S}\right\\}\leavevmode\nobreak\
,$

is far more difficult to prove. Let $\sigma$ be the current state and
$\sigma^{\prime}$ be the next state chosen in the sum. To prove this, one need
to consider sequences of schedulers for each summand
$\mathfrak{s}_{\sigma^{\prime},i}$ such that they convert to the infimum,
i.e.,

$\inf\left\\{f(\mathfrak{s},\sigma^{\prime})\mid\mathfrak{s}\in
S\right\\}=\lim_{i\rightarrow\infty}f(\mathfrak{s}_{\sigma^{\prime},i},\sigma^{\prime})\leavevmode\nobreak\
.$

From these, one can show that we can always construct a sequence of schedulers
$\mathfrak{s}_{i}$ for all summands such that $\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}_{i}(\sigma.\sigma^{\prime}.\pi)=\lambda\pi.\leavevmode\nobreak\
\mathfrak{s}_{\sigma^{\prime},i}(\sigma.\sigma^{\prime}.\pi)$. The expression
then converges for the sequence $\mathfrak{s}_{i}$ to the same value, i.e.,

$\lim_{i\rightarrow\infty}\sum_{\sigma^{\prime}\in
A}f(\mathfrak{s}_{i},\sigma^{\prime})=\sum_{\sigma^{\prime}\in
A}\lim_{i\rightarrow\infty}f(\mathfrak{s}_{\sigma^{\prime},i},\sigma^{\prime})\leavevmode\nobreak\
.$

From both directions, the equality then also follows.

Thus, the claim is proven.

##  Appendix C Proofs about Framing

######  Definition C.1.

We define stacks $s$ and $s^{\prime}$ as equal for variables in $V$ as

$\left(s\sim s^{\prime}\right)^{V}\quad\text{iff}\quad\forall x\in
V\leavevmode\nobreak\ s(x)=s^{\prime}(x)\leavevmode\nobreak\ .$

######  Definition C.2.

We define the in program $C$ written variables $\text{Write}(C)$ as all
variables occurring on left sides of assignments, lookups and allocation.

######  Lemma C.3.

For a chpGCL program without atomic region $C$ and
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})$ we have $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$.

######  Proof C.4.

We prove this by induction on $C$.

As the induction base we have that

  * •

for the terminated program, such a transition does not exist;

  * •

for the non-terminating program, probabilistic choice, conditional choice,
loops, disposal and mutations, we always have $C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\ C^{\prime},(s,h^{\prime})$,
trivializing the statement; and

  * •

for assignment, allocation and lookup that the program on the left hand side
is in $\text{Write}(C)$ and thus does not change the value of variables in
$\mathsf{Vars}\setminus\text{Write}(C)$.

Now we establish the induction hypothesis that for $C_{1}$, $C_{2}$ and
$C_{i},(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C_{i},(s_{i}^{\prime},h_{i}^{\prime})$ we have $\left(s\sim
s_{i}^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C_{i})}$ and prove
the claim for the sequential composition and concurrency.

For the induction step we have that

  * •

for the sequential composition, we directly have that for
${C_{1}}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
{C_{1}^{\prime}}{\,;}\leavevmode\nobreak\
{C_{2}},(s_{1}^{\prime},h_{i}^{\prime})$ and
${\;\downarrow\;}{\,;}\leavevmode\nobreak\ {C_{2}},(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C_{2}^{\prime},(s_{1}^{\prime},h_{i}^{\prime})$, the claim follows directly by
the induction hypothesis;

  * •

for concurrency, we have for both cases of $i$ in
$\left.C_{1}\;\middle\|\;C_{2}\right.,(s,h)\leavevmode\nobreak\
\xrightarrow[Ci.a]{p}\leavevmode\nobreak\
\left.C_{1}^{\prime}\;\middle\|\;C_{2}^{\prime}\right.(s_{i}^{\prime},h_{i}^{\prime})$
that the claim follows in both cases directly by the induction hypothesis.

######  Lemma C.5.

For a chpGCL program $C$ with atomic regions and $C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ we have that $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$.

######  Proof C.6.

We prove the claim with nested inductions. The first induction is on the level
of atomic regions, i.e., we start with a program without any atomic region and
increase the possible nested atomic regions in the induction step. The second
induction is on the number of steps on the operational semantics $n$.

Thus, we first start with a program that does not have any atomic region and
prove that for $C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ we have $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$. For $n=0$ we only
have $C=\;\downarrow\;$, thus trivially $s=s^{\prime}$. We establish the
induction hypothesis $\dagger$ for $n$ and prove the claim for $n+1$. By Lemma
C.3 we have for $C,(s,h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\ C^{\prime},(s^{\prime},h)$ that
$\left(s\sim s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$,
furthermore by induction hypothesis $\dagger$ we have for
$C^{\prime},(s^{\prime},h^{\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p^{\prime}}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime\prime},h^{\prime\prime})$ that $\left(s^{\prime}\sim
s^{\prime\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$. Together we
also have by Lemma B.18 that for $C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}^{\prime}]{p^{\prime\prime}}^{n+1}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime\prime},h^{\prime\prime})$ we also have $\left(s\sim
s^{\prime\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$.

Now we assume that for a fixed but arbitrary level of nested atomic regions
the claim holds as our induction hypothesis $\spadesuit$.

For the induction step, we again prove by induction over n that
$C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$. We prove this again by induction over
$n$. For $n=0$ we have $C=\;\downarrow\;$, thus trivially $s=s^{\prime}$. We
establish the induction hypothesis $\dagger\dagger$ for $n$ and prove the
claim for $n+1$. The first part of the proof is for most cases totally
analogous to Lemma C.3 except for the atomic region. Thus, we only consider
the case that $C=\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\}$ Then
we have the transition
$\textnormal{{atomic}}\left\\{\,{C^{\prime}}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ and by $\spadesuit$ that for all $m$
with $C^{\prime},(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{m}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ also $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C^{\prime})}$, therefore
also for $C^{\prime},(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}{}^{*}\hskip 3.01125pt\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ we have $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C^{\prime})}$ by Lemma
B.16 and thus also for
$\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime},h^{\prime})$ we have $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$. For
$\textnormal{{atomic}}\left\\{\,{C}\,\right\\},(s,h)\leavevmode\nobreak\
\xrightarrow[atomic]{p}\leavevmode\nobreak\ \textnormal{{diverge}},(s,h)$ we
trivially have $s=s$. With a similar proof as Lemma C.3, we get for
$C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})$ that $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$ and from
$\dagger\dagger$ we get
$C^{\prime},(s^{\prime},h^{\prime})\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}]{p}^{n}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime\prime},h^{\prime\prime})$. Together and by Lemma
B.18 we get that for $C,(s,h)\leavevmode\nobreak\
\xrightarrow[\mathfrak{s}^{\prime}]{p^{\prime\prime}}^{n+1}\leavevmode\nobreak\
\;\downarrow\;,(s^{\prime\prime},h^{\prime\prime})$ we also have $\left(s\sim
s^{\prime\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$.

######  Lemma C.7.

For $C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})$ we have $\left(s\sim
s^{\prime}\right)^{\mathsf{Vars}\setminus\text{Write}(C)}$.

######  Proof C.8.

Follows from Lemma C.5 with $n=1$.

######  Definition C.9 (Free Variables).

We define the free variables of an expectation $X$ as

$\text{Vars}\,(X)\quad=\quad\\{x\in\mathsf{Vars}\mid\exists
v,v^{\prime}\in\mathbb{Z}:X\left[{x}\coloneqq{v}\right]\neq
X\left[{x}\coloneqq{v^{\prime}}\right]\\}\leavevmode\nobreak\ .$

We define the free variables of a program $\text{Vars}\,(C)$ as all variables
occurring in the program $C$. We furthermore define
$\text{Vars}\,(A_{1},A_{2},\dots)=\text{Vars}\,(A_{1})\cup\text{Vars}\,(A_{2})\cup\dots$.

######  Lemma C.10.

If $\left(s\sim s^{\prime}\right)^{V}$ and $\text{Vars}\,(X)\subseteq V$ then
$X(s,h)=X(s^{\prime},h)$.

######  Proof C.11.

Assume there are stacks $s$ and $s^{\prime}$ with $\left(s\sim
s^{\prime}\right)^{V}$ such that $X(s,h)\neq X(s^{\prime},h)$. Then $s$ and
$s^{\prime}$ need to be different in at least one variable. For simplicity, we
assume they differ in exactly one variable. Let $x$ be this variable, such
that $s(x)\neq s^{\prime}(x)$. Then $x\not\in V$ since $\left(s\sim
s^{\prime}\right)^{V}$ and $x\not\in\text{Vars}\,(X)$ since
$\text{Vars}\,(X)\subseteq V$. Therefore, there exists no
$v,v^{\prime}\in\mathsf{Vars}$ such that $X\left[{x}\coloneqq{v}\right]\neq
X\left[{x}\coloneqq{v^{\prime}}\right]$. Then there can also not exist
$v,v^{\prime}\in\mathsf{Vars}$ with $X(s\left[{x}\coloneqq{v}\right],h)\neq
X(s\left[{x}\coloneqq{v^{\prime}}\right],h)$ and therefore
$s(x)=s^{\prime}(x)$, which violates our assumption. It is now easy to extend
this proof to $s$ and $s^{\prime}$ which differ in arbitrary many variables
using a sequence of stacks that only differ in one variable with their
predecessor and successor each.

######  Lemma C.12 (Overapproximating Free Variables).

$\text{Vars}\,(\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right))\subseteq\text{Vars}\,(C,X,\xi)$

######  Proof C.13.

We prove this by contraposition, i.e., that for every
$x\in\mathsf{Vars}\setminus\text{Vars}\,(C,X,\xi)$ we have for all values
$v,v^{\prime}$ that $\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v}\right]=\textsf{{wrlp}}_{n}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v^{\prime}}\right]$. We
will prove this by induction on $n$.

The induction base $n=0$ holds trivially, since we have
$\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v}\right]=1=\textsf{{wrlp}}_{0}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v^{\prime}}\right]$.

We now assume that the claim holds for some arbitrary but fixed $n$ as our
induction hypothesis.

For the induction step, we have two cases. For the case that
$C=\;\downarrow\;$ we have the equality
$\textsf{{wrlp}}_{n+1}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v}\right]=X\left[{x}\coloneqq{v}\right]=X\left[{x}\coloneqq{v^{\prime}}\right]=\textsf{{wrlp}}_{n}\llbracket\;\downarrow\;\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v^{\prime}}\right]$
by assumption that $x\not\in\text{Vars}\,(X)$. For the case that
$C\neq\;\downarrow\;$ we have

$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v}\right]$ $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)\left[{x}\coloneqq{v}\right]$
(Definition of wrlp) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($x\not\in\text{Vars}\,(\xi)$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($\dagger$ see below) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($x\not\in\text{Vars}\,(\xi)$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
(Induction Hypothesis) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($x\not\in\text{Vars}\,(\xi)$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\
\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}$
($\dagger$ see below) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\left(\xi\mathbin{\text{\raisebox{-0.43057pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.55974pt}{\rotatebox{-17.0}{$\star$}}}}\right)\left[{x}\coloneqq{v^{\prime}}\right]$
($x\not\in\text{Vars}\,(\xi)$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \textsf{{wrlp}}_{n+1}\llbracket
C\rrbracket\left(X\mid\xi\right)\left[{x}\coloneqq{v^{\prime}}\right]$
(Definition of wrlp)

Now regarding $\dagger$:

$\displaystyle=$ (Definition of substitution) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime},h^{\prime})\mid
C,(s\left[{x}\coloneqq{v}\right],h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s\left[{x}\coloneqq{v}\right],h))\bigg{\\}}$ (Definition of
step) $\displaystyle=$ $\displaystyle\leavevmode\nobreak\
\inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime}\left[{x}\coloneqq{v}\right],h^{\prime})\mid
C,(s\left[{x}\coloneqq{v}\right],h)\leavevmode\nobreak\
\xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime}\left[{x}\coloneqq{v}\right],h^{\prime})\right]$
$\displaystyle\leavevmode\nobreak\ \qquad\bigg{|}\leavevmode\nobreak\
a\in\text{Act}(C,(s\left[{x}\coloneqq{v}\right],h))\bigg{\\}}$ (Since
$x\not\in\text{Vars}\,(C)$ we have $s^{\prime}(x)=v$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\left[p\cdot
t(C^{\prime})(s^{\prime}\left[{x}\coloneqq{v}\right],h^{\prime})\mid
C,(s,h)\leavevmode\nobreak\ \xrightarrow[a]{p}\leavevmode\nobreak\
C^{\prime},(s^{\prime},h^{\prime})\right]$ $\displaystyle\leavevmode\nobreak\
\qquad\bigg{|}\leavevmode\nobreak\ a\in\text{Act}(C,(s,h))\bigg{\\}}$
(Operational semantics and since $x\not\in\text{Vars}\,(C)$) $\displaystyle=$
$\displaystyle\leavevmode\nobreak\ \inf\bigg{\\{}\sum\left[p\cdot