diff options
author | Alex Auvolat <alex@adnab.me> | 2023-10-20 12:13:11 +0200 |
---|---|---|
committer | Alex Auvolat <alex@adnab.me> | 2023-10-20 12:13:11 +0200 |
commit | 4ba18ce9cca1b828edcf3f8c8770d49c75ed3083 (patch) | |
tree | d277897b498200440f9450d66f77cbacedbf2974 | |
parent | ef662822c9e48ff7cfd9300590617e089c0a9498 (diff) | |
download | garage-4ba18ce9cca1b828edcf3f8c8770d49c75ed3083.tar.gz garage-4ba18ce9cca1b828edcf3f8c8770d49c75ed3083.zip |
jepsen: wip checker for register-like behavior
-rw-r--r-- | script/jepsen.garage/src/jepsen/garage/reg.clj | 66 |
1 files changed, 62 insertions, 4 deletions
diff --git a/script/jepsen.garage/src/jepsen/garage/reg.clj b/script/jepsen.garage/src/jepsen/garage/reg.clj index f3d5cec5..b5bf28ff 100644 --- a/script/jepsen.garage/src/jepsen/garage/reg.clj +++ b/script/jepsen.garage/src/jepsen/garage/reg.clj @@ -1,6 +1,7 @@ (ns jepsen.garage.reg (:require [clojure.tools.logging :refer :all] [clojure.string :as str] + [clojure.set :as set] [jepsen [checker :as checker] [cli :as cli] [client :as client] @@ -20,7 +21,7 @@ [slingshot.slingshot :refer [try+]])) (defn op-get [_ _] {:type :invoke, :f :read, :value nil}) -(defn op-put [_ _] {:type :invoke, :f :write, :value (str (rand-int 9))}) +(defn op-put [_ _] {:type :invoke, :f :write, :value (str (rand-int 99))}) (defn op-del [_ _] {:type :invoke, :f :write, :value nil}) (defrecord RegClient [creds] @@ -47,15 +48,72 @@ (teardown! [this test]) (close! [this test])) +(defn reg-read-after-write + "Read-after-Write checker for register operations" + [] + (reify checker/Checker + (check [this test history opts] + (let [init {:put-values {-1 nil} + :put-done #{-1} + :put-in-progress {} + :read-can-contain {} + :bad-reads #{}} + final (reduce + (fn [state op] + (let [current-values (set/union + (set (map (fn [idx] (get (:put-values state) idx)) (:put-done state))) + (set (map (fn [[_ [idx _]]] (get (:put-values state) idx)) (:put-in-progress state)))) + read-can-contain (reduce + (fn [rcc [idx v]] (assoc rcc idx (set/union current-values v))) + {} (:read-can-contain state))] + (info "--------") + (info "state: " state) + (info "current-values: " current-values) + (info "read-can-contain: " read-can-contain) + (info "op: " op) + (case [(:type op) (:f op)] + ([:invoke :write]) + (assoc state + :read-can-contain read-can-contain + :put-values (assoc (:put-values state) (:index op) (:value op)) + :put-in-progress (assoc (:put-in-progress state) (:process op) [(:index op) (:put-done state)])) + ([:ok :write]) + (let [[index overwrites] (get (:put-in-progress state) (:process op))] + (assoc state + :read-can-contain read-can-contain + :put-in-progress (dissoc (:put-in-progress state) (:process op)) + :put-done + (conj + (set/difference (:put-done state) overwrites) + index))) + ([:invoke :read]) + (assoc state + :read-can-contain (assoc read-can-contain (:process op) current-values)) + ([:ok :read]) + (let [this-read-can-contain (get read-can-contain (:process op)) + bad-reads (if (contains? this-read-can-contain (:value op)) + (:bad-reads state) + (conj (:bad-reads state) [(:process op) (:index op) (:value op) this-read-can-contain]))] + (info "this-read-can-contain: " this-read-can-contain) + (assoc state + :read-can-contain (dissoc read-can-contain (:process op)) + :bad-reads bad-reads)) + state))) + init history) + valid? (empty? (:bad-reads final))] + (assoc final :valid? valid?))))) + (defn workload "Tests linearizable reads and writes" [opts] {:client (RegClient. nil) :checker (independent/checker (checker/compose - {:linear (checker/linearizable - {:model (model/register) - :algorithm :linear}) + {:reg-read-after-write (reg-read-after-write) + ; linear test is desactivated, indeed Garage is not linear + ;:linear (checker/linearizable + ; {:model (model/register) + ; :algorithm :linear}) :timeline (timeline/html)})) :generator (independent/concurrent-generator 10 |