Forward build systems, formally
summary
Defines forward-build correctness as: either reproduce the result of running the script sequentially or report a hazard. Models commands, filesystems, Fabricate and Rattle in Agda, assumes deterministic commands and correct tracing. Proves Fabricate correct for hazard-free builds and proves sequential Rattle correct; speculative Rattle gets only a partial correctness theorem because speculation can induce a speculative right-before-read hazard that destroys inputs so rerun may fail.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:32Backward Build System
- 1:00Correctness of a Build System
- 1:43Alternative
- 2:36Idempotence
- 3:16Not Idempotent (Read before Write Hazard)
- 3:44Not Idempotent (Write before Write Hazard)
- 4:09Hazards
- 4:24Correctness of a Forward Build System
- 5:07Outline
- 6:21Model Assumptions
- 8:23Script
- 9:33Fabricate model
- 10:11Correctness of Fabricate
- 11:47Parallelism in Rattle: Speculation
- 13:39Rattle model
- 14:53Correctness of Sequential Rattle
- 15:24Correctness of Speculative Rattle
- 16:00Correctness of Speculative Ratlle (False)
- 16:47Partial correctness
- 17:22Conclusion
related talks
16mA Model for Detecting Faults in Build Specifications
20mOn Extending Incorrectness Logic with Backwards Reasoning
23mSpecifying and Verifying Future Conditions
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction
47mHow to trust a verified program?
13mBackward Symbolic Execution with Loop Folding
50mFrom Prompt Hacking to Architectural Determinism: Engineering Reliable GenAI Systems
13mRevealing Sources of (Memory) Errors via Backward Analysis