From 040d9dc46af0e625fcfa22b383cd8aa7aefbbf3f Mon Sep 17 00:00:00 2001 From: Sergey Bronnikov Date: Wed, 9 Sep 2026 17:10:14 +0300 Subject: [PATCH] Validate history/model compatibility before checking Report a clear error when the selected model cannot check a history, instead of failing with an obscure exception from deep inside a checker (e.g. "No matching clause: :append" when running rw-register on a list-append history). Each model now declares the shape of operation rows it supports (model-specs): transactional histories (:f :txn with micro-operations [f k v]) for rw-register/list-append, micro-operation-valued operations for long-fork, and flat scalar operations for the remaining models. Client operations in a history are validated against the requested model before a checker runs; on a mismatch elle-cli prints a clear message to stderr, hints at the correct model, and exits with status 1. Add regression tests covering cross-model mismatches, including rw-register on an append-register history. Fixes #103 --- CHANGELOG.md | 6 ++ src/elle_cli/cli.clj | 146 ++++++++++++++++++++++++++++++++ test/elle_cli/elle_cli_test.clj | 22 +++++ 3 files changed, 174 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6f647fe..17c9b8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,12 @@ change log follows the conventions of ### Fixed +- Validate that a history matches the selected model before + running a checker and report a clear error otherwise, instead + of an obscure exception from deep inside a checker (e.g. when + checking a `list-append` history with the `rw-register` model) + (#103). + [Unreleased]: https://github.com/ligurio/elle-cli/compare/0.1.11...HEAD ## [0.1.11] diff --git a/src/elle_cli/cli.clj b/src/elle_cli/cli.clj index 877a16d..a26bf5a 100644 --- a/src/elle_cli/cli.clj +++ b/src/elle_cli/cli.clj @@ -96,6 +96,141 @@ {"edn" read-edn-history "json" read-json-history}) +(def model-specs + "A description of the operation rows each model can check, used to detect a + mis-selected model before running a checker. Every client operation in a + history must conform to the spec of the requested model: + + :shape The expected shape of an operation row. + - :txn - :f is :txn, :value is a list of micro-operations [f k v]. + - :mops - :f is an operation over lists, and :value is a list of + micro-operations [f k v]. + - :flat - :f is an operation with a scalar (non-transactional) + value. + :f (optional) A set of allowed operation keys. + :mops (optional) A set of allowed micro-operation keys. + + History rows produced by a nemesis (:process :nemesis, e.g. :pause, :resume, + :start, :stop) are not client operations and are ignored, as checkers do." + {"rw-register" {:shape :txn + :mops #{:r :w}} + "list-append" {:shape :txn + :mops #{:r :append}} + "long-fork" {:shape :mops + :f #{:read :write} + :mops #{:r :w}} + "cas-register" {:shape :flat + :f #{:read :write :cas}} + "mutex" {:shape :flat + :f #{:acquire :release}} + "bank" {:shape :flat + :f #{:read :transfer}} + "comments" {:shape :flat + :f #{:read :write}} + "sequential" {:shape :flat + :f #{:add :read}} + "counter" {:shape :flat + :f #{:add :read}} + "set" {:shape :flat + :f #{:add :read}} + "set-full" {:shape :flat + :f #{:add :read}}}) + +(defn mop-rows + "Given an operation, returns its sequence of micro-operation rows [f k v] if + the operation is transactional (:f :txn) or its value is otherwise a list of + micro-operation rows; nil otherwise." + [op] + (let [v (:value op)] + (cond + (= :txn (:f op)) + (when (sequential? v) v) + + (and (sequential? v) + (seq v) + (sequential? (first v)) + (not (map? (first v)))) + v))) + +(defn row-family + "Classifies an operation row as :txn, :mops or :flat." + [op] + (let [f (:f op)] + (cond + (= :txn f) :txn + ; Elle histories often omit the :f :txn key on transaction rows. + (and (nil? f) (mop-rows op)) :txn + (mop-rows op) :mops + :else :flat))) + +(defn shape-str + "A short human description of an operation shape." + [shape] + (case shape + :txn "a transaction (:f :txn) over micro-operations" + :mops "an operation whose :value is a list of micro-operations" + :flat "a non-transactional operation with a scalar value")) + +(defn row-err + "Returns nil if the operation row conforms to the model spec, or a string + describing why the row cannot be checked with that model." + [{:keys [shape f mops]} op] + (let [ix (:index op)] + (cond + ; The row doesn't have the shape this model checks. + (not= shape (row-family op)) + (str "op at :index " ix " is " + (shape-str (row-family op)) + ", but this model expects " + (shape-str shape)) + + ; Flat and micro-operation models restrict operation keys. + (and f (not (contains? f (:f op)))) + (str "op at :index " ix " uses :f " (pr-str (:f op)) + ", which is not supported by this model") + + ; Transactional models restrict keys of micro-operations. + (and mops (mop-rows op)) + (let [bad (first (remove mops (map first (mop-rows op))))] + (when bad + (str "op at :index " ix " contains a micro-operation with key " + (pr-str bad) ", which is not supported by this model"))) + + :else nil))) + +(defn fits-model? + "True if every client operation in the history conforms to the model spec." + [model-name history] + (let [spec (get model-specs model-name)] + (every? #(nil? (row-err spec %)) history))) + +(defn validate-model-ops + "Checks that client operations in a history have the rows the requested + model can check. Throws an informative ex-info if a row does not fit, so a + mis-selected model is reported with a clear error (and a hint about the + right model) instead of an obscure exception deep inside a checker." + [model-name history] + (when-let [spec (get model-specs model-name)] + (let [client-history (h/client-ops history) + bad (first (keep #(row-err spec %) client-history))] + (when bad + (let [candidates (->> (keys model-specs) + (remove #{model-name}) + (filter #(fits-model? % client-history)) + sort) + hint (when (seq candidates) + (str ". This history looks like a " + (str/join " or " (map #(str "\"" % "\"") candidates)) + " workload")) + msg (str "Model \"" model-name "\" does not match this history: " + bad + hint + " - wrong model selected?")] + (throw (ex-info msg + {:model-mismatch true + :model model-name + :candidate-models (vec candidates)}))))))) + (def opts "tools.cli options" @@ -196,6 +331,8 @@ "Check a specified history according to model specified by model name" [model-name history options] + (validate-model-ops model-name history) + (let [checker-fn (get models model-name)] (case model-name ; Operations in a histories passed to a Knossos additionally normalized, @@ -266,6 +403,15 @@ (System/exit ({true 1 false 0} (lazy-contains? (vals @results) false)))) + (catch clojure.lang.ExceptionInfo e + (if (true? (:model-mismatch (ex-data e))) + (do (binding [*out* *err*] + (println (.getMessage e))) + (System/exit 1)) + (do (println) + (.printStackTrace e) + (System/exit 255)))) + (catch Throwable t (println) (.printStackTrace t) diff --git a/test/elle_cli/elle_cli_test.clj b/test/elle_cli/elle_cli_test.clj index 6a57894..1b0784d 100644 --- a/test/elle_cli/elle_cli_test.clj +++ b/test/elle_cli/elle_cli_test.clj @@ -302,3 +302,25 @@ (flush) (testing (str model ": " case " with options " (pr-str opts)) (assert-result model case (check-case model case opts))))) + +(deftest check-model-mismatch + (testing "rw-register cannot check a list-append history" + (is (thrown-with-msg? + clojure.lang.ExceptionInfo + #"list-append" + (check-case "rw-register" "list-append-gh-30")))) + (testing "list-append cannot check a rw-register history" + (is (thrown-with-msg? + clojure.lang.ExceptionInfo + #"rw-register" + (check-case "list-append" "rw-register")))) + (testing "rw-register cannot check a flat cas-register history" + (is (thrown-with-msg? + clojure.lang.ExceptionInfo + #"cas-register" + (check-case "rw-register" "bad-analysis")))) + (testing "cas-register cannot check a transactional rw-register history" + (is (thrown-with-msg? + clojure.lang.ExceptionInfo + #"rw-register" + (check-case "cas-register" "rw-register")))))