3 ms·
Show HN: PON-BEAM re-architecture of the Erlang VM
PON-BEAM is a complete re-architecture of the Erlang/OTP Virtual Machine (ERTS — Erlang Run-Time System) using the Notification-Oriented Paradigm (PON)
- matheusosan 2mo ago[flagged]
- matheusosan 2mo ago[flagged]
- matheusosan 2mo agoHi HN, 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. Repo: https://github.com/matheuscamarques/pon_beam https://github.com/matheuscamarques/pon_beam
- conradfr 2mo agoInteresting. 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.
- matheusosan 2mo ago[dead]