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?


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.

  • $\begingroup$ Thanks for your answer. I have to ponder over it. By the way, are you referring to the book "Topology" by James R. Munkres when you says that The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...? $\endgroup$ – hengxin Feb 27 '14 at 13:53
  • $\begingroup$ Yes, I've added the reference. $\endgroup$ – Peter Feb 27 '14 at 16:38
  • $\begingroup$ I noticed that you have suggested a modification of the title of this post (if I have made a mistake, please ignore this comment). First of all, I agree that the two subproblems should be reflected in the title. However, I am not asking about "why is linearizability a safety property?". I am asking about the consequences of this fact. I am not sure how to modify the title appropriately and I have skipped this modification. Please let me know if you have other comments or ideas. $\endgroup$ – hengxin Feb 28 '14 at 9:03
  • $\begingroup$ I realized that the characterization (proof) of linearizability as closed set basically has nothing to do with the notion of linearization points. It seems like a more general proof which characterizes any safety property as closed set. Did I miss something? $\endgroup$ – hengxin Feb 28 '14 at 9:54
  • $\begingroup$ Yes, all safety properties are closed sets, while liveness properties are dense sets in this topology. In fact, every property (i.e. set of runs) can be expressed as a conjunction (i.e. intersection) of safety and liveness properties. $\endgroup$ – Peter Mar 3 '14 at 1:40

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.

  • $\begingroup$ When expressed in linear temporal logic, the safety properties can be captured and checked against some special class of B$\ddot{u}$chi automata. However, I have not realized any material on how to express and check linearizability in terms of automata. Therefore, such advantage may be not shared by linearizability (as a safety property). What do you think of that? $\endgroup$ – hengxin Feb 27 '14 at 13:46
  • $\begingroup$ I'm pretty sure Iv'e seen papers that deal with linearizability via LTL, at least in specific cases. If I find them, I'll comment. $\endgroup$ – Shaull Feb 27 '14 at 14:07
  • $\begingroup$ That will be great. I am always curious about how to deal with linearizability via LTL, especially with the notion of linearization points. Following your hint, I find the paper Proving linearizability with temporal logic. I will try to read it in these days. However, I not sure about its quality. Looking forward to your comments. $\endgroup$ – hengxin Feb 28 '14 at 2:02
  • $\begingroup$ Perhaps this will be of use. Judging by the authors, this is a serious paper. I'm not sure how tight the connection to LTL is, though. $\endgroup$ – Shaull Feb 28 '14 at 5:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.