FlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic(…)
summary
FlowCert implements translation validation from LLVM to asynchronous dataflow graphs for the RipTide CGRA by constructing a deterministic canonical schedule and checking a forward simulation augmented with dynamic fractional permissions. The Python tool emits verification conditions (checked in a solver) and finds concrete counterexamples; it uncovers 8 compiler bugs including a previously elusive data race, then verifies the entire RipTide benchmark suite. Typical simulation checks run under one second while permission solving dominates time.
AI-written summary · about
chapters (14)
- 0:00FlowCert introduction
- 1:48CGRA architectures overview
- 3:58C to dataflow compilation
- 5:26Translation validation approach
- 7:15Cut simulation step
- 9:46Fractional permissions step
- 13:42Varus verification tool
- 14:03Evaluation and bugs
- 14:47Conclusion and future
- 15:09Q&A: Cut points
- 16:12Q&A: Memory tracking
- 17:40Q&A: Arbitrary C programs
- 18:41Q&A: Technique limitations
- 19:46Q&A: Benchmarks
related talks
17mLet It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
59mCompiler-assisted Translation Validation
01h 02mHydroflow: A Compiler Target for Fast, Correct Distributed Programs
19mFormally Verifying Optimizations with Block Simulations
09mBreaking the RISC-V Processor Customization Barrier with Formal Verification
19mFlow: An Introduction
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
18mTowards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…)