running it on real threadsmade with verso-snippets
View
not needed — no prose in this code
-- `runTask` spawns one Lean `Task` per thread of every `parallel` block. #check @runTask runTask : ParProg → Regs → State → Regs × State-- The real-threads run leaves exactly the heap the canonical sequential run leaves. The `Task` -- scheduler may interleave however it likes; `wfB` is what makes the outcome independent of it. #check @runTask_eq @runTask_eq : ∀ {s : ParProg}, s.wfB = true → ∀ (ρ : Regs) (σ : State), s.runTask ρ σ = runSeq (s.execPar ρ) σ-- So a wall-clock comparison of the two is fair *by theorem* rather than by observation. #check @runTask_eq_runTaskSeq @runTask_eq_runTaskSeq : ∀ {s : ParProg}, s.wfB = true → ∀ (ρ : Regs) (σ : State), s.runTask ρ σ = s.runTaskSeq ρ σ-- run the pipeline on real threads and read cell 4 back #eval evalTask pipeline (fun _ => .int 0) [4] [Paralever.Val.int 25]