`linearizable` calls `step` in invalid states?

[stevana]

I'm confused about why checker/linearizable calls step in models that are not in the set of valid models produced by applying reduce step model to the set of prefixes of the history.

Here's an example:

(defrecord TurnstileModel [state]
  Model
  (step [_model op]
    (case (:f op)
      :coin (if (= state :locked)
              (TurnstileModel. :unlocked)
              (assert false "never happens"))
      :push (if (= state :unlocked)
              (TurnstileModel. :locked)
              (assert false "also never happens")))))

(deftest linearizeable-stepping-non-prefixes
  (let [model (TurnstileModel. :locked)
        history [{:process 0, :type :invoke, :f :coin}
                 {:process 0, :type :ok,     :f :coin}
                 {:process 0, :type :invoke, :f :push}
                 {:process 0, :type :ok,     :f :push}]]

    (testing "reduce"
      (let [history' (filter op/ok? history)
            result   (reduce model/step model history')]
        (is (not (model/inconsistent? result)) (str result))))

    (testing "linearizable"
      (let [result (checker/check
                    (checker/linearizable {:model model})
                    {}
                    history
                    {})]

        (is (:valid? result))))))

The first test using reduce succeeds as expected, but the second using linarizable fails with the error java.lang.AssertionError: Assert failed: also never happens.

I don't see why step (TurnstileModel. :locked) {:f :push} is ever called, given that there is no prefix of the history in which we would end up in that state?

[aphyr]

The short answer is that models aren't supposed to throw; you should return a (model/inconsistent ...) when asked to perform an inconsistent state transition.

The deeper answer is that Knossos performs some optimization techniques to try and make traversal of the search space more efficient, and one of those techniques is speculatively exploring all possible states and transitions between them (up to some limit), and condensing those states into a compact pointer graph. It's significantly friendlier to cache, since we re-use the same immutable objects constantly rather than constructing new ones, and means we don't actually have to call step at all during the search process; all your arbitrary step logic essentially gets compiled into an in-memory DAG between enumerated states.

[stevana]

Thanks for the explanation!