Why is linearizability a safety property and why are safety properties closed sets?

Question

In Chapter 13 "Atomic Objects" of the book "Distributed Algorithms" by Nancy Lynch, linearizability (also known as atomicity) is proved to be a safety property. That is to say, its corresponding trace property is nonempty, prefix-closed, and limit-closed, as defined in Section 8.5.3. Informally, a safety property is often interpreted as saying that some particular "bad" thing never happens.

Based on this, my first problem is as follows:

What are the advantages of linearizability as a safety property? Are there some results based on this fact in the literature?

In the study of the classification of safety property and liveness property, it is well-known that safety property can be characterized as the closed set in an appropriate topology. In the paper "The Safety-Progress Classification" @1993 by Amir Pnueli et al., a metric topology is adopted. More specifically, a property $\Phi$ is a set of (finite or infinite) words over the alphabet $\Sigma$. The property $A(\Phi)$ consists of all infinite words $\sigma$ such that all prefixes of $\sigma$ belong to $\Phi$. For example, if $\Phi = a^{+}b^{\ast}$, then $A(\Phi) = a^{\omega} + a^{+}b^{\omega}$. An infinitary property $\Pi$ is defined to be a safety property if $\Pi = A(\Phi)$ for some finitary property $\Phi$. The metric $d(\sigma, \sigma')$ between infinite words $\sigma$ and $\sigma'$ is defined to be 0 if they are identical, and $d(\sigma, \sigma') = 2^{-j}$ otherwise, where $j$ is the length of the longest common prefix on which they agree. With this metric, the safety property can be characterized as closed sets topologically.

Here comes my second problem:

How to characterize linearizablity as closed sets topologically? In particular, what is the underlying set and what is the topology?

Answer 1

What are the advantages of linearizability as a safety property? Are there some results based on this fact in the literature?

Suppose that you've implemented a shared memory machine $M$ that only satisfies eventual linearization, defined as follows: in every run $\alpha$ of $M$, there exists some point in time $T_\alpha$, such that linearization holds from time $T_\alpha$ on. Note that there is no upper bound on $T$. (*) (This is an artificial liveness counterpart of the standard safety property definition of linearizability.)

Such a shared memory implementation wouldn't be very useful to the programmer: Note that if only eventual linearizability holds, there are no guarantees whatsoever on the consistency of read/write operations in any "early" prefix of a run (before the unknown time $T$). Or, in other words, whatever has happened until now, you can still extend the current prefix of a run to one that satisfies eventual linearizability.

(*) If there was such an upper bound, then eventual linearizability would become a safety property.

How to characterize linearizablity as closed sets topologically? In particular, what is the underlying set and what is the topology?

We can define a metric topology on the set $ASYNC$, which is the set of all possible runs of a distributed algorithms. Note that each run $\alpha \in ASYNC$ corresponds to an infinite sequence of state transitions. For $\alpha, \beta \in ASYNC$, $\alpha \ne \beta$, we define $$d(\alpha,\beta) := 2^{-N}$$where $N$ is the earliest index where the state transitions in $\alpha$ and $\beta$ differ; otherwise, if $\alpha = \beta$, we define $d(\alpha,\beta) = 0$.

We first argue that $d$ is a metric on $ASYNC$. By definition, $d$ is nonnegative and $\forall \alpha,\beta \in ASYNC$ we have $d(\alpha,\beta)=d(\beta,\alpha)$. For $\alpha,\beta,\gamma \in ASYNC$, the triangle-inequality $d(\alpha,\beta) \le d(\alpha,\gamma) + d(\gamma,\beta)$ trivially holds if $\gamma=\alpha$ or $\gamma=\beta$. Now consider the case that $d(\alpha,\gamma) \ge d(\gamma,\beta) > 0$, i.e., $d(\alpha,\gamma)=2^{-n_1}$ and $d(\gamma,\beta)=2^{-n_2}$, for some indices $n_1\le n_2$. Since $\gamma$ shares a common prefix of length $n_2-1$ with $\beta$ but only a prefix of length $n_1-1$ with $\alpha$, it follows that $\alpha$ and $\beta$ differ at index $n_1$, and thus $d(\alpha,\beta) = d(\alpha,\gamma)$ and the triangle-inequality follows. The case where $0<d(\alpha,\gamma) < d(\gamma,\beta)$ follows analogously.

The metric $d$ induces a topology (e.g., page 119 of [1]) where the $\epsilon$-balls $B_\varepsilon(\alpha) = \{ \beta \in ASYNC \mid d(\alpha,\beta) < \varepsilon \}$ are the basic open sets. We will now argue why safety properties correspond to closed sets: If an execution $\alpha$ does not satisfy a safety property $S\subseteq ASYNC$, i.e.\ $\alpha \notin S$, then there is an index $N$ where all runs $\beta$ that share a prefix longer than $N$ with $\alpha$ are not in $S$. This closely matches intuition, since once a safety property is violated in a prefix of an execution, it makes no difference how this prefix is extended! Formally speaking, suppose that $\alpha \notin S$. There exists an $N\geq 0$ such that, if some $\beta \in ASYNC$ has $d(\alpha,\beta) < {2^{-N}}\text{,}$ i.e., $\alpha$ and $\beta$ share a prefix of length $\ge N$, then $\beta \notin S$. Thus, the set of runs $S$ is closed, since its complement is open.

[1] James Munkres. Topology.

Answer 2

Regarding your first question - safety properties are, in a way, the "easiest" properties to handle, with respect to problems such as model-checking and synthesis.

The basic reason for this is that in the automata-theoretic approach to formal methods, reasoning about safety properties reduces to reasoning about finite traces, which is easier than the standard infinite-trace setting.

See the work of Orna Kupferman here as a starting point.