Show HN: PON-BEAM re-architecture of the Erlang VM
github.com
PON-BEAM is a complete re-architecture of the Erlang/OTP Virtual Machine (ERTS — Erlang Run-Time System) using the Notification-Oriented Paradigm (PON)
github.com
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.
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.