1–6 of 6 posts
Show HN: PON-BEAM re-architecture of the Erlang VM
github.com
I built PON-BEAM, a heavily modified version of the Erlang/OTP 30 virtual machine. I wanted to eliminate the O(N) selective receive bottleneck and the CPU-heavy scheduler spinlocks by introducing a reactive, event-driven notification mesh at the C level (using epoll/eventfd).
However, changing how the Erlang scheduler and garbage collector handle state transitions is notoriously dangerous and prone to lost wakeups or deadlocks. To make this viable, I had to formally prove the new architecture.
I used a 4-pillar verification pipeline:
TLA+ / TLC to model the non-blocking invariants of the new scheduler and mailbox.
Coq for mechanized proofs of the Tri-Color garbage collection propagation.
Frama-C / ACSL for C source-level memory safety and loop termination.
PropEr for stateful equivalence testing against the baseline OTP 30.
The result is a VM that maintains exact Erlang semantics but achieves O(1) mailbox reads and 0.0% idle CPU. It is a completely different way to think about VM design (based on the Notification-Oriented Paradigm).
You can read the architectural breakdown and the formal proofs in the repo. Would love to discuss formal methods and VM design with this community.
Do you think the #ifdef PON_BEAM approach would make following OTP updates easy?
I guess being tied to Linux would prevent any chance of getting into the official repo.
Interesting. Do you think the #ifdef PON_BEAM approach would make following OTP updates easy? I guess being tied to Linux would prevent any chance of getting into the official repo.