jepsen-io / knossos

Verifies the linearizability of experimentally accessible histories.
398 stars 31 forks source link

Knossos seems to fail linearizable results #13

Closed gator1 closed 7 years ago

gator1 commented 7 years ago

The jepsen linearizable test fails for the attached history. But, I don't see anything wrong. ** history.txt results.edn.txt

**

0 :invoke :cas [4 0] 0 :ok :cas [4 0] 0 :invoke :write 4 0 :ok :write 4 3 :invoke :cas [4 2] 1 :invoke :write 0 1 :ok :write 0 3 :ok :cas [4 2] 3 :invoke :read nil 3 :ok :read 2 2 :invoke :write 1 2 :ok :write 1 :nemesis :info :start nil 2 :invoke :read nil 1 :invoke :read nil 2 :ok :read 1

knossos says the process 3 "can't read 2 from register 0"

aphyr commented 7 years ago

(We discussed this via email; the history is nonlinearizable)