Expand strong-session-SI and strong-SI anomalies

Our definitions of strong session SI and strong SI were limited
specifically to G-nonadjacent-(process|realtime), respectively. We now
consider internal and G1-(process|realtime) anomalies as well.

src/elle/consistency_model.clj

@@ -65,7 +65,10 @@
      :G1a [:G1]
      :G1b [:G1]
      :G1c [:G1]
-     :G1c-process  [:G1c-realtime]
+     ; Since processes are singlethreaded
+     :G1c-process  [:G1c-realtime :G1-process]
+     :G1c-realtime [:G1-realtime]
+     :G1-process   [:G1-realtime]
 
      ; G-single is a special case of G-nonadjacent
      :G-single          [:G-nonadjacent
@@ -400,9 +403,11 @@
         ; (G-single-realtime), and since we actually formalize this in SI as
         ; G-nonadjacent rather than just G-single, I'm going to include
         ; G-nonadjacent's realtime and process variants here too.
-        :strong-session-snapshot-isolation [:G-nonadjacent-process]
-        :strong-snapshot-isolation         [:G-nonadjacent-realtime]
-        :strong-session-serializable [:G1c-process     ; Daudjee
+        :strong-session-snapshot-isolation [:G1-process
+                                            :G-nonadjacent-process]
+        :strong-snapshot-isolation         [:G1-realtime
+                                            :G-nonadjacent-realtime]
+        :strong-session-serializable [:G1-process      ; Daudjee
                                       :G2-process]     ; Daudjee
         :update-serializable       [:G1 :G-update]     ; Adya
 

test/elle/list_append_test.clj

@@ -1027,9 +1027,39 @@
       (is (= {:valid? true}
              (c {} h))))))
 
-; Example of checking a file, for later
-;(deftest dirty-update-1-test
-;  (cf {} "histories/dirty-update-1.edn")))
+(deftest wr-process-test
+  ; An anomaly reported in https://github.com/jepsen-io/elle/issues/21. Elle
+  ; detected this as a violation of strong serializability, but did not
+  ; originally consider it a violation of strong session SI
+  (let [[t0 t0' t1 t1' t2 t2' :as h]
+        (h/history
+          [{:process 1, :type :invoke, :f :txn, :value [[:r :x] [:append :y 1]], :index 0}
+           {:process 1, :type :ok, :f :txn, :value [[:r :x [1]] [:append :y 1]], :index 1}
+           {:process 2, :type :invoke, :f :txn, :value [[:r :y]], :index 2}
+           {:process 2, :type :ok, :f :txn, :value [[:r :y [1]]], :index 3}
+           {:process 2, :type :invoke, :f :txn, :value [[:append :x 1]], :index 4}
+           {:process 2, :type :ok, :f :txn, :value [[:append :x 1]], :index 5}])]
+    (is (= {:valid? false
+            :anomaly-types [:G1c-process],
+           :anomalies
+           {:G1c-process
+            [{:cycle [t0' t1' t2' t0']
+              :steps
+              [{:type :wr,
+                :key :y,
+                :value 1,
+                :a-mop-index 1,
+                :b-mop-index 0}
+               {:type :process, :process 2}
+               {:type :wr,
+                :key :x,
+                :value 1,
+                :a-mop-index 0,
+                :b-mop-index 0}],
+              :type :G1c-process}]},
+           :not #{:strong-session-snapshot-isolation
+                  :strong-session-serializable}}
+           (c {:consistency-models [:strong-session-snapshot-isolation]} h)))))
 
 (deftest ^:perf scc-search-perf-test
   ; A case where even small SCCs caused the cycle search to time out
@@ -1087,3 +1117,7 @@
                      n run-time (/ n run-time)
                      check-time (/ n check-time)))))
 
+; Example of checking a file, for later
+;(deftest dirty-update-1-test
+;  (cf {} "histories/dirty-update-1.edn")))
+