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

In Section 4.3.2 entitled "Proof Method" of

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?

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}}$$