<p>Herlihy and Wing write on p. 477: </p>

<blockquote>
  <p>In conclusion, the rep invariant $\mathbf{I}$ must be continually satisfied and the abstraction function continually defined, not only between abstract operations, but also between rep operations implementing abstract operations. The abstraction function maps each rep value to a nonempty set of abstract values:
  $$
\mathbf{A}: \mathrm{REP} \to 2^{\mathrm{ABS}}
$$</p>
</blockquote>

<p>I am tempted to read into this that even when an abstract operation is implemented by a sequence of multiple rep operations, the rep invariant has to hold after each of those rep operations, and when it holds, then the rep value must have at least one abstract counterpart.</p>

<p>Many people have addressed some of the challenges posed in this paper. One of the more interesting and recent developments is  R Jagadeesan and J Riely's <em>Quantitative Quiescent Consistency</em> [<a href="http://arxiv.org/abs/1402.4043" rel="nofollow">http://arxiv.org/abs/1402.4043</a>].</p>

CC BY-SA 3.0
2015-11-25T01:30:45.893Z
Thanks. However it does not answer my questions on *verification techniques*. Could you please make it more specific?
hengxin
CC BY-SA 3.0
2015-11-24T13:40:35.100Z
2015-11-24T13:40:35.100Z
Kai
<p>In Section 4.3.2 entitled "Proof Method" of</p>

<ul>
<li>Herlihy and Wing, "<a href="https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf" rel="nofollow">Linearizability: A Correctness Condition for Concurrent Objects</a>", 1990</li>
</ul>

<p>the authors describe the technique for 
verifying implementations of linearizable objects as follows:</p>

<blockquote>
  <p>Assume that the implementation of $r$ is correct, 
  hence $\text{H} \mid {\small \text{REP}}$ is linearizable 
  for all $\text{H}$ in the implementation. 
  Our verification technique focuses on showing the following property 
  (denoted $\mathcal{P}$ for later reference, by myself):
  $$\text{For all } r \in \text{Lin}(\text{H}\mid{\small\text{REP}}), \text{I}(r)
\text{ holds and } \text{A}(r) \subseteq 
\text{Lin}(\text{H}\mid{\small\text{ABS}}).$$
  This condition implies that $\text{Lin}(\text{H} \mid {\small \text{ABS}})$ 
  is nonempty, hence that $\text{H} \mid {\small \text{ABS}}$ is linearizable.</p>
</blockquote>

<p>I don't understand:</p>

<blockquote>
  <p>Why is it <em>sufficient</em> to show that $\text{A}(r) \subseteq 
\text{Lin}(\text{H}\mid{\small\text{ABS}})$ (besides the "invariant" $\text{I}(r)$ property) 
  holds for the verification purpose?</p>
</blockquote>

<p>Specifically, to show the property $\mathcal{P}$, 
are we showing that there <strong>exists</strong> an $\text{I}(r)$ and an $\text{A}(r)$
such that $\mathcal{P}$ holds? 
If so, why cannot we just set $\text{I}(r) = \top$ and $\text{A}(I) = \emptyset$
which trivially satisfy $\mathcal{P}$? 
If not, what is the formal definition of "verification" here?</p>

<hr>

<h3>About examples in this paper:</h3>

<ul>
<li><p>Section 4.3.3: in the <code>queue</code> example, 
$\text{I}(r)$ and $\text{A}(I)$ are far from trivial.<br>
What are the specifications that prevent us from choosing 
$\text{A}(I) = \emptyset$ in this example?</p></li>
<li><p>Section 4.2: to motivate their definitions of 
$\text{I}(r)$ and $\text{A}(r)$, 
the authors also use the <code>queue</code> example. 
At the top of page 477, it reads:</p>

<blockquote>
  <p>Let $r$ be the rep value after this history. 
  Because $\beta$'s <code>Enq</code> operation has returned, 
  $\text{A}(r)$ <strong>must</strong> reflect $\beta$'s <code>Enq</code>. 
  Because $\alpha$'s <code>Enq</code> operation is still in progress, 
  $\text{A}(r)$ may or may not reflect $\alpha$'s <code>Enq</code>, 
  <strong>depending on</strong> how $\text{A}$ is defined.</p>
</blockquote></li>
</ul>

<p>(Note that I have used $\alpha, \beta$ instead of 
$A, B$ to denote the processes, to avoid symbol abuses.)
According to this argument, 
I suppose that there are some constraints on the definition of $\text{A}$. 
But what are they?</p>

<pl.programming-languages><dc.distributed-comp><concurrency><program-verification><formal-methods>
Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]
hengxin
# Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

(Asked by: username_0 on 2015-11-23)

In Section 4.3.2 entitled "Proof Method" of

* Herlihy and Wing, "[Linearizability: A Correctness Condition for Concurrent Objects](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)", 1990

the authors describe the technique for
verifying implementations of linearizable objects as follows:

> Assume that the implementation of $r$ is correct,
> hence $\text{H} \mid {\small \text{REP}}$ is linearizable
> for all $\text{H}$ in the implementation.
> Our verification technique focuses on showing the following property
> (denoted $\mathcal{P}$ for later reference, by myself):
> $$\text{For all } r \in \text{Lin}(\text{H}\mid{\small\text{REP}}), \text{I}(r)
> \text{ holds and } \text{A}(r) \subseteq
> \text{Lin}(\text{H}\mid{\small\text{ABS}}).$$
> This condition implies that $\text{Lin}(\text{H} \mid {\small \text{ABS}})$
> is nonempty, hence that $\text{H} \mid {\small \text{ABS}}$ is linearizable.

I don't understand:

> Why is it *sufficient* to show that $\text{A}(r) \subseteq
> \text{Lin}(\text{H}\mid{\small\text{ABS}})$ (besides the "invariant" $\text{I}(r)$ property)
> holds for the verification purpose?

Specifically, to show the property $\mathcal{P}$,
are we showing that there **exists** an $\text{I}(r)$ and an $\text{A}(r)$
such that $\mathcal{P}$ holds?
If so, why cannot we just set $\text{I}(r) = \top$ and $\text{A}(I) = \emptyset$
which trivially satisfy $\mathcal{P}$?
If not, what is the formal definition of "verification" here?

---

### About examples in this paper:

* Section 4.3.3: in the `queue` example,
  $\text{I}(r)$ and $\text{A}(I)$ are far from trivial.  
  What are the specifications that prevent us from choosing
  $\text{A}(I) = \emptyset$ in this example?
* Section 4.2: to motivate their definitions of
  $\text{I}(r)$ and $\text{A}(r)$,
  the authors also use the `queue` example.
  At the top of page 477, it reads:

  > Let $r$ be the rep value after this history.
  > Because $\beta$'s `Enq` operation has returned,
  > $\text{A}(r)$ **must** reflect $\beta$'s `Enq`.
  > Because $\alpha$'s `Enq` operation is still in progress,
  > $\text{A}(r)$ may or may not reflect $\alpha$'s `Enq`,
  > **depending on** how $\text{A}$ is defined.

(Note that I have used $\alpha, \beta$ instead of
$A, B$ to denote the processes, to avoid symbol abuses.)
According to this argument,
I suppose that there are some constraints on the definition of $\text{A}$.
But what are they?

**Tags:** pl.programming-languages, dc.distributed-comp, concurrency, program-verification, formal-methods


---

## 1 answers

### Answer by username_1 on 2015-11-24. Score: 1

Herlihy and Wing write on p. 477:

> In conclusion, the rep invariant $\mathbf{I}$ must be continually satisfied and the abstraction function continually defined, not only between abstract operations, but also between rep operations implementing abstract operations. The abstraction function maps each rep value to a nonempty set of abstract values:
> $$
> \mathbf{A}: \mathrm{REP} \to 2^{\mathrm{ABS}}
> $$

I am tempted to read into this that even when an abstract operation is implemented by a sequence of multiple rep operations, the rep invariant has to hold after each of those rep operations, and when it holds, then the rep value must have at least one abstract counterpart.

Many people have addressed some of the challenges posed in this paper. One of the more interesting and recent developments is R Jagadeesan and J Riely's *Quantitative Quiescent Consistency* [<http://arxiv.org/abs/1402.4043>].

> **Comments:**
> **username_0**: Thanks. However it does not answer my questions on *verification techniques*. Could you please make it more specific?  

---

