Skip to content

Commit

Permalink
Add a checker for sequential test
Browse files Browse the repository at this point in the history
Closes #33
  • Loading branch information
ligurio committed May 3, 2022
1 parent 64c07c4 commit 63be4d3
Show file tree
Hide file tree
Showing 4 changed files with 80 additions and 0 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
19 changes: 19 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -299,6 +299,25 @@ Example of history:
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
Expand Down
4 changes: 4 additions & 0 deletions src/elle_cli/cli.clj
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -87,6 +88,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
Expand Down Expand Up @@ -167,6 +169,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."
" sequential - a custom checker for sequential histories."
""
"Options:"
options-summary
Expand All @@ -188,6 +191,7 @@
"knossos-cas-register" (competition/analysis (checker-fn) (history/parse-ops history))
"knossos-mutex" (competition/analysis (checker-fn) (history/parse-ops history))
"comments" (checker-fn)
"sequential" (checker-fn)
"list-append" (checker-fn options history)
"rw-register" (checker-fn options history)
"elle-list-append" (checker-fn options history)
Expand Down
56 changes: 56 additions & 0 deletions src/elle_cli/sequential.clj
Original file line number Diff line number Diff line change
@@ -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}))))

0 comments on commit 63be4d3

Please sign in to comment.