search

advancedtelematic / quickcheck-state-machine

Test monadic programs using state machine based models
Other
203 stars 25 forks source link

Improving the linearisability checker #120

Open stevana opened 7 years ago

stevana commented 7 years ago

Some links:

We should also think about incomplete histories...

stevana commented 7 years ago

To address the performance problem, we added a new algorithm to Knossos, based on Lowe, Horn and Kroening’s refinement of Wing & Gong’s algorithm for verifying linearizability. Following Lowe’s approach, we apply both Lowe’s just-in-time graph search (already a part of Knossos) and Wing & Gong’s backtracking search in parallel, and use whichever strategy terminates first. This led to dramatic speedups—two orders of magnitude—in verifying Tendermint histories.

Quoted from: https://jepsen.io/analyses/tendermint-0-10-2

stevana commented 6 years ago

https://github.com/rystsov/fast-jepsen

stevana commented 4 years ago

Concurrent Specifications Beyond Linearizability: