hayounav/linearizability

Use this repo to explore linearizability, using the concurrent counter as a toy problem

Linearizable Objects

The purpose of this repo to explore linearizability, using the concurrent data types, such as counter and snapshot data structures, as toy problems on which to test ideas.

Implemetations

Eventually, there should be proofs of the linearizability of the counter in at least:

• Z3 - https://github.com/Z3Prover/z3
• Lean - https://leanprover.github.io/
• Prolog - http://www.swi-prolog.org/ (this might not happen)

Optimally, the wiki pages of this repo will be used to record insights and ideas with which we come up along the way.

Coding environments

emacs

• Z3- https://github.com/zv/z3-mode
• Lean - https://github.com/leanprover/lean/tree/master/src/emacs