Permchecker: A Toolchain for Debugging Memory Managers with Typestate
summary
Permchecker makes heap structure explicit by generating a DSL compiler for typestate specs, an LLVM annotation pass, and a PIN dynamic tool that enforces typestates at runtime; it detects allocation/state mismatches early. Applied to Hotspot, JikesRVM and dlmalloc, the workflow required 144 typestate-change sites, 64 function annotations and ~1,600 lines of glue, and it catches almost all injected faults (836 use-after-free injections, only 4 benign misses). Overhead matches Memcheck and costs ~2–3 months of developer annotation time.
AI-written summary · about
chapters (6)
- 0:00Motivation
- 3:03Dynamic Typestate
- 4:06DSL for Heap Layout: BNF
- 5:13DSL for Heap Layout: Example
- 6:01DSL Artifacts
- 8:39Permchecker Pin Tool: Access Violation
related talks
28mMemory simulations, security and optimization in a verified compiler
01h 22mCompile-Time Borrow Checker with Stateful Metaprogramming
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
21mWeak Memory Demands Model-based Compiler Testing
53mLocknote: How Badly Do We Want Correct Compilers?
01h 02mMemory and Compilers
27mTowards Type Debugging using Partial Evaluation
32mBit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...