Add a checker for sequential test

Closes #33

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
 

README.md

@@ -299,6 +299,25 @@ Example of history:
                                            430}}
 ```
 
+### custom-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

src/elle_cli/cli.clj

@@ -11,6 +11,7 @@
             [jepsen.tests.bank :as jepsen-bank]
             [jepsen.tests.long-fork :as jepsen-long-fork]
             [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]
@@ -82,6 +83,7 @@
    "jepsen-set"              jepsen-model/set
    "jepsen-set-full"         jepsen-model/set-full
    "custom-comments"         comments-model/checker
+   "custom-sequential"       sequential-model/checker
    "elle-rw-register"        elle-rw-register/check
    "elle-list-append"        elle-list-append/check})
 
@@ -160,6 +162,7 @@
         "  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."
+        "  custom-sequential - a custom checker for sequential histories."
         ""
         "Options:"
         options-summary
@@ -176,6 +179,7 @@
        "elle" (checker-fn options history)
        "custom" (case model-name
                   "custom-comments" (checker-fn)
+                  "custom-sequential" (checker-fn)
                  )
        "jepsen" (case model-name
                   "jepsen-bank" (jepsen-model/check-safe (checker-fn {:negative-balances? true}) nil history)

src/elle_cli/sequential.clj

@@ -0,0 +1,114 @@
+(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]))
+
+; 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
+(defn checker
+  []
+  (reify checker/Checker
+    (check [this test model 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}))))
+
+(comment
+(defn non-monotonic-pairs
+  "Given a history, finds pairs of ops on the same process where the value
+  decreases."
+  [history]
+  (->> history
+       (filter op/ok?)
+       (reduce (fn [[last errs] op]
+                 ; Last is a map of process ids to the last
+                 ; operation we saw for that process. Errs is a
+                 ; collection of error maps.
+                 (let [p          (:process op)
+                       value      (:value op)
+                       last-value (-> (last p) :value (or 0))]
+                   (if (<= last-value value)
+                     ; Monotonic
+                     [(assoc last p op) errs]
+                     ; Non-monotonic!
+                     [(assoc last p op)
+                      (conj errs [(last p) op])])))
+               [{} []])
+       second))
+
+; https://github.com/jepsen-io/jepsen/blob/main/dgraph/src/jepsen/dgraph/sequential.clj
+; Verifies sequentialish consistency by ensuring that each process observes
+; monotonic states.
+; Dgraph provides snapshot isolation, but snapshot isolation allows reads to
+; observe arbitrarily stale values, so long as writes do not conflict. In
+; particular, there is no guarantee that reads will observe logically monotonic
+; states of the system. From https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-95-51.pdf:
+; > ... each transaction reads data from a snapshot of the (committed) data as
+; > of the time the transaction started, called its Start-Timestamp. This time
+; > may be any time before the transaction's first Read.
+; We wish to verify a different sort of property, which I'm going to call
+; *sequential consistency*, but isn't exactly.
+; Sequential implies that there exists a total order of transactions which is
+; consistent with the order on each process. Snapshot isolation, however, does
+; not necessarily admit any totally ordered history; that would require
+; serializability.
+; What we're going to do here is restrict ourselves to transactions of two
+; forms:
+; 1. Read-only transactions
+; 2. Transactions where every read key is also written
+; I would like to argue that this is sufficient to imply serializability, by
+; making hand-waving gestures and muttering about materializing conflicts, and
+; observing that the example of a read-only nonserializable history in
+; https://www.cs.umb.edu/~poneil/ROAnom.pdf requires a transaction which
+; doesn't write its full read set.
+; So, if we allow that a total transaction order *does* exist, then we can
+; construct a transactional analogy for sequential consistency: there exists a
+; total order of transactions which is compatible with the order of
+; transactions on every given process.
+; To check this, we perform two types of transactions on a register: a read
+; transaction, and a read, increment, and write transaction. These are of type
+; 1 and type 2 respectively, so our histories ought to be serializable. Since
+; no transaction can *lower* the value of the register, once a value is
+; observed by a process, that process should observe that value or higher from
+; that point forward.
+; To verify this, we'll record the resulting value of the register in the
+; :value for each operation, and ensure that in each process, those values are
+; monotonic.
+(defn checker
+  "This checks a single register; we generalize it using independent/checker."
+  []
+  (reify checker/Checker
+    (check [_ test history opts]
+      (let [errs (non-monotonic-pairs history)]
+        {:valid? (empty? errs)
+         :non-monotonic errs}))))
+)