a race, and how it is foundmade with verso-snippets
View
/-- Both threads work for a while, then both write `[9]`. -/
def late : Prog :=
  .par (.seq (.wr 10 1) (.wr 9 1))
       (.seq (.wr 20 1) (.wr 9 2))

/-- Everything starts at `0`. -/
def σ0 : State := fun _ => .int 0

-- Phase 1 walks the tree and collects every fork whose children fail Bernstein. It is linear in
-- the program, and it *is* the obligation: `raceSites_nil_iff` says an empty list is race freedom.
#eval raceSites late.toParM σ0

[{ left := { reads := [], writes := [10, 9] }, right := { reads := [], writes := [20, 9] }, conflicts := [9] }]-- so the program is rejected, by evaluation rather than by search
example : wellFormedB late.toParM σ0 = false := by⊢ wellFormedB late.toParM σ0 = false decideAll goals completed! 🐙

-- Phase 2 is a bounded search, aimed at the cells phase 1 named. It returns a `Schedule`, and
-- `follow_sound` turns any schedule that replays into a `Reaches` proof — so a wrong guess
-- cannot produce a wrong claim, it just fails to find anything.
#check @follow_sound

@follow_sound : ∀ {τ : Type} (s : Schedule) (c c' : Conf τ), follow c s = some c' → Reaches c c'-- the counterexample, replayed against the real `step`
#eval IO.println (explainProg late σ0)
step:thread  action          state
0:T0         write [10] ← 1  10↦1, 9↦0, 20↦0
1:T1         write [20] ← 1  10↦1, 9↦0, 20↦1
2:T1         write [9] ← 2   pending
2:T0         write [9] ← 1   pending
Parallel aborts at Step 2. Reason: T0, T1 write to: {9}.
Parallel: 9↦1
Sequential: 9↦2