micropelago/garage
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Check read-after-write property for sets

Browse Source
This commit is contained in:
Alex Auvolat 2023-04-19 22:02:03 +02:00
parent 55eb4e87c4
commit 18ee8efb5f
1 changed files with 43 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
script/jepsen.garage/src/jepsen/garage/set.clj
View File

@ -1,10 +1,12 @@
(ns jepsen.garage.set (ns jepsen.garage.set
(:require [clojure.tools.logging :refer :all] (:require [clojure.tools.logging :refer :all]
[clojure.string :as str] [clojure.string :as str]
[clojure.set :as set]
[jepsen [checker :as checker] [jepsen [checker :as checker]
[cli :as cli] [cli :as cli]
[client :as client] [client :as client]
[control :as c] [control :as c]
[checker :as checker]
[db :as db] [db :as db]
[generator :as gen] [generator :as gen]
[independent :as independent] [independent :as independent]
@ -17,7 +19,7 @@
[knossos.model :as model] [knossos.model :as model]
[slingshot.slingshot :refer [try+]])) [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}) (defn op-read [_ _] {:type :invoke, :f :read, :value nil})
(defrecord SetClient [creds] (defrecord SetClient [creds]
@ -43,6 +45,41 @@
(teardown! [this test]) (teardown! [this test])
(close! [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 (defn workload1
"Tests insertions and deletions" "Tests insertions and deletions"
[opts] [opts]
@ -55,8 +92,8 @@
10 10
(range 100) (range 100)
(fn [k] (fn [k]
(->> (->> (range)
(gen/mix [op-add]) (map (fn [x] {:type :invoke, :f :add, :value x}))
(gen/limit (:ops-per-key opts))))) (gen/limit (:ops-per-key opts)))))
:final-generator (independent/sequential-generator :final-generator (independent/sequential-generator
(range 100) (range 100)
@ -68,12 +105,13 @@
{:client (SetClient. nil) {:client (SetClient. nil)
:checker (independent/checker :checker (independent/checker
(checker/compose (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)})) :timeline (timeline/html)}))
:generator (independent/concurrent-generator :generator (independent/concurrent-generator
10 10
(range 100) (range 100)
(fn [k] (fn [k]
(gen/mix [op-add op-read])))}) (gen/mix [op-add-rand100 op-read])))})