From 454dd3328c330a9fe9d0a4f8b70b2ee86f1f7cc5 Mon Sep 17 00:00:00 2001 From: Sergey Bronnikov Date: Fri, 22 Apr 2022 11:39:12 +0300 Subject: [PATCH] src: add a checker for comments test Closes #32 --- CHANGELOG.md | 2 + README.md | 28 +++++++++++ histories/custom/comments.edn | 10 ++++ src/elle_cli/cli.clj | 6 +++ src/elle_cli/comments.clj | 88 +++++++++++++++++++++++++++++++++++ test.sh | 2 + 6 files changed, 136 insertions(+) create mode 100644 histories/custom/comments.edn create mode 100644 src/elle_cli/comments.clj diff --git a/CHANGELOG.md b/CHANGELOG.md index 09c3a49..ec65c56 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,8 @@ change log follows the conventions of ### Added +- Add a checker for comments test (#32). + ### Fixed - Fixed defaults for anomalies in a README. diff --git a/README.md b/README.md index 582f259..03da020 100644 --- a/README.md +++ b/README.md @@ -271,6 +271,34 @@ Example of history: {:type :invoke, :f :release, :process 0, :time 679093895, :index 10} ``` +### custom-comments + +A custom checker for a comments histories. + +Imagine an application which has a sequential stream of comments. Users make +comments by inserting new rows into a table. Because each request is +load-balanced to a different server, two transactions from the same user may +execute on different nodes. Now imagine that a user makes a comment `C1` in +transaction `T1`. `T1` completes successfully. The user then realizes they made +a mistake, and posts a correction comment `C2`, in transaction `T2`. Meanwhile, +someone attempts to read all comments in a third transaction `T3`, concurrent +with both `T1` and `T2`. + +Example of history: + +```clojure +{:index 1, :type :invoke :f :read :value nil} +{:index 2, :type :invoke :f :write :value 425} +{:index 3, :type :ok :f :write :value 425} +{:index 4, :type :invoke :f :write :value 430} +{:index 5, :type :ok :f :write :value 430} +{:index 6, :type :ok :f :read :value #{2 10 15 20 34 35 38 42 43 47 51 53 59 61 71 72 82 88 89 + 113 119 123 129 132 145 146 163 167 176 206 216 224 230 + 238 243 244 255 260 292 294 299 312 316 324 325 327 330 + 350 356 359 360 361 363 366 367 371 376 403 410 419 422 + 430}} +``` + ## License Copyright © 2021-2022 Sergey Bronnikov diff --git a/histories/custom/comments.edn b/histories/custom/comments.edn new file mode 100644 index 0000000..25d9226 --- /dev/null +++ b/histories/custom/comments.edn @@ -0,0 +1,10 @@ +{:index 1, :type :invoke :f :read :value nil} +{:index 2, :type :invoke :f :write :value 425} +{:index 3, :type :ok :f :write :value 425} +{:index 4, :type :invoke :f :write :value 430} +{:index 5, :type :ok :f :write :value 430} +{:index 6, :type :ok :f :read :value #{2 10 15 20 34 35 38 42 43 47 51 53 59 61 71 72 82 88 89 + 113 119 123 129 132 145 146 163 167 176 206 216 224 230 + 238 243 244 255 260 292 294 299 312 316 324 325 327 330 + 350 356 359 360 361 363 366 367 371 376 403 410 419 422 + 430}} diff --git a/src/elle_cli/cli.clj b/src/elle_cli/cli.clj index 3652983..2fe750e 100644 --- a/src/elle_cli/cli.clj +++ b/src/elle_cli/cli.clj @@ -10,6 +10,7 @@ [jepsen [checker :as jepsen-model]] [jepsen.tests.bank :as jepsen-bank] [jepsen.tests.long-fork :as jepsen-long-fork] + [elle-cli.comments :as comments-model] [elle.list-append :as elle-list-append] [elle.rw-register :as elle-rw-register] [elle.consistency-model :as elle-consistency-model] @@ -80,6 +81,7 @@ "jepsen-counter" jepsen-model/counter "jepsen-set" jepsen-model/set "jepsen-set-full" jepsen-model/set-full + "custom-comments" comments-model/checker "elle-rw-register" elle-rw-register/check "elle-list-append" elle-list-append/check}) @@ -157,6 +159,7 @@ " knossos-register - a Knossos checker for write-read registers." " knossos-cas-register - a Knossos checker for CAS (Compare-And-Set) registers." " knossos-mutex - a Knossos checker for a mutex histories." + " custom-comments - a custom checker for a comments histories." "" "Options:" options-summary @@ -171,6 +174,9 @@ (case checker-group "knossos" (competition/analysis (checker-fn) history) "elle" (checker-fn options history) + "custom" (case model-name + "custom-comments" (checker-fn) + ) "jepsen" (case model-name "jepsen-bank" (jepsen-model/check-safe (checker-fn {:negative-balances? true}) nil history) "jepsen-set-full" (jepsen-model/check-safe (checker-fn) nil history) diff --git a/src/elle_cli/comments.clj b/src/elle_cli/comments.clj new file mode 100644 index 0000000..3b9edd0 --- /dev/null +++ b/src/elle_cli/comments.clj @@ -0,0 +1,88 @@ +(ns elle-cli.comments + "Checks for a strict serializability anomaly in which T1 < T2, but T2 is + visible without T1. + We perform concurrent blind inserts across n tables, and meanwhile, perform + reads of both tables in a transaction. To verify, we replay the history, + tracking the writes which were known to have completed before the invocation + of any write w_i. If w_i is visible, and some w_j < w_i is *not* visible, + we've found a violation of strict serializability. + Splits keys up onto different tables to make sure they fall in different + shard ranges" + (:require [jepsen.checker :as checker] + [knossos.model :as model] + [knossos.op :as op])) + +(defprotocol Checker + (check [checker test history opts] + "Verify the history is correct. Returns a map like + {:valid? true} + or + {:valid? false + :some-details ... + :failed-at [details of specific operations]} + Opts is a map of options controlling checker execution. Keys include: + :subdirectory - A directory within this test's store directory where + output files should be written. Defaults to nil.")) + +(defn checker + "An empty checker that only returns nil." + [] + (reify Checker + (check [_ _ _ _]))) + +(comment +; Source: https://github.com/jepsen-io/jepsen/blob/main/cockroachdb/src/jepsen/cockroach/comments.clj +(defn checker + [] + (reify Checker + (check [this test model history opts] + ; Determine first-order write precedence graph + (let [expected (loop [completed (sorted-set) + expected {} + [op & more :as history] history] + (cond + ; Done + (not (seq history)) + expected + + ; We know this value is definitely written + (= :write (:f op)) + (cond ; Write is beginning; record precedence + (op/invoke? op) + (recur completed + (assoc expected (:value op) completed) + more) + + ; Write is completing; we can now expect to see + ; it + (op/ok? op) + (recur (conj completed (:value op)) + expected more) + + true + (recur completed expected more)) + + true + (recur completed expected more))) + errors (->> history + (r/filter op/ok?) + (r/filter #(= :read (:f %))) + (reduce (fn [errors op] + (let [seen (:value op) + our-expected (->> seen + (map expected) + (reduce set/union)) + missing (set/difference our-expected + seen)] + (if (empty? missing) + errors + (conj errors + (-> op + (dissoc :value) + (assoc :missing missing) + (assoc :expected-count + (count our-expected))))))) + []))] + {:valid? (empty? errors) + :errors errors})))) +) diff --git a/test.sh b/test.sh index 4aa84cf..148a647 100755 --- a/test.sh +++ b/test.sh @@ -38,3 +38,5 @@ $ELLE_CLI_BIN $ELLE_CLI_OPT jepsen-set-full histories/jepsen/set_full.json $ELLE_CLI_BIN $ELLE_CLI_OPT jepsen-bank histories/jepsen/bank.edn $ELLE_CLI_BIN $ELLE_CLI_OPT jepsen-bank histories/jepsen/bank.json + +$ELLE_CLI_BIN $ELLE_CLI_OPT custom-comments histories/custom/comments.edn