Towards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced(…)
summary
Built an emulator in Erlang and decompiler pipeline reproduces BEAM behavior for most cases but exposes four concrete mismatches: binary pattern ops need dedicated helpers (floats, UTF‑8, non‑aligned bits), funs hit a 255 arity limit requiring an erase/named‑fun adapter, selective receive only admits a costly selective receive approximation that scans and queues mailboxes, and exception frames show a stack/line metadata mismatch with erl_eval. Tests and executable validation scripts run and empirically confirm these gaps and the proposed workarounds.
AI-written summary · about
chapters (12)
- 0:00Semantic equivalence in BEAM
- 1:49Exact equivalence boundaries
- 3:59Equivalence criteria and exclusions
- 6:04Decompiler lessons and mismatches
- 9:41Binary matching gaps
- 12:59Function adapter 255 args
- 17:10Selective receive emulation
- 20:26Stack trace differences
- 22:11Published work and validation
- 23:56Boundary frontier findings
- 24:59Takeaways and design
- 26:25Q&A
related talks
46mBuild Your Own Elixir
39mJIT Compiler for Erlang OTP
34mAnalysing and Understanding Erlang Programmatically
39mFireside chat on JIT compiler
37mBEAM NIFs in Ziglang for Elixir AND Erlang
44mA Few Improvements to Erlang
35mDeriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
24mBean: A Language for Backward Error Analysis