Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...
summary
A compiler and DSL called ribbit accepts a high‑level ADT plus a separate memory type, emits LLVM IR, and proves pattern‑match compilation correct; it implements bit stealing for pointers, encodes Linux‑style red‑black layouts, and uses a decision‑tree weaving algorithm to generate switch-based code. Benchmarks show ribbit reproduces native memory size exactly (within one root pointer) and that space‑optimized layouts produce the expected speedups, so the tool and compilation strategy work end‑to‑end.
AI-written summary · about
chapters (8)
- 0:00Custom memory layouts
- 3:00ADT performance cost
- 6:11Combining layouts with ADTs
- 7:12Ribbit memory layout
- 13:58Pattern matching compilation
- 21:05Benchmarking layouts
- 23:13Formal guarantees & future work
- 24:37Q&A
related talks
51mRibbit with Memory Morphisms
21mWeak Memory Demands Model-based Compiler Testing
01h 02mMemory and Compilers
22mReconciling High-level Optimizations and Low-level Code in LLVM
19mPanel: Compilation Frameworks
01h 25mRISC V Bit Manipulation ISA Extension Spec, Hardware, Software
37mAssembling
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends