Verification — bi-11-scheduling

A module is complete when these pass against measured or observed output, not when the prose has been read.

  • fe-01 completed first
  • Priority-inversion ordering predicted, then measured
  • Yield-cost curves plotted for MessageChannel and scheduler.yield()
  • A case constructed where continuation priority demonstrably matters
  • Long task reduced from >300 ms to <50 ms input delay without reducing total work
  • One trace event name correlated back to source

Gate (§44) — for every source-reading exercise in this module

  • Why does this code exist?
  • What invariant does it maintain?
  • Who calls it?
  • What does it call?
  • Which process and thread executes it?
  • What happens if it is removed?
  • How is it tested?
  • What simpler design would fail, and why?

Record