Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

Question

In Section 4.3.2 entitled "Proof Method" of

• Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 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?

Answer 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].