A Type System for Safe Intermittent Computing
summary
Curricle is a Rust-based information-flow type system that classifies variables as item-potent or non-item-potent, adds access-mode inference to decide when checkpointing is required, and enforces a noninterference-style correctness theorem. Implementation plugs into the Rust compiler, adds about 3.5% LOC overhead, and an evaluation on prior benchmarks shows Curricle’s identified checkpoint list uses roughly 3x less memory and ~2x fewer dynamic writes than an all-writes policy while preserving forward progress.
AI-written summary · about
chapters (13)
- 0:00Intermittent computing intro
- 1:02Intermittent computing correctness
- 2:28Problems with low-level approaches
- 5:59Motivation for type-level approach
- 7:02CCLE type system design
- 8:05CCLE type checking
- 10:08Item potency access modes
- 11:55Programmer specification and impl
- 12:38Inference and checkpointing
- 13:00Correctness theorem and results
- 14:02CCLE benefits over prior systems
- 15:46Handling inputs and references
- 16:06Conclusion and Q&A
related talks
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
17mA Difference World: High-performance, NVM-invariant, Software-only Intermittent...
29mProgramming machine learning algorithms in hardware, sanely, using Haskell and Rust!
38mCorrosive C - Compiling Rust to C to target new platforms
01h 01mConcurrency Challenges of Interrupt Service Routines
34mWriting an Embedded Operating System in Rust
29mSafety monitor: Using Rust in mixed-criticality Linux systems
05mInterview