three threads, one shared readmade with verso-snippets

View

/-- Three threads, all of which read `[2]`. Bernstein admits this; `∗`-disjointness does not. -/
def shared : ParProg := paralever {
  %0 := [0];
  %1 := [1];
  [2] := R 0 + R 1;
  parallel { %3 := [2]; [3] := R 3 * 2 }
    | { %4 := [2]; [4] := R 4 - 1 }
    | { [5] := 7 }
}

-- the footprint is a fold over the syntax: reads on the left, writes on the right
example : footprintOf shared = ⟨[0, 1, 2, 2], [2, 3, 4, 5]⟩ := rfl
example : wfB shared = true := by⊢ shared.wfB = true decideAll goals completed! 🐙