Automatic Energy Analysis Using Types
summary
Claims a new type system called Heliot that encodes peripheral state machines as types and combines that with typestate + AARA to produce symbolic energy bounds for embedded code. It synthesizes per-statement cost expressions for CPU work, explicit peripheral operations, and background-active peripherals; creates a fresh state variable per transition, collects constraints at call sites, and solves them decidably to infer initial states. Prototype targets Rust and reports timing-aware, compositional worst-case energy estimates.
AI-written summary · about
chapters (7)
- 0:00Embedded energy challenges
- 1:25Prior energy analysis limits
- 2:28Heliot type system
- 3:52Cost expressions and type state
- 5:57State inference for peripherals
- 7:42Q&A: Judges on time
- 10:38Q&A: Type systems
related talks
16mAnnotating Executable DSLs with Energy Estimation Formulas
35mProactive Energy-Aware Programming with PEEK
01h 12mPower, Energy and Analysis
26mAP Power Sequence Subsystem
01h 19mEnergy and Efficiency
20mACES: Automatic Compartments for Embedded Systems
22mAlgorithm-Aware Hardware Optimization using E-Graph Rewriting: how should we marry(…)
57mC++ to the RISCue! A Practical Guide for Embedded C++20