From 18ee8efb5f7bfcd64bf1a1336ffd6f54574aa79f Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 19 Apr 2023 22:02:03 +0200 Subject: Check read-after-write property for sets --- script/jepsen.garage/src/jepsen/garage/set.clj | 48 +++++++++++++++++++++++--- 1 file changed, 43 insertions(+), 5 deletions(-) (limited to 'script') diff --git a/script/jepsen.garage/src/jepsen/garage/set.clj b/script/jepsen.garage/src/jepsen/garage/set.clj index 156493bc..9b21d50e 100644 --- a/script/jepsen.garage/src/jepsen/garage/set.clj +++ b/script/jepsen.garage/src/jepsen/garage/set.clj @@ -1,10 +1,12 @@ (ns jepsen.garage.set (:require [clojure.tools.logging :refer :all] [clojure.string :as str] + [clojure.set :as set] [jepsen [checker :as checker] [cli :as cli] [client :as client] [control :as c] + [checker :as checker] [db :as db] [generator :as gen] [independent :as independent] @@ -17,7 +19,7 @@ [knossos.model :as model] [slingshot.slingshot :refer [try+]])) -(defn op-add [_ _] {:type :invoke, :f :add, :value (rand-int 100000)}) +(defn op-add-rand100 [_ _] {:type :invoke, :f :add, :value (rand-int 100)}) (defn op-read [_ _] {:type :invoke, :f :read, :value nil}) (defrecord SetClient [creds] @@ -43,6 +45,41 @@ (teardown! [this test]) (close! [this test])) +(defn set-read-after-write + "Read-after-Write checker for set operations" + [] + (reify checker/Checker + (check [this test history opts] + (let [init {:add-started #{} + :add-done #{} + :read-must-contain {} + :missed #{} + :unexpected #{}} + final (reduce + (fn [state op] + (info "state:" state) + (info "operation:" op) + (case [(:type op) (:f op)] + ([:invoke :add]) + (assoc state :add-started (conj (:add-started state) (:value op))) + ([:ok :add]) + (assoc state :add-done (conj (:add-done state) (:value op))) + ([:invoke :read]) + (assoc-in state [:read-must-contain (:process op)] (:add-done state)) + ([:ok :read]) + (let [read-must-contain (get (:process op) (:read-must-contain state)) + new-missed (set/difference read-must-contain (:value op)) + new-unexpected (set/difference (:value op) (:add-started state))] + (assoc state + :read-must-contain (dissoc (:read-must-contain state) (:process op)) + :missed (set/union (:missed state) new-missed), + :unexpected (set/union (:unexpected state) new-unexpected))) + state)) + init history) + valid? (and (empty? (:missed final)) (empty? (:unexpected final)))] + (info "final state:" final) + (assoc final :valid? valid?))))) + (defn workload1 "Tests insertions and deletions" [opts] @@ -55,8 +92,8 @@ 10 (range 100) (fn [k] - (->> - (gen/mix [op-add]) + (->> (range) + (map (fn [x] {:type :invoke, :f :add, :value x})) (gen/limit (:ops-per-key opts))))) :final-generator (independent/sequential-generator (range 100) @@ -68,12 +105,13 @@ {:client (SetClient. nil) :checker (independent/checker (checker/compose - {:set (checker/set-full {:linearizable? false}) + {:set-full (checker/set-full {:linearizable? false}) + :set-read-after-write (set-read-after-write) :timeline (timeline/html)})) :generator (independent/concurrent-generator 10 (range 100) (fn [k] - (gen/mix [op-add op-read])))}) + (gen/mix [op-add-rand100 op-read])))}) -- cgit v1.2.3