tarjan-multi-increment.clj

(let [r0 {:type :ok, :f :read, :value {:x 0, :y 0}  ; Initially, x and y are 0
      i1 {:type :ok, :f :inc, :value [:x]}          ; Increment key x by 1
      r1 {:type :ok, :f :read, :value {:x 1, :y 0}} ; Read x and y
      i2 {:type :ok, :f :inc, :value [:y]           ; Increment y
      r2 {:type :ok, :f :read, :value {:x 1, :y 1}} ; Read x and y
      ; So far, so good. The above set of txns is consistent with an order
      ; where i1 precedes i2. Now, let's have a read transaction which observed
      ; the *opposite* order of increments: i2 < i1.
      r3 {:type :ok, :f :read, :value {:x 0, :y 1}}

      ; The history can contain these ops in any order
      h (shuffle [r0 r1 r2 r3 i1 i2])

      ; What's the precedence graph of h with respect to x? We want a map that
      ; relates each read to all the reads which observed the next highest (or,
      ; if you like, lowest) value of x. For r0, which saw x=0, its successors
      ; are r1 and r2, both of which saw x=1.
      <x {r0 [r1 r2]
          ; r1 saw x=1, and there's no read which saw x=2, 3, ..., so it has no
          ; successors in this graph. We could leave it out for performance, but
          ; I'll write it here for clarity:
          r1 []
          ; Ditto for r2
          r2 []
          ; Similarly, r3 also saw x=0, so its successors are r1 and r2 as well:
          r3 [r1 r2]}

      ; OK, now let's do the same thing for reads which observed y. r0 saw y=0,
      ; and r2 and r3 saw y=1:
      <y {r0 [r2 r3]
          ; Ditto: r1 saw y=0, so its set is the same
          r1 [r2 r3]
          ; r2 and r3 saw y=1, and there's no higher y in this history
          r2 []
          r3 []}

      ; We only have two keys here, so our collection of partial orders based
      ; on keys is:
      key-orders [<x <y]

      ; The total precedence graph, g, is the union of all key-orders.
      g {r0 [r1 r2 r3]
         r1 [r2 r3]
         r2 []
         r3 [r1 r2]}

      ; We can use Tarjan's SCC algorithm to identify that g has a cycle.
      ; Specifically, r1 precedes r3 (thanks to <y), and r3 precedes r1 (thanks
      ; to <x). These two reads conflict with each other!
      g-cycle [r1 r3]

      ; If we left out either r1 or r3, this test should pass!
      ])