quickcheck-state-machine icon indicating copy to clipboard operation
quickcheck-state-machine copied to clipboard

Published 20 hours ago • verified publisher icon advancedtelematic

Improving the linearisability checker

Open stevana opened this issue 8 years ago • 3 comments

Some links:

  • http://www.anishathalye.com/2017/06/04/testing-distributed-systems-for-linearizability/
  • https://github.com/anishathalye/porcupine
  • https://github.com/ahorn/linearizability-checker

We should also think about incomplete histories...

stevana avatar Jun 20 '17 13:06 stevana

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 avatar Sep 06 '17 11:09 stevana

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

stevana avatar Aug 20 '18 14:08 stevana

Concurrent Specifications Beyond Linearizability:

  • http://drops.dagstuhl.de/opus/volltexte/2018/10088/pdf/LIPIcs-OPODIS-2018-28.pdf
  • http://personal.strath.ac.uk/jeremy.ledent/slides_OPODIS.pdf

stevana avatar Nov 06 '19 09:11 stevana