From 4ba18ce9cca1b828edcf3f8c8770d49c75ed3083 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex@adnab.me>
Date: Fri, 20 Oct 2023 12:13:11 +0200
Subject: [PATCH] jepsen: wip checker for register-like behavior

---
 .../jepsen.garage/src/jepsen/garage/reg.clj   | 66 +++++++++++++++++--
 1 file 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