From 18ee8efb5f7bfcd64bf1a1336ffd6f54574aa79f Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex@adnab.me>
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/jepsen.garage/src/jepsen/garage')

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