From 4fd888cb30369a72dff268a9d13a3f261e26b1b1 Mon Sep 17 00:00:00 2001 From: Aphyr Date: Tue, 22 Jun 2021 08:50:13 -0400 Subject: [PATCH] WIP: expanding set test --- src/elle/explanation.clj | 12 +- src/elle/graph.clj | 49 +++++- src/elle/infer/cyclic.clj | 38 +++++ src/elle/rw_register.clj | 7 +- src/elle/set_add.clj | 301 ++++++++++++++++++++++++++++++++----- src/elle/txn.clj | 13 +- src/elle/txn_graph.clj | 127 ++++++++++++++++ test/elle/set_add_test.clj | 111 +++++++++++++- 8 files changed, 602 insertions(+), 56 deletions(-) create mode 100644 src/elle/infer/cyclic.clj create mode 100644 src/elle/txn_graph.clj diff --git a/src/elle/explanation.clj b/src/elle/explanation.clj index cd3902e..6aa5dff 100644 --- a/src/elle/explanation.clj +++ b/src/elle/explanation.clj @@ -4,12 +4,16 @@ structures or text.") (defprotocol Explanation - (->data [ex] "Converts the explanation to a data structure.") - (->text [ex] "Converts the explanation to plain text.")) + (->data [ex] + "Converts the explanation to a data structure.") + (->text [ex context] + "Converts the explanation to plain text. An optional context map + provides extra information used in rendering--for instance, short + names for transactions.")) (def trivial "A trivial explanation which doesn't explain anything. Helpful for stubbing out methods." (reify Explanation - (->data [ex] :just-cuz) - (->text [ex] "just cuz"))) + (->data [ex] :just-cuz) + (->text [ex ctx] "just cuz"))) diff --git a/src/elle/graph.clj b/src/elle/graph.clj index f9e58d2..8e1c040 100644 --- a/src/elle/graph.clj +++ b/src/elle/graph.clj @@ -124,11 +124,18 @@ (apply [_ a b] (set/union a b)))) -(defn ^IEdge edge +(defn edge "Returns the edge between two vertices." [^IGraph g a b] (.edge g a b)) +(defn maybe-edge + "Returns the edge between two vertices, or nil if one does not exist." + [^IGraph g a b] + (let [o (out g a)] + (when (and o (.contains o b)) + (.edge g a b)))) + (defn edges "A lazy seq of all edges." [^IGraph g] @@ -694,3 +701,43 @@ ; Keep exploring (let [v (first (c/remove seen vs))] (recur (conj path v) (assoc seen v (count path))))))))) + +(defn total-order? + "Returns truthy iff this graph is a total order: every vertex has at most one + outbound edge and one inbound edge, exactly one vertex has no inbound edge, + and exactly one different vertex has no outbound edge. + + If this graph is a total order, returns {:min min, :max max}, where min and + max are the vertices with no inbound and no outbound edges, respectively." + [g] + (let [res (reduce (fn [[min max :as bounds] v] + (let [in-count (.size (in g v)) + out-count (.size (out g v))] + (cond ; Normal vertex + (and (= 1 in-count) (= 1 out-count)) + bounds + + ; Too many edges! + (or (< 1 in-count) (< 1 out-count)) + (reduced false) + + ; Too few edges! + (and (= 0 in-count) (= 0 out-count)) + (reduced false) + + ; This node is a minimum + (= 0 in-count) + (if min + (reduced false) ; Duplicate minimum! + [v max]) ; We found our minimum + + (= 0 out-count) + (if max + (reduced false) + [min v])))) + [nil nil] + (vertices g))] + (if res + {:min (first res) + :max (second res)} + false))) diff --git a/src/elle/infer/cyclic.clj b/src/elle/infer/cyclic.clj new file mode 100644 index 0000000..cc4b372 --- /dev/null +++ b/src/elle/infer/cyclic.clj @@ -0,0 +1,38 @@ +(ns elle.infer.cyclic + "This namespace infers cyclic anomalies over analyses with transaction + graphs--for instance, G1c, G2, G-single, etc." + (:require [elle [core :as elle] + [explanation :as expl] + [txn-graph :as tg] + [txn :as et]])) + +(defn anomalies + "Returns a map of cyclic anomalies present in an analysis." + [analysis] + (let [txn-graph (:txn-graph analysis) + pair-explainer (reify elle/DataExplainer + (explain-pair-data [_ a b] + ; Bit of a hack: explain-pair-data is supposed to + ; return a map, so we're returning a defrecord + ; Explanation, which works as *both* a map and also + ; lets us do our text rendering later. + (assoc (tg/explain txn-graph a b) + :a a + :b b)) + + (render-explanation [_ expl a-name b-name] + (expl/->text expl {:txn-names {(:a expl) a-name + (:b expl) b-name}}))) + graph-analyzer (fn [history] + {:graph (tg/graph txn-graph) + :explainer pair-explainer}) + analyzer (apply elle/combine + (cons graph-analyzer + (et/additional-graphs analysis)))] + (et/cycles analysis analyzer (:history analysis)))) + +(defn add-anomalies + "Takes an analysis, and updates its :anomalies field to include any cyclic + anomalies found." + [analysis] + (update analysis :anomalies merge (anomalies analysis))) diff --git a/src/elle/rw_register.clj b/src/elle/rw_register.clj index 44449fd..a0c0777 100644 --- a/src/elle/rw_register.clj +++ b/src/elle/rw_register.clj @@ -1,5 +1,5 @@ (ns elle.rw-register - "A test which looks for cycles in write/read transactionss over registers. + "A test which looks for cycles in write/read transactions over registers. Writes are assumed to be unique, but this is the only constraint. Operations are of two forms: @@ -460,7 +460,10 @@ (reduce (fn [cases [k version-graph]] (let [sccs (g/strongly-connected-components version-graph)] (->> sccs - (sort-by (partial reduce min)) + (sort-by (partial reduce (fn option-compare [a b] + (cond (nil? a) b + (nil? b) a + true (min a b))))) (map (fn [scc] {:key k :scc scc})) diff --git a/src/elle/set_add.clj b/src/elle/set_add.clj index 783604f..c5c3d3f 100644 --- a/src/elle/set_add.clj +++ b/src/elle/set_add.clj @@ -5,10 +5,12 @@ [set :as set]] [elle [explanation :as expl] [graph :as g] - [recovery :as recovery] + [recovery :as rec] [txn :as et] + [txn-graph :as tg] [util :as util :refer [map-vals]] [version-graph :as vg]] + [elle.infer [cyclic :as cyclic]] [jepsen.txn :as jt] [knossos.op :as op]) (:import (io.lacuna.bifurcan IntSet))) @@ -75,7 +77,10 @@ ; argument would be to maximize entropy by choosing early bits with ; roughly 50% probability of appearing, but I think that the intset ; representation can actually be more compact if we sort the elements - ; in ascending order, the way they were likely added to the set? + ; in ascending order, the way they were likely added to the set? This + ; packing is probably denser, but it also means differences are + ; probably at the end of the intset, so maybe it takes longer to check? + ; Might be worth revisiting this later. element-order (vec (sort elements)) ; This gives us a mapping from indexes to elements. Now we need the ; inverse index: @@ -95,15 +100,16 @@ (defn all-versions "Returns a map of keys to the set of all versions we know existed for that - key, in a given history." + key, in a given history. We always infer the empty set, even if not observed." [history] (->> history (filter op/ok?) jt/op-mops - (reduce (fn [kvs [_ [f k v]]] + (reduce (fn version-finder [kvs [_ [f k v]]] (when (= :r f) - (let [vs (get kvs k #{})] - (assoc kvs k (conj vs v)))))))) + (let [vs (get kvs k #{#{}})] + (assoc kvs k (conj vs v))))) + {}))) (def ^:dynamic *calls* "Perf testing helper, delete me later" @@ -259,7 +265,26 @@ (explain-version-pair [this k v v'] (reify expl/Explanation (->data [_] [:subset v v']) - (->text [_] (str (pr-str v) "is a subset of" (pr-str v')))))))) + (->text [_ ctx] (str (pr-str v) "is a subset of" (pr-str v')))))))) + +(defn add-version-graph + "Adds a version graph to an analysis." + [analysis] + (assoc analysis :version-graph (version-graph (:history analysis)))) + +(defrecord WriteRecovery [elements->versions versions->writes] + rec/WriteRecovery + (write->version [_ [f k v]] + (get-in elements->versions [k v])) + + (explain-write->version [_ [f k v] version] + expl/trivial) + + (version->write [_ k version] + (get-in versions->writes [k version])) + + (explain-version->write [_ k version [op mop]] + expl/trivial)) (defn write-recovery "Returns a WriteRecovery object mapping between versions and writes. @@ -274,43 +299,237 @@ anomaly detection. Obviously it would find serializability violations, but we might miscategorize dependencies." [history] - (let [versions (->> (all-versions history) - (map-vals (fn [versions-of-key] - ; For each set of versions, we want a series - ; of pairs like [vs vs'], where vs are of - ; size n, and vs' are of size n+1. That way - ; we can incrementally compare them. - (group-by count) - (sort-by key) - (map val) - (partition 2 1)))) - ; Now, for each key, take every combination of versions which differ in - ; size by 1, and look for a single-element difference between them. - elements->versions - (->> (for [[k [vs vs']] versions - v vs - v' vs'] - (let [diff (set/difference v' v)] - (when (= 1 (count diff)) - ; Aha! We found the version resulting from the write of e! - (let [e (first diff)] - [e v'])))) - (remove nil?) - (into {})) - versions->elements (set/map-invert elements->versions) - elements->writes (et/args->writes history) + (let [elements->versions + (->> (all-versions history) + (map-vals (fn [versions-of-key] + ; For each set of versions, we want a series + ; of pairs like [vs vs'], where vs are of + ; size n, and vs' are of size n+1. That way + ; we can incrementally compare them. + (let [tier-pairs (->> versions-of-key + (group-by count) + (sort-by key) + (map val) + (partition 2 1))] + ; Now, for each of those pairs, look for + ; single-element differences between them, and + ; produce an [element resulting-version] pair + (->> (for [[vs vs'] tier-pairs + v vs + v' vs'] + (let [diff (set/difference v' v)] + (when (= 1 (count diff)) + ; Aha! We found the version resulting + ; from the write of e! + (let [e (first diff)] + [e v'])))) + ; Turn those into a map of elements to versions + (remove nil?) + (into {})))))) + versions->elements (map-vals set/map-invert elements->versions) + elements->writes (et/args->writes #{:add} history) versions->writes (util/keyed-map-compose versions->elements elements->writes)] + (->WriteRecovery elements->versions versions->writes))) + +(defn explain-indirect-wr + "Explains an indirect relationship where T1 writes something visible to T2." + [t1 t2] + ; TODO: this is gonna break when we find relationships on internal + ; reads/writes--those shouldn't be generated, but we do right now. Fix this + ; in indirect-txn-graph. + (let [writes (jt/ext-writes (:value t1)) + reads (jt/ext-reads (:value t2))] + (reduce (fn [_ [k v]] + (when-let [e (get writes k)] + (when (contains? v (get writes k)) + (reduced + (reify expl/Explanation + (->data [_] {:type :indirect-wr + :write [:add k e] + :read [:r k v]}) + (->text [_ ctx] + (str "added " e " to " k + ", which was visible in a read of " v))))))) + nil + reads))) + +(defn explain-indirect-rw + "Explains an indirect relationship where T1 read a state prior to T2's write." + [t1 t2] + ; TODO: this is gonna break when we find relationships on internal + ; reads/writes--those shouldn't be generated, but we do right now. Fix this + ; in indirect-txn-graph. + (let [reads (jt/ext-reads (:value t1)) + writes (jt/ext-writes (:value t2))] + (reduce (fn [_ [k v]] + (when-let [e (get writes k)] + (when-not (contains? v (get writes k)) + (reduced + (reify expl/Explanation + (->data [_] {:type :indirect-rw + :write [:add k e] + :read [:r k v]}) + (->text [_ ctx] + (str "added " e " to " k + ", which was not present in a read of " v))))))) + nil + reads))) + +(defrecord IndirectTxnGraph [graph txn-graph] + tg/TxnGraph + (graph [this] + ; Just return the merged graph + (:graph this)) + + (explain [_ t1 t2] + ; Try to let the direct txn graph explain it, and if not, we'll try. + (or (tg/explain txn-graph t1 t2) + ; Do we have an edge in the expanded graph? + (when-let [edge (g/maybe-edge graph t1 t2)] + ; OK, cool, what kind? + (cond + (edge :wr) (explain-indirect-wr t1 t2) + (edge :rw) (explain-indirect-rw t1 t2) + true (throw (RuntimeException. + (str "Don't know how to explain edge of type " + (pr-str edge))))))))) + +(defn indirect-txn-graph + "We can use the usual recovery+version graph to infer relationships between + transactions, but there are some legal inferences we *can't* draw this way. + For instance, consider a history with three transactions: ax1, ax2, rx12. We + know that both ax1 and ax2 had to precede rx12, but we can't actually SHOW + that via recoverability: ax1 and ax2 are non-recoverable, and because we + don't know what versions EXIST, we don't have version graph vertices for #{1} + or #{2}. We could try to generate them via the power set of all unrecoverable + vertices, but down that path lies madness. + + Instead, we take advantage of a nifty trick: if the version graph is a total + order for each key, then each read version effectively *partitions* the set + of writes into those which could have come before, and those which could have + come after, that read. So long as the jumps between versions aren't huge + (e.g. #{1 2 3} -> #{1 2 3 4 5} leaves only two elements unfixed), we can + derive rw edges from any read of #{1 2 3} to the writes ax4 and ax5, and wr + edges from ax4 and ax5 to any read of #{1 2 3 4 5}. Our normal recovery graph + is simply the limiting case of this algorithm--when the jump between versions + is exactly one element. + + Our approach here is to fill in the gaps: we check to make sure the version + graph is totally ordered, and if it is, we run through each successful read + in the history. For that read, we take the next smaller and next larger + versions in the version graph, and compute the differences between the + smaller (larger) and the present read: this gives us the writes which must + have occurred just before (after) this read. We look find the transactions + which wrote those values, and link them using wr (rw) edges. + + These aren't necessarily the TRUE wr and rw edges, but there should exist a + path which is comprised of any number of ww edges *plus* that wr (rw) edge; + this inference can't cause us to infer more dangerous anomalies. + + Takes an analysis with a version and transaction graph, and returns the + TransactionGraph augmented with indirect edges, or nil if we can't infer any + indirect edges." + [analysis] + (when (let [vg (:version-graph analysis)] + (->> (vg/all-keys vg) + (map (partial vg/graph vg)) + (every? g/total-order?))) + (let [vg (:version-graph analysis) + tg (:txn-graph analysis) + rec (:recovery analysis) + history (:history analysis) + args->writes (et/args->writes #{:add} history) + ; A function which returns true if a write [op2 mop2] is recoverable + ; OR is the current operation op. + ignored-write? (fn [op [op2 mop2]] + (or (rec/write->version rec mop2) + (= op op2))) + tgg' + (->> history + (filter op/ok?) + ; TODO: instead of reduce-mops (which gives us every mop) we + ; should take just external reads. + (jt/reduce-mops + (fn [g op [f k v :as mop]] + (if (= :r f) + (let [; Link previous writes to current read. + g' + (as-> v % + ; Find the previous version + (first (g/in (vg/graph vg k) %)) + ; Compute the delta with the current version + (set/difference v %) + ; Map those elements back to [op mop] pairs + (map (get args->writes k) %) + ; Remove unrecoverable writes, and this op to + ; prevent self-edges: + (remove (partial ignored-write? op) %) + ; And taking just the ops from those pairs + (map first %) + ; And creating links in the graph. + (g/link-all-to g % op :wr)) + + ; Almost symmetrically, link following writes to the + ; current read. + g' + (as-> v % + (first (g/out (vg/graph vg k) %)) + (set/difference % v) + (map (get args->writes k) %) + (remove (partial ignored-write? op) %) + (map first %) + (g/link-to-all g' op % :rw))] + g') + ; Not a read + g)) + (tg/graph tg)))] + (IndirectTxnGraph. tgg' tg)))) + +(defn add-indirect-txn-graph + "Takes an analysis, and augments its txn-graph as per indirect-txn-graph." + [analysis] + (when-let [tg (indirect-txn-graph analysis)] + (assoc analysis :txn-graph tg))) + +(defn add-recovery + "Adds a recovery to an analysis." + [analysis] + (assoc analysis :recovery (write-recovery (:history analysis)))) + +(defn preprocess + "Removes the nemesis from an analysis' history, checks for type sanity, etc." + [analysis] + (let [history (:history analysis) + history (vec (remove (comp #{:nemesis} :process) history)) + _ (et/assert-type-sanity history)] + (assoc analysis :history history))) + +(defn check + "Full checker for sets with addition. Options are: + + :consistency-models A collection of consistency models we expect this + history to obey. Defaults to [:strict-serializable]. + See elle.consistency-model for available models. - (reify recovery/WriteRecovery - (write->version [_ [f k v]] - (get-in elements->versions [k v])) + :anomalies You can also specify a collection of specific + anomalies you'd like to look for. Performs limited + expansion as per + elle.consistency-model/implied-anomalies. - (explain-write->version [_ [f k v] version] - expl/trivial) + :additional-graphs A collection of graph analyzers (e.g. realtime) + which should be merged with our own dependency + graph. - (version->write [_ k version] - (get-in versions->writes [k version])) + :directory Where to output files, if desired. (default nil) - (explain-version->write [_ k version [op mop]] - expl/trivial)))) + :plot-format Either :png or :svg (default :svg)" + [opts history] + (-> {:options opts + :history history} + preprocess + add-recovery + add-version-graph + tg/add-txn-graph + add-indirect-txn-graph + cyclic/add-anomalies)) diff --git a/src/elle/txn.clj b/src/elle/txn.clj index ab819b5..5ca3edc 100644 --- a/src/elle/txn.clj +++ b/src/elle/txn.clj @@ -50,12 +50,13 @@ and [op mop] is the operation, and micro-op in that operation, which wrote that argument." [write? history] - (reduce-mops (fn [m op [f k v :as mop]] - (if (write? f) - (assoc-in m [k v] [op mop]) - m)) - {} - history)) + (->> history + (remove op/invoke?) + (reduce-mops (fn [m op [f k v :as mop]] + (if (write? f) + (assoc-in m [k v] [op mop]) + m)) + {}))) (defn ReadRecovery "Takes a history and returns a ReadRecovery object mapping read mops to their diff --git a/src/elle/txn_graph.clj b/src/elle/txn_graph.clj new file mode 100644 index 0000000..f8caa07 --- /dev/null +++ b/src/elle/txn_graph.clj @@ -0,0 +1,127 @@ +(ns elle.txn-graph + "This structure forms a graph over transactions (completed operations), where + relationships are sets of dependency types like :ww, :wr, :rw, and :rt." + (:require [jepsen.txn :as txn] + [elle [explanation :as expl] + [graph :as g] + [recovery :as recovery] + [version-graph :as vg]])) + +(defprotocol TxnGraph + "A TxnGraph basically combines a Bifurcan graph between completed operations + with a means of *justifying* the relationships in that graph." + + (graph [_] + "Returns a Bifurcan DirectedGraph over transactions (completed + operations).") + + (explain [_ t1 t2] + "Returns an Explanation of why transaction T1 precedes T2.")) + +(defn add-ww-edges + "Takes a txn graph, a recovery, a version graph, and a write mop in an op t1. + Finds the transactions t2 which wrote the immediately following version, and + adds t1 -ww-> t2 edges in the transaction graph." + [txn-graph recovery version-graph t1 [f k v :as mop]] + ; What version did this write produce? + (if-let [v (recovery/write->version recovery mop)] + ; Find following versions + (let [next-versions (g/out (vg/graph version-graph k) v) + ; And the txns which wrote them + t2s (map (comp first (partial recovery/version->write recovery k)) + next-versions)] + (g/link-to-all txn-graph t1 t2s :ww)) + ; Shoot, we don't know what version this write produced. + txn-graph)) + +(defn add-wr-edge + "Takes a txn graph, a recovery, a version graph, and a read mop in an op t2. + Finds the transation t1 which wrote the value this read observed, and adds a + :wr edge to the txn graph." + [txn-graph recovery version-graph t2 [f k v]] + (if-let [[t1 _] (recovery/version->write recovery k v)] + (g/link txn-graph t1 t2 :wr) + txn-graph)) + +(defn add-rw-edges + "Takes a txn graph, a recovery, a version graph, and a read mop in an op t1. + Finds the transactions t2 which wrote the immediately following version(s) in + the version graph, and adds :rw edges from t1 -> t2 to the transaction graph. + + Why is this legal? Imagine we have a record with versions 1 and 2, both of + which follow version 0, but no relationship between 1 and 2. Assume, WLOG, 0 + < 1 < 2 in the real history--but we don't know this. Can we emit improper + cycles by having a direct rw edge 0 -rw-> 2, and missing the edges 0-ww->1 + and 1-ww->2, etc? + + The answer is no, GIVEN the types of anomalies we infer. Any cycle which uses + the inferred edge 0 -rw-> 2 has a corresponding path of the form [0 -rw-> 1, + 1 -ww-> 2], and the same holds true for arbitrary additional 'hidden + versions' between 0 and 2: each must be connected by a ww edge. We might + accidentally infer a more conservative cycle--like interpreting a g-single as + a g2, but missing some ww edges won't cause us to miss a cycle, or interpret + it as a *worse* cycle." + [txn-graph recovery version-graph t1 [f k v]] + ; Find the following versions + (let [next-versions (g/out (vg/graph version-graph k) v) + ; And the txns which wrote them + t2s (map (comp first (partial recovery/version->write recovery k)) + next-versions)] + ; Now, generate links + (g/link-to-all txn-graph t1 t2s :rw))) + +(defn add-txn-edges + "Takes a transaction graph, a recovery, a version graph, and a mop in an op. + Adds ww, wr, and rw edges to the transaction graph which are inferrable from + this particular mop." + [txn-graph recovery version-graph op [f :as mop]] + (case f + ; For reads, we infer wr and rw edges into and out of (respectively) this + ; read version. + :r (-> txn-graph + (add-wr-edge recovery version-graph op mop) + (add-rw-edges recovery version-graph op mop)) + ; Must be a write. For this, we infer the outbound ww edges--inbound will + ; be covered by other ops. + (-> txn-graph + (add-ww-edges recovery version-graph op mop)))) + +(defn version-graph->txn-graph + "Takes an analysis and yields a TxnGraph from it, using that analysis' + :history, :recovery, and :version-graph." + [analysis] + (let [r (:recovery analysis) + vg (:version-graph analysis) + tg (g/forked + (txn/reduce-mops (fn [g op mop] + (add-txn-edges g r vg op mop)) + (g/linear (g/digraph)) + ; For our purposes, we only care about ok and + ; info ops; no need to infer dependencies over + ; failed operations. + (filter (comp #{:ok :info} :type) + (:history analysis))))] + (reify TxnGraph + (graph [_] tg) + + (explain [_ t1 t2] + ; What kind of edge do we have? + (when-let [edge (g/maybe-edge tg t1 t2)] + (cond + (edge :ww) (reify expl/Explanation + (->data [_] :ww) + (->text [_ ctx] "ww")) + (edge :wr) (reify expl/Explanation + (->data [_] :wr) + (->text [_ ctx] "wr")) + (edge :rw) (reify expl/Explanation + (->data [_] :rw) + (->text [_ ctx] "rw")) + true (throw (RuntimeException. + (str "Don't know how to explain edge of type " + (pr-str edge)))))))))) + +(defn add-txn-graph + "Takes an analysis with a history, recovery, and version graph, and infers a txn graph for it." + [analysis] + (assoc analysis :txn-graph (version-graph->txn-graph analysis))) diff --git a/test/elle/set_add_test.clj b/test/elle/set_add_test.clj index d6a016d..d57b6c4 100644 --- a/test/elle/set_add_test.clj +++ b/test/elle/set_add_test.clj @@ -6,8 +6,52 @@ [clojure.test.check [clojure-test :refer [defspec]] [generators :as gen] [properties :as prop]] - [elle [graph :as g] - [set-add :refer :all]])) + [elle [explanation :as expl] + [graph :as g] + [recovery :as rec] + [set-add :refer :all] + [txn-graph :as tg] + [version-graph :as vg]] + [knossos.history :as history])) + +(defn op + "Generates an operation from a string language like so: + + ax1 append 1 to x + ry12 read y = [1 2] + ax1ax2 append 1 to x, append 2 to x" + ([string] + (let [[txn mop] (reduce (fn [[txn [f k v :as mop]] c] + (case c + \a [(conj txn mop) [:add]] + \r [(conj txn mop) [:r]] + \x [txn (conj mop :x)] + \y [txn (conj mop :y)] + \z [txn (conj mop :z)] + (let [e (Long/parseLong (str c))] + [txn [f k (case f + :add e + :r (conj (or v #{}) e))]]))) + [[] nil] + string) + txn (-> txn + (subvec 1) + (conj mop))] + {:type :ok, :value txn})) + ([process type string] + (assoc (op string) :process process :type type))) + +(defn pair + "Takes a completed op and returns an [invocation, completion] pair." + [completion] + [(-> completion + (assoc :type :invoke) + (update :value (partial map (fn [[f k v :as mop]] + (if (= :r f) + [f k nil] + mop))))) + completion]) + (defn naive-version-graph-for-key "A simple implementation which finds the version graph for a key by @@ -128,5 +172,68 @@ (prn)) tc?))) +(deftest empty-test + (let [r (check {} [])] + (is (= [] (:history r))) + (is (= (g/digraph) (tg/graph (:txn-graph r)))))) + +(deftest single-write-read-test + (let [[t1 t1'] (pair (op "ax1")) + [t2 t2'] (pair (op "rx1")) + h (history/index [t1 t1' t2 t2']) + [t1 t1' t2 t2'] h + r (check {} h) + rec (:recovery r) + vg (:version-graph r) + tg (:txn-graph r)] + (pprint vg) + ; We can show that ax1 produced the set #{1} + (is (= #{1} (rec/write->version rec (first (:value t1'))))) + ; And that #{1} was produced by ax1 + (is (= [t1' (first (:value t1'))] (rec/version->write rec :x #{1}))) + + ; We know #{1} came after #{} + (is (= {#{} #{#{1}} + #{1} #{}} + (g/->clj (vg/graph vg :x)))) + + ; And we can infer a write-read dependency here + (is (= {t1' #{t2'} + t2' #{}} + (g/->clj (tg/graph tg)))))) + +(deftest ambiguous-writes-both-read-test + (let [[t1 t1'] (pair (op "ax1")) + [t2 t2'] (pair (op "ax2")) + [t3 t3'] (pair (op "rx12")) + h (history/index [t1 t1' t2 t2' t3 t3']) + [t1 t1' t2 t2' t3 t3'] h + r (check {} h) + rec (:recovery r)] + ; We can't show what write generated {1 2}, or whether {1} or {2} even + ; existed. + (is (nil? (rec/version->write rec :x #{1}))) + (is (nil? (rec/version->write rec :x #{2}))) + (is (nil? (rec/version->write rec :x #{1 2}))) + (is (nil? (rec/write->version rec (first (:value t1'))))) + (is (nil? (rec/write->version rec (first (:value t2'))))) + + ; But we CAN infer version relationships here. We know #{} (indirectly) + ; precedes #{1 2}, because #{} is the initial state. + (is (= {#{} #{#{1 2}} + #{1 2} #{}} + (g/->clj (vg/graph (:version-graph r) :x)))) + ; We can't actually infer any relationships from this graph *directly*, + ; because we don't have recoverability for the writes. However, our + ; indirect wr and rw inference CAN identify these edges, which gives us the + ; following > shaped graph. + (is (= {t1' #{t3'} + t2' #{t3'} + t3' #{}} + (g/->clj (tg/graph (:txn-graph r))))) + (is (= {:type :indirect-wr + :write [:add :x 1] + :read [:r :x #{1 2}]} + (expl/->data (tg/explain (:txn-graph r) t1' t3'))))))