Proving Correctness of a Concurrent Data Structure via Logics

Concurrent data structure implementations like stacks, queues, sets, hash-maps and lists are core components of operating system kernels, virtual machines and other platforms that support development and deployment of concurrent applications. These implementations must be both efficient and correct. However, there is a trade-off between the performance and reasoning about the correctness of the concurrent data structure. In order to achieve better performance, concurrent algorithm designers and developers try to allow as much concurrency (interleavings among executions of different processing units) as possible. A program that calls operations of a concurrent library might generate numerous different executions. Then, it is quite easy to miss some executions while reasoning about correctness of a highly concurrent data structure manually. Testing based methods also do not help much because:
i) it is not possible to model every possible client of the data structure,
ii) even a single failure is not tolerable and all behaviours (possible infinite) cannot be generated via tests,
iii) interleavings depend on the scheduler which lies in a lower layer and developers have no control over it.
For these reasons, rigorous mathematical and logical correctness arguments are necessary.

Time-stamped stack[1] (TSS), is a highly concurrent and scalable stack implementation. Like many concurrent data structures, correctness for TSS is proven by showing that the algorithm is linearizable[2]. However, linearizability proofs presented in both the original paper and later works are done in pen and paper style and some are based on some informal arguments. In this project, students are expected to develop a reliable and mechanized correctness (linearizability) proof for the TSS. Here, mechanized means that the proof should be done by using a modern proof assistant software like Coq[3], Lean[4], Boogie[5] or Dafny[6].

References:
1. Mike Dodds, Andreas Haas, Christoph M. Kirsch:
A Scalable, Correct Time-Stamped Stack. POPL 2015: 233-246
2. Maurice Herlihy, Jeannette M. Wing:
Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12(3): 463-492 (1990)
3. https://coq.inria.fr/
4. https://leanprover.github.io/about/
5. https://github.com/boogie-org/boogie
6. https://github.com/dafny-lang/dafny