commit c660bce8c10041aa3353f4fb8269eca7f3ffb228 from: Sergey Bronnikov date: Tue Jul 12 15:07:03 2022 UTC Add a checker for sequential test Closes #33 commit - 935da4cf63a9fdc003fd51b77be4fea1c33f68e0 commit + c660bce8c10041aa3353f4fb8269eca7f3ffb228 blob - ba7df2ad31b35228e20e3575bbe3f79b786b0d33 blob + fd7011ff02cfab1b505d595cf052b1f886539c6a --- CHANGELOG.md +++ CHANGELOG.md @@ -11,6 +11,7 @@ change log follows the conventions of ### Added - Add a checker for comments test (#32). +- Add a checker for sequential test (#33). ### Fixed blob - 5dc3aff3d137de29ce45ed31cc7b63eacbca6f14 blob + 2462bda7d76c2ee5075c579ccde2dcf285a4dc7a --- README.md +++ README.md @@ -372,7 +372,26 @@ Example of history: 350 356 359 360 361 363 366 367 371 376 403 410 419 422 430}} ``` + +### sequential +A standalone checker for a sequential consistency, it checks that the effective +order of transactions should be consistent with the order on every client. Any +execution is the same as if all `read` and `write` ops were executed in some +global ordering, and the ops of each client process appear in the order +specified by its program. If a process order enforces that `x` must be visible +before `y`, we should always read both or neither. + +To verify this, we have a single client perform a sequence of independent +transactions, inserting `k1`, `k2`, ..., `kn` into different tables. +Concurrently, a different client attempts to read each of `kn`, ..., `k2`, `k1` +in turn. Because all inserts occur from the same process, they must also be +visible to any single process in that order. This implies that once a process +observes `kn`, any subsequent read must see `kn − 1`, and by induction, all +smaller keys. + +Like G2 and the bank tests, this test does not verify consistency *in general*. + ## License Copyright © 2021-2022 Sergey Bronnikov blob - 8e1b83e0db2ba7d1f94ab8432d48ac3048b2292c blob + 4251b1a28d2c23839abdd02bd63545c607f7a88b --- src/elle_cli/cli.clj +++ src/elle_cli/cli.clj @@ -13,6 +13,7 @@ [jepsen.tests.long-fork :as jepsen-long-fork] [jepsen.independent :as independent] [elle-cli.comments :as comments-model] + [elle-cli.sequential :as sequential-model] [elle.list-append :as elle-list-append] [elle.rw-register :as elle-rw-register] [elle.consistency-model :as elle-consistency-model] @@ -89,6 +90,7 @@ "set" jepsen-model/set "set-full" jepsen-model/set-full "comments" comments-model/checker + "sequential" sequential-model/checker "elle-rw-register" elle-rw-register/check "elle-list-append" elle-list-append/check "rw-register" elle-rw-register/check @@ -168,6 +170,7 @@ " 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)." + " sequential - a custom checker for sequential histories (experimental)." "" "Options:" options-summary @@ -189,6 +192,7 @@ "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)) + "sequential" ((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 + 3645ec884b232d7cb3706ccbad009cf483fd8f37 (mode 644) --- /dev/null +++ src/elle_cli/sequential.clj @@ -0,0 +1,56 @@ +(ns elle-cli.sequential + "A sequential consistency test. + Verify that client order is consistent with DB order by performing queries + (in four distinct transactions) like: + A: insert x + A: insert y + B: read y + B: read x + A's process order enforces that x must be visible before y, so we should + always read both or neither. + Splits keys up onto different tables to make sure they fall in different + shard ranges." + (:require [jepsen [checker :as checker] + [independent :as independent]] + [knossos.model :as model] + [knossos.op :as op] + [clojure.core.reducers :as r])) + +(defn trailing-nil? + "Does the given sequence contain a nil anywhere after a non-nil element?" + [coll] + (some nil? (drop-while nil? coll))) + +(defn subkeys + "The subkeys used for a given key, in order." + [key-count k] + (mapv (partial str k "_") (range key-count))) + +; https://jepsen.io/consistency/models/sequential +; https://github.com/jepsen-io/jepsen/blob/main/cockroachdb/src/jepsen/cockroach/sequential.clj +; https://github.com/jepsen-io/jepsen/blob/main/tidb/src/tidb/sequential.clj +; https://github.com/jepsen-io/jepsen/blob/main/dgraph/src/jepsen/dgraph/sequential.clj +(defn checker + "A sequential consistency checker." + [] + (reify checker/Checker + (check [this test history opts] + (assert (integer? (:key-count test))) + (let [reads (->> history + (r/filter op/ok?) + (r/filter #(= :read (:f %))) + (r/map :value) + (into [])) + none (filter (comp (partial every? nil?) second) reads) + some (filter (comp (partial some nil?) second) reads) + bad (filter (comp trailing-nil? second) reads) + all (filter (fn [[k ks]] + (= (subkeys (:key-count test) k) + (reverse ks))) + reads)] + {:valid? (not (seq bad)) + :all-count (count all) + :some-count (count some) + :none-count (count none) + :bad-count (count bad) + :bad bad}))))