commit 935da4cf63a9fdc003fd51b77be4fea1c33f68e0 from: Sergey Bronnikov date: Tue Jul 12 14:42:33 2022 UTC Add a checker for comments test Closes #32 commit - d9145d2205e8e2ad30b16fed056ac6ec2fef975f commit + 935da4cf63a9fdc003fd51b77be4fea1c33f68e0 blob - a15798d24b6a96656156d3f698b50625fadf7f86 blob + ba7df2ad31b35228e20e3575bbe3f79b786b0d33 --- CHANGELOG.md +++ CHANGELOG.md @@ -10,6 +10,8 @@ change log follows the conventions of ### Added +- Add a checker for comments test (#32). + ### Fixed ### Changed blob - 90ed5e5317ab4f0634ba0d51e6d7b20ed0b77920 blob + 5dc3aff3d137de29ce45ed31cc7b63eacbca6f14 --- README.md +++ README.md @@ -343,6 +343,34 @@ Example of history: {:type :fail, :f :release, :process 1, :time 585478186, :error :not-held, :index 8} {:type :invoke, :f :acquire, :process 2, :time 584335820, :index 9} {:type :invoke, :f :release, :process 0, :time 679093895, :index 10} +``` + +### 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 blob - /dev/null blob + 25d9226b5dee1f3e06c9a29e1dc79fafd68a79e9 (mode 644) --- /dev/null +++ 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}} blob - 5eea0a12126c46cf45b32c593d6ca85552dedf70 blob + 8e1b83e0db2ba7d1f94ab8432d48ac3048b2292c --- src/elle_cli/cli.clj +++ src/elle_cli/cli.clj @@ -11,6 +11,8 @@ [jepsen [checker :as jepsen-model]] [jepsen.tests.bank :as jepsen-bank] [jepsen.tests.long-fork :as jepsen-long-fork] + [jepsen.independent :as independent] + [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] @@ -86,6 +88,7 @@ "counter" jepsen-model/counter "set" jepsen-model/set "set-full" jepsen-model/set-full + "comments" comments-model/checker "elle-rw-register" elle-rw-register/check "elle-list-append" elle-list-append/check "rw-register" elle-rw-register/check @@ -164,6 +167,7 @@ " long-fork - a checker for an anomaly in parallel snapshot isolation." " cas-register - a checker for CAS (Compare-And-Set) registers." " mutex - a checker for a mutex histories." + " comments - a custom checker for a comments histories (experimental)." "" "Options:" options-summary @@ -184,6 +188,7 @@ "knossos-register" (competition/analysis (checker-fn) (history/parse-ops history)) "knossos-cas-register" (competition/analysis (checker-fn) (history/parse-ops history)) "knossos-mutex" (competition/analysis (checker-fn) (history/parse-ops history)) + "comments" ((independent/checker (checker-fn)) (history/parse-ops history)) "list-append" (checker-fn options history) "rw-register" (checker-fn options history) "elle-list-append" (checker-fn options history) blob - /dev/null blob + d61f41da3c6350da99f1f6a84807272c3cab699b (mode 644) --- /dev/null +++ src/elle_cli/comments.clj @@ -0,0 +1,70 @@ +(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] + [clojure.core.reducers :as r] + [clojure.set :as set])) + +; Source: https://github.com/jepsen-io/jepsen/blob/main/cockroachdb/src/jepsen/cockroach/comments.clj +(defn checker + [] + (reify checker/Checker + (check [this test 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})))) blob - 3e61bc3e913494d72b6043d61345bee864b780c2 blob + 1a66e6dab5d6da626ff342f9272dfe98aad900bc --- test.sh +++ test.sh @@ -60,4 +60,5 @@ run_test 1 "--model set-full histories/jepsen/set_full run_test 1 "--model bank histories/jepsen/bank.edn" run_test 1 "--model bank histories/jepsen/bank.json" + exit $suite_status