<p>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.</p>

<p>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. </p>

<p>See the work of <a href="http://www.cs.huji.ac.il/~ornak/publications/atva06a.pdf">Orna Kupferman here</a> as a starting point.</p>

CC BY-SA 3.0
2014-02-27T13:46:20.910Z
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?
hengxin
CC BY-SA 3.0
2014-02-27T14:07:03.993Z
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.
Shaull
CC BY-SA 3.0
2014-02-28T02:02:38.677Z
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](http://link.springer.com/content/pdf/10.1007%2Fs00165-009-0130-y.pdf). I will try to read it in these days. However, I not sure about its quality. Looking forward to your comments.
hengxin
CC BY-SA 3.0
2014-02-28T05:53:17.543Z
Perhaps [this](http://dl.acm.org/citation.cfm?id=2144362) 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.
Shaull
CC BY-SA 3.0
2014-02-27T12:51:03.560Z
2014-02-27T12:51:03.560Z
Shaull
<blockquote>
  <p>What are the advantages of linearizability as a safety property? Are there some results based on this fact in the literature?</p>
</blockquote>

<p>Suppose that you've implemented a shared memory machine $M$ that only satisfies <em>eventual linearization</em>, 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.)</p>

<p>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.  </p>

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

<blockquote>
  <p>How to characterize linearizablity as closed sets topologically? In particular, what is the underlying set and what is the topology?</p>
</blockquote>

<p>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$.</p>

<p>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) &gt; 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&lt;d(\alpha,\gamma) &lt; d(\gamma,\beta)$ follows analogously.</p>

<p>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) &lt; \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$. <strong>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!</strong>
Formally speaking, suppose that $\alpha \notin S$. 
There exists an $N\geq 0$ such that, if some
$\beta \in ASYNC$ has $d(\alpha,\beta) &lt; {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.</p>

<p>[1] James Munkres. Topology. </p>

CC BY-SA 3.0
2014-02-27T13:53:59.107Z
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...`?
hengxin
CC BY-SA 3.0
2014-02-27T16:38:01.933Z
Yes, I've added the reference.
Peter
CC BY-SA 3.0
2014-02-28T09:03:43.573Z
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.
hengxin
CC BY-SA 3.0
2014-02-28T09:54:11.293Z
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?
hengxin
CC BY-SA 3.0
2014-03-03T01:40:23.967Z
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.
Peter
CC BY-SA 3.0
2014-02-27T13:39:10.680Z
2014-02-28T07:27:19.867Z
2014-02-28T07:27:19.867Z
Peter
<p>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 <em>nonempty, prefix-closed, and limit-closed</em>, as defined in Section 8.5.3. Informally, a safety property is often interpreted as saying that some particular "bad" thing never happens.  </p>

<p>Based on this, my first problem is as follows:</p>

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

<p>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 <a href="http://link.springer.com/chapter/10.1007%2F978-3-642-58041-3_5">"The Safety-Progress Classification" @1993 by Amir Pnueli et al.</a>, 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 <em>all</em> 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 <em>safety property</em> 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.</p>

<p>Here comes my second problem:</p>

<blockquote>
  <p>How to characterize linearizablity as closed sets topologically? In particular, what is the underlying set and what is the topology?</p>
</blockquote>

<reference-request><fl.formal-languages><dc.distributed-comp><concurrency>
Why is linearizability a safety property and why are safety properties closed sets?
hengxin
# Why is linearizability a safety property and why are safety properties closed sets?

(Asked by: username_0 on 2014-02-27)

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.](http://link.springer.com/chapter/10.1007%2F978-3-642-58041-3_5), 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?

**Tags:** reference-request, fl.formal-languages, dc.distributed-comp, concurrency


---

## 2 answers

### Answer by username_2 on 2014-02-27. Score: 8 | Accepted answer

> 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

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.

> **Comments:**
> **username_0**: 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...`?  
> **username_2**: Yes, I've added the reference.  
> **username_0**: 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.  
> **username_0**: 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?  
> **username_2**: 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.  

---

### Answer by username_1 on 2014-02-27. Score: 6

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](http://www.cs.huji.ac.il/~ornak/publications/atva06a.pdf) as a starting point.

> **Comments:**
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: 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](http://link.springer.com/content/pdf/10.1007%2Fs00165-009-0130-y.pdf). I will try to read it in these days. However, I not sure about its quality. Looking forward to your comments.  
> **username_1**: Perhaps [this](http://dl.acm.org/citation.cfm?id=2144362) 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.  

---

