# Proof strategies for linearizability of implementations

Background:

In section 4.2 of the paper Linearizable Implementations Do Not Suffice for Randomized Distributed Computation@STOC'2011, the authors mentioned two typical proof strategies for linearizability of implementations. In the following, Let $O$ be the implemented object and let $H$ be a history over $O$.

In one proof strategy, for each operation $op$ on $O$ a unique "linearization point" $pt(op)$ is assigned, which is a shared memory operation that occurs during the execution of operation $op$. A sequential history $S$ is formed by ordering the operations on $O$ in $H$ so that $op_1$ precedes $op_2$ in $S$ if and only if $pt (op_1) \prec_{H} pt (op_2)$. The construction of $S$ guarantees agreement with the "happens before" order of operations on $O$ in $H$, and so the proof obligation for linearizability is only to show that $S$ is valid for $O$.

In the second general proof strategy, the operations in a history $H$ are first ordered somehow into a valid sequence $S$, and the proof obligation is to show that $S$ is consistent with the "happens before" order of $H$.

For instance, the practical constructions of sets and lists such as the "FineList", "OptimisticList", and "LazyList" described by Herlihy and Shavit in their book "The Art of Multiprocessor Programming" fall into the first category while the classic construction of atomic snapshot object and the implementation of atomic multi-writer register from atomic single-writer ones are in the second category.

My problems here are as follows:

1. Are there some implementations in the literature whose linearizability can be proved by both of the above-mentioned proof strategies? Such examples may be useful to help people understand and compare these two proof strategies better.
2. Are there any other proof strategies for linearizability used in the literature? It need not be general and can be specific to its particular problem.
• @D.W. Thanks for your attention. I am not familiar with the notion of linearizability and proof of it. Basically, I want to learn from examples. Especially, I am seeking for such an example that both the proof strategies mentioned in the post are applicable. I also want to see other proof strategies. I have tried to edit my problems. – hengxin Feb 21 '14 at 2:23
• Thanks, hengxin! Looks like a nice question. I hope someone is able to help you. – D.W. Feb 21 '14 at 7:21
• – Raphael Feb 21 '14 at 10:31
• @Raphael Yes, they are. And both of them are my questions. I am working on such topics and want to understand linearizability and its proof from different perspectives. Hope they are not considered duplicated. Thanks. – hengxin Feb 21 '14 at 11:00
• @hengxin No worries, I just wanted to create the links for others' reference. – Raphael Feb 21 '14 at 11:43