11:00
12:00

Verifying Liveness Properties under Weak Memory Models

I will discuss verifying liveness properties for concurrent programs running on
weak memory models. To that end, I will introduce the notion of
Memory-Boundness-Fairness (MBF) that precludes demonic memory updates that make
most liveness properties trivially unsatisfiable. MBF implies the existence of
an (unknown) bound on the number of messages in transient in the memory system.
In the case of the classical TSO semantics, MBF says that the store buffers are
bounded in size, although the bound is not known. MBF is motivated by practical
limitations on the system, such as the physical size of the underlying hardware.
Furthermore, we show that MBF makes liveness properties amenable to algorithmic
verification.

To develop algorithms for checking liveness conditions under MBF, we consider an
alternative fairness condition, namely probabilistic fairness, and show that MBF
coincides with probabilistic fairness in liveness verification. We exploit this
connection to reduce the liveness checking problem (repeated state reachability)
to the safety checking problem (simple state reachability). We show this is a
general phenomenon by developing a uniform framework that is the formal
foundation of our fairness definition and can be instantiated to a broad
landscape of memory models. These models include SC, TSO, PSO, (Strong/Weak)
Release-Acquire, Strong Coherence, Causal Consistency, FIFO Consistency, and
RMO.

sale 178