Lasagne: A Static Binary Translator for Weak Memory Model Architectures
summary
Lasagne is a static x86→ARM translator that lifts x86 binaries to LLVM IR (via Microsoft mactool), applies pattern-based IR refinements to recover pointer operations, inserts proven-correct fences using a new LLVM memory model, and compiles to ARM. Mechanized Agda proofs show fence mappings and several optimizations are sound. On Phoenix benchmarks fence rules cut fences by ~50%, fence-only optimizations reduce runtime 2.6% and combined optimizations more than double that, trimming translation overhead versus native ARM from ~3× down to ~1.5×.
AI-written summary · about
chapters (6)
related talks
15mTranslation Validation for LLVM's AArch64 Backend
17mCrossMapping: Harmonizing Memory Consistency in Cross-ISA Binary Translation
27mCompiler Support for Control-Flow Linearization Using Architectural Mimicry
01h 02mMemory and Compilers
22mReconciling High-level Optimizations and Low-level Code in LLVM
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
01h 11mProgramming language memory models: Problems, solutions, and directions