Verifying Optimistic Algorithms Should Be Easy

Highly-concurrent optimistic algorithms are notoriously hard to verify. In particular, verifying that an optimistic algorithm is linearizable is quite challenging. Given a highly-concurrent algorithm, the goal is to find a proof that captures its designer's intuition as to why the algorithm works. The paper believes that simple and intuitive proofs can, and should, be obtained by embracing the spirit in which these algorithms are written. This paper shows that the intuition behind many optimistic concurrent algorithm can be naturally captured using global invariants, a la Lamprot, of a particular class: In this class, observations regarding the local state of a thread are completely separated from observations regarding either the local states of other threads or the global state.