jepsen-io / knossos

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

Visualization fails on latest master with README example #23

Open andrewjstone opened 6 years ago

andrewjstone commented 6 years ago

I get the following when trying to run the example in the README. I'm on Ubuntu 17.10 with oracle jdk 9. I also tried on OSX previously and got the same thing.

knossos.cli=> (def h (read-history "data/cas-register/bad/rethink-fail-minimal.edn"))
#'knossos.cli/h
knossos.cli=> (pprint h)
[{:process 0, :type :invoke, :f :write, :value 0, :index nil}
 {:process 0, :type :ok, :f :write, :value 0, :index nil}
 {:process 1, :type :invoke, :f :read, :value nil, :index nil}
 {:process 2, :type :invoke, :f :write, :value 4, :index nil}
 {:process 1, :type :ok, :f :read, :value 3, :index nil}
 {:process 2, :type :ok, :f :write, :value 4, :index nil}
 {:process 3, :type :invoke, :f :read, :value nil, :index nil}
 {:process 3, :type :ok, :f :read, :value 4, :index nil}]
nil
knossos.cli=> (def a (competition/analysis (model/cas-register) h))
#'knossos.cli/a
knossos.cli=> a
{:valid? false, :configs ({:model #knossos.model.CASRegister{:value 0}, :last-op {:process 0, :type :ok, :f :write, :value 0, :index 1}, :pending [{:process 1, :type :invoke, :f :read, :value 3, :index 2} {:process 2, :type :invoke, :f :write, :value 4, :index 3}]}), :final-paths #{[{:op {:process 0, :type :ok, :f :write, :value 0, :index 1}, :model #knossos.model.CASRegister{:value 0}} {:op {:process 2, :type :invoke, :f :write, :value 4, :index 3}, :model #knossos.model.CASRegister{:value 4}} {:op {:process 1, :type :ok, :f :read, :value 3, :index 4}, :model #knossos.model.Inconsistent{:msg "can't read 3 from register 4"}}] [{:op {:process 0, :type :ok, :f :write, :value 0, :index 1}, :model #knossos.model.CASRegister{:value 0}} {:op {:process 1, :type :ok, :f :read, :value 3, :index 4}, :model #knossos.model.Inconsistent{:msg "can't read 3 from register 0"}}]}, :previous-ok {:process 0, :type :ok, :f :write, :value 0, :index 1}, :last-op {:process 0, :type :ok, :f :write, :value 0, :index 1}, :op {:process 1, :type :ok, :f :read, :value 3, :index 4}}
knossos.cli=> (pprint a)
{:valid? false,
 :configs
 ({:model {:value 0},
   :last-op {:process 0, :type :ok, :f :write, :value 0, :index 1},
   :pending
   [{:process 1, :type :invoke, :f :read, :value 3, :index 2}
    {:process 2, :type :invoke, :f :write, :value 4, :index 3}]}),
 :final-paths
 #{[{:op {:process 0, :type :ok, :f :write, :value 0, :index 1},
     :model {:value 0}}
    {:op {:process 2, :type :invoke, :f :write, :value 4, :index 3},
     :model {:value 4}}
    {:op {:process 1, :type :ok, :f :read, :value 3, :index 4},
     :model {:msg "can't read 3 from register 4"}}]
   [{:op {:process 0, :type :ok, :f :write, :value 0, :index 1},
     :model {:value 0}}
    {:op {:process 1, :type :ok, :f :read, :value 3, :index 4},
     :model {:msg "can't read 3 from register 0"}}]},
 :previous-ok {:process 0, :type :ok, :f :write, :value 0, :index 1},
 :last-op {:process 0, :type :ok, :f :write, :value 0, :index 1},
 :op {:process 1, :type :ok, :f :read, :value 3, :index 4}}
nil
knossos.cli=> (require '[knossos.linear.report :as report])
nil
knossos.cli=> (report/render-analysis! h a "linear.svg")

AssertionError Assert failed: No invocation for op {:process 0, :type :ok, :f :write, :value 0, :index 1}
inv  knossos.linear.report/time-coords/fn--5148 (report.clj:186)
knossos.cli=> 
leapsky commented 5 years ago

Hi Andrew,

did you manage to solve this issue?

andrewjstone commented 5 years ago

Nope. I was just playing around at the time. I never dug in deep.

millennium-falcon42 commented 5 years ago

come across this thing too.

aphyr commented 5 years ago

This might just be a bad history which needs to be re-written; looks like there's no invoke op for that particular ok.