Commit 3f33781f authored by Ralf Jung's avatar Ralf Jung

more logatom case studies

parent 193241d0
Pipeline #19045 failed with stage
in 16 minutes and 8 seconds
......@@ -53,8 +53,11 @@ This repository contains the following case studies:
* [logrel_heaplang](theories/logrel_heaplang): A unary logical relation for
semantic typing of heap lang.
* [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
- Elimination Stack
- Treiber Stack (by Zhen Zhang)
- Elimination Stack (by Ralf Jung)
- Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf)) and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf)) (by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy)
- [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)
- Atomic Snapshot (by Marianna Rapoport)
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre)
- Flat Combiner (by Zhen Zhang, also see [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs))
* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
algorithm by Amin Timany.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment