⚠️ Honest status — leia antes de tudo. PON-BEAM é um protótipo de pesquisa em andamento, não um produto acabado e não uma superação da BEAM original. Este README descreve apenas o que existe e foi medido de verdade. Os ganhos asintóticos prometidos pela tese (receiveO(1), scheduler sem polling, ETS/GC re-arquitetados) ainda não estão implementados em todas as fases — ver Estado real por fase e Medições honestas. As fases 6–7 não passam de hooks/contadores no código-fonte e cenários de benchmark; números anteriores deste README foram removidos por não corresponderem a medições.
PON-BEAM é um projeto de pesquisa que testa a Notification-Oriented Paradigm (PON) — criado por Prof. Dr. Jean Marcelo Simão — dentro da máquina virtual Erlang/OTP 30 (ERTS): cada subsistema interno é redesenhado como uma malha reativa de Entidades, Premises, Conditions e Instigações, substituindo varredura linear (scan) e polling periódico por notificações point-to-point.
| Fase | Subsistema | Estado atual | Evidência |
|---|---|---|---|
| 0 | Fork Infrastructure | ✅ Implementado — build real -DPON_BEAM, beam.smp funcional, #ifdef PON_BEAM overlay |
RPT-09 §1, RPT-11 |
| 0 | PID Virtual + ring MPSC | ✅ Implementado e validado — roteamento declarado de mensagens para PIDs virtuais, send_after, inventário de BIFs (register/whereis/process_info/link/monitor/exit), fix de use-after-free; smokes ×5 PASS, stress ×3 +A 12, microbench ring sem regressão SMP (0.32 → 0.30 µs/msg) |
RPT-12, smoke_pon_*.erl |
| 1 | PON-Receive | ✅ Fechada (jump O(1) validado) — registro de premissas + contabilidade no enqueue (PLAN-11: tag_chain + atômicos, sem walk no fetch) + jump advance_to_matched com gates; curva plana medida em mailbox profunda: fase1_jump 2.4× @100 → 181× @10k, fase1_real 25–45× @100 → 1812–2023× @10k (total 85.4×), mailbox_scans_avoided 18k/54k. Escopo: premissa única/cabeça concreta; multicláusula/variáveis = Fase 6; o notify cross-thread do receive continua fora de escopo (o canal causal da Fase 4 existe, mas o fast-path O(1) cross-thread não foi religado) |
RPT-01, RPT-10, 507122c3, da3686db |
| 2 | PON-Timer | ✅ Fechada (paridade sem regressão) — timerfd para timers de PID virtual (ERTS_TMR_ROFLG_PON_VIRTUAL) validado; canary em memória implementado e revertido a fallback por regressão medida (RPT-14); ps->timer_fd do pollset como única Instigação temporal; churn 1.00×, idle 1.00×, load 1.03×, sparse 1.01×, fair_timer ≥ 1.0×. Critério "0.0% CPU idle" declarado ingênuo e substituído por paridade |
RPT-14, PLAN-12 |
| 3 | PON-Spawn | ✅ Fechada (paridade sem regressão + instigação causal) — PIDs virtuais validados (RPT-12); regressão estrutural de spawn real (−26%, RPT-09) eliminada por gates de custo nos hooks de schedule/GC (PLAN-13); fair_spawn 0.98–1.28× (mediana 5 VMs: 1.28×), microbenchmark spawn por paridade; spawn_instigations/spawn_notifications contam a instigação causal real. Critério "latência ~2× menor" declarado projeção e substituído por paridade |
RPT-15, PLAN-13 |
| 4 | PON-Scheduler | ✅ Fechada (paridade sem regressão + instigação causal) — ErtsCondition real (eventfd+epoll) com node próprio PonSchedNode (correção definitiva do bug de corrupção de PID, RPT-09 §1.2.1); notify no add2runq + drain no scheduler_wait; scheduler_idle_blocks no ponto de bloqueio TSE real; paridade nos 5 cenários fase4_sched_* (idle 0ms/0ms, wake_latency p50 ~60µs ambos). Critério "0.0% CPU idle" declarado ingênuo e substituído por paridade |
RPT-04, 8713875e |
| 5 | PON-ETS | ✅ Fechada (instigação causal funcional + paridade) — watcher lateral real em erl_db_hash.c: processos registram interesse em {Tabela, Chave} e recebem {pon_ets_change, TableId, KeyHash} na escrita, eliminando polling; registro com mutex + padrão snapshot (sem lock-ordering); BIFs pon_ets_register_watcher/2, pon_ets_unregister_watcher/2; polling 1000 lookups 282–374µs vs notificação + 1 lookup 34–43µs (8.3–8.7×); grupo de controle fase5_stress_ets 1.00×. Critério original ets_read_repeat ~1000× declarado projeção (ETS stock já é hash O(1)) |
RPT-05, 99d59f4f |
| 6 | PON-Compiler | ❌ Não implementado — nenhuma mudança em beam_ssa.erl/beam_opcodes.tab |
— |
| 7 | PON-GC | ❌ Não implementado — hooks em pon_gc.c são instrumentação (stats only); GC stock intacto |
RPT-09 §1.2.2 |
Aceitação global: as Fases 0, 1, 2, 3, 4 e 5 cumprem seus critérios (Fase 1: jump O(1) com curva plana medida no escopo de premissa única; Fases 2–4: critérios ingênuos substituídos por paridade sem regressão + instigação causal instrumentada — RPT-14/RPT-15/RPT-04; Fase 5: instigação causal funcional do watcher lateral + paridade sem regressão — RPT-05). As Fases 6–7 não começaram.
- Fork OTP 30.0-rc0 compilável com overlay PON por
#ifdef PON_BEAM— o código stock permanece intacto (otp-30.0-rc0-stock). - Motor PON (MCE): motor C standalone com nós, premisas
gt/lt/eq, condições e instigações — validado com ASan/TSan (RPT-11: 6039 checks). - Subsistema de PID Virtual: ring MPSC de entrada por nó,
send/2,3roteado,send_after, drain FIFO, inventário de BIFs — tudo validado por smokes e stress. - Telemetria real no ERTS:
erlang:system_info(pon_stats)retornapremises_registered,mailbox_scans_avoided,timerfd_created,gc_incremental_steps, etc. Primeira evidência objetiva de um ERTS PON de verdade (builds antigos rotulados "PON" eram stock relabelados — ver RPT-09 §1.1). - Modo PON-RECEIVE-PARITY: registro de premisas funcional com semântica de receive idêntica ao stock (segurança > velocidade) até o fast-path O(1) ser religado no scheduler do receptor.
- Canal de instigação causal do scheduler (Fase 4):
ErtsConditionreal comeventfd+epoll, FIFO estrita com node próprioPonSchedNode, notify noadd2runqe drain noscheduler_wait— fechado por paridade + instigação causal (RPT-04). - Watcher lateral PON-ETS (Fase 5): processos registram interesse em
{Tabela, Chave}e são notificados por{pon_ets_change, TableId, KeyHash}na escrita — elimina pollingets:lookup; fechado por instigação causal funcional + paridade (RPT-05). - Suíte formal: TLA+/TLC 11/11 modelos, provas Coq 4/4 verificadas com
coqc8.20 (semadmit), Frama-C/WP 23/23 goals provados (Frama-C 33.0 + Alt-Ergo), PropEr 14/14 propriedades — 4 pilares verdes (RPT-16, ART-01).
A tese propõe inverter o fluxo de controle da VM: Entidades registram Premises e Conditions; mudanças de estado disparam Instigações point-to-point direto para os consumidores, eliminando scans lineares (mailbox, GC) e polling periódico (timers, scheduler).
flowchart LR
subgraph Traditional ["Stock BEAM (OTP 30) — Polling and Linear Scan"]
direction TB
P_Scan["Selective Receive: Linear Scan Mailbox"]
T_Poll["Timer Wheel: Periodic Polling Ticks"]
S_Spin["Scheduler: Idle Busy-Spin"]
end
subgraph PON_BEAM ["PON-BEAM — Reactive Push Graphs (design)"]
direction TB
Cond["PON Condition (State Change / Message Arrival)"]
Premise["PON Premise (Pattern Match Slot)"]
Instig["PON Instigation (Direct Execution Jump)"]
Cond -->|Pushes Event| Premise
Premise -->|Satisfies| Instig
end
Traditional ==>|Re-Architected As| PON_BEAM
⚠️ O diagrama acima é o alvo arquitetural. Hoje, o overlay real cobre: motor MCE, PIDs virtuais (ring+timer), bookkeeping de premisas no receive, canal de instigação causal do scheduler (eventfd+epoll, Fase 4) e watcher lateral do ETS (Fase 5). O caminho PON-Timer foi revertido a fallback (paridade validada — RPT-14); o scheduler real continua 100% stock — o overlay PON é instrumentação causal de custo ~zero, e o progresso é garantido pelo caminho stock (RPT-04).
Placar em 30 segundos (mediana de 5 amostras, +S 8:8 — RPT-09, atualizado RPT-15):
| 🟢 Ganhos reais e leves | 🟡 Paridade (±5%) | 🔴 Regressões conhecidas |
|---|---|---|
fair_msg +18% · fair_order +24% · fair_receive +12% · fair_compute +5% · fair_spawn +28% (pós-gates, RPT-15) |
fair_ets −3% · fair_memory 0% · fair_timer 0% · fase5_stress_ets 1.00× · fase4_sched_* 1.00× |
— (regressão de spawn eliminada em RPT-15) |
Leitura honesta: o PON-BEAM atual não é uma revolução de performance — é um overlay com cinco resultados reais medidos: o jump O(1) do receive em mailbox profunda com padrão concreto (escala a complexidade de O(N) para O(1) — Fase 1), a Fase 2 (timers) encerrada como paridade sem regressão (critério "idle 0%" declarado ingênuo, RPT-14), a Fase 3 (spawn) encerrada como paridade sem regressão (a regressão estrutural de −26% foi eliminada por gates de custo — RPT-15), a Fase 4 (scheduler) encerrada como paridade + instigação causal (ErtsCondition real, sem alterar o caminho quente — RPT-04) e a Fase 5 (ETS) encerrada por instigação causal funcional (watcher lateral: notificação + 1 lookup 34–43µs vs polling 1000 lookups 282–374µs, ~8.3×; paridade robusta no controle — RPT-05). Na maioria dos cenários o overlay não piora a BEAM (mensagens/receive pequeno até ganham um pouco). Os grandes ganhos restantes da tese (idle 0% de scheduler, ETS/GC re-arquitetados) foram declarados projeções ingênuas e substituídos por paridade + instigação causal, exceto os de Fases 6–7 (compiler, GC), que ainda não existem na VM — ver estado por fase acima.
Cenários de fortaleza da BEAM original (não selecionados a favor do PON). Razão stock/pon: >1 = PON mais rápido.
| # | Cenário | Stock (µs) | PON (µs) | Razão | Veredicto |
|---|---|---|---|---|---|
| 1 | fair_compute |
217 799 | 208 197 | 1.05× | leve ganho (+5%) |
| 2 | fair_ets |
409 492 | 421 204 | 0.97× | paridade (−3%) |
| 3 | fair_memory |
117 142 | 117 383 | 1.00× | paridade |
| 4 | fair_msg |
197 854 | 168 192 | 1.18× | leve ganho (+18%) |
| 5 | fair_order |
17 803 | 14 400 | 1.24× | leve ganho (+24%) |
| 6 | fair_receive |
161 748 | 143 998 | 1.12× | leve ganho (+12%) |
| 7 | fair_spawn (RPT-09, pré-gates) |
84 580 | 106 234 | 0.80× | 🔴 regressão (−26%) |
| 7b | fair_spawn (RPT-15, pós-gates) |
87 000 | 68 000 | 1.28× | 🟢 paridade/ganho (ver RPT-15) |
| 8 | fair_timer |
317 583 | 318 519 | 1.00× | paridade |
Interpretação honesta: 6/8 em paridade ou leve ganho no RPT-09; a única regressão estrutural (fair_spawn) foi eliminada em RPT-15 — 7/8 em paridade ou ganho (0.98–1.28× no spawn). A causa era hooks incondicionais de instrumentação por schedule/GC, agora gateados por processo PON (PLAN-13). fair_order confirma o invariante FIFO com receive em modo parity.
Metodologia: builds reais idênticos (-O2 -g, JIT), VM nova por execução, 5 execuções por cenário por lado, mediana — auditoria em RPT-09 §1.
Não é protocolo estatístico (limitação declarada no RPT-12 §3.3): serve para direção, não afirmação.
+S 1:1: ganhos expressivos em cenários de stress (GC 3.37×, ETS concurrent 2.55×, compiler 2.37×, dist 2.29×, spawn-under-stress 2.04×, pubsub 1.91×) — mas perdas concentradas emfase1_receive*(0.27–0.62×) (pré-fix do head, errata RPT-12 §5.2),fair_memory0.58×,fair_spawn0.36× (pré-gates; paridade em RPT-15),fifo_pingpong0.49×,fair_compute0.78×. Timers e scheduler em 1.00×.+S 8:8(SMP): perdas em 7/8 cenários fair (0.52–0.99×) — a inversão SMP foi investigada e não é do ring MPSC (microbench 0.32→0.30 µs/msg sob 8 schedulers); o alvo real é o caminhoreceivesob contenção (RPT-12 §5.5).
Tudo é reproduzível: cada run grava JSONs crus em harness/results/<timestamp>/{baseline,ponbeam}/ e o relatório HTML diferencial em <timestamp>/diff/index.html (apontado por harness/results/latest após o término do run).
Sobre os gráficos: as imagens antigas de
docs/assets/charts/foram geradas com valores hardcoded (fabricados) e removidas do repositório. O gerador atual (harness/report/generate_charts.py+charts_data.erl) é 100% data-driven: lê os resultados reais deharness/results/lateste, se um cenário estiver ausente, omite o gráfico (nunca inventa dado). Onde não existia série real mensurável (ex.: "rastreabilidade por commit"), o gráfico foi descontinuado. Para (re)gerar após um run completo:
make benchmark # suíte completa nos dois ERTS
python3 harness/report/generate_charts.py # regenera os PNGs com dados reais- Operating System: Linux com suporte a
timerfd/eventfd(kernel ≥ 2.6.25; ≥ 4.18 recomendado). - Compiler: GCC ≥ 9.0 ou Clang ≥ 11.0.
- Build Tools:
make,autoconf(≥ 2.69),m4,flex,bison. - Runtime Bootstrap: uma instalação Erlang/OTP existente (bootstrap da compilação).
- Formal Tools (opcional): Java 11+ (TLA+ TLC), Coq ≥ 8.13, Frama-C.
git clone https://github.com/matheuscamarques/pon-beam.git
cd pon-beam
# Baseline Stock Erlang/OTP 30 (instala em /opt/erlang-30-stock)
make build-stock
# PON-BEAM ERTS (instala em /opt/erlang-30-pon)
make build-pon
# PON-BEAM com telemetria de debug
make build-pon-debugIteração rápida no C do emulador:
make emulator-pon # recompila só o ERTS PON (~1–3 min)
make emulator-stock # recompila o ERTS stockHarness comparativo real (harness/run.sh) executando os dois ERTS sob workloads idênticos:
make benchmark # suíte completa (aviso: inclui 2× maratona de 10 min)
make benchmark-fair # grupo controle fair_* (rápido)
make benchmark-fair-smp # fair_* com +S 8:8 (SMP)
make benchmark-list # lista cenários disponíveis
./harness/run.sh --fase=1 # apenas os cenários de uma fase (ex.: fase 1)
make report # abre o último relatório HTML diferencialgraph TD
P1["Pillar 1: Model Checking (TLA+/TLC)"] --> V1["Scheduler Wakeup and Mailbox Invariants"]
P2["Pillar 2: Theorem Proving (Coq)"] --> V2["Tri-Color GC Safety and PON Complexity"]
P3["Pillar 3: Static Analysis (Frama-C/ACSL)"] --> V3["C Memory Safety Contracts"]
P4["Pillar 4: Property Testing (PropEr)"] --> V4["Model Equivalence (Stock vs PON)"]
make verify-all # suíte completa (TLA+, PropEr, Frama-C)
make verify-tla # TLA+/TLC (SchedulerWakeup, MailboxPON)
make verify-proper # PropEr stateful equivalence
make verify-c # Frama-C ACSLEstado real (RPT-16, 2026-08-14 — primeira execução completa e verde): TLA+/TLC 11/11 modelos sem erro, Coq 4/4 provas verificadas com coqc 8.20 (sem admit; PONComplexity.v, PONReceiveEquiv.v, PONTimer.v, TriColorGC.v), Frama-C/WP 23/23 goals provados (Frama-C 33.0 + Alt-Ergo, contratos em formal/framac/pon_acsl.c), PropEr 14/14 propriedades (200 testes cada, ERTS stock). O motor PON (MCE) passou o gate de qualidade (RPT-11: 6039 checks de equivalência, ASan/UBSan/TSan limpos). Validação formal e empírica documentadas em docs/ART-01-validacao-formal-matematica.md.
make docker-build # imagem com Stock OTP 30 + PON-BEAM (~30 min)
make bench-docker # benchmarks no container; relatórios em harness/results/docker/pon-beam/
├── otp/ # Fork de Erlang/OTP 30.0-rc0 (branch: pon-beam)
│ └── erts/emulator/beam/ # ERTS VM Core — overlay PON (#ifdef PON_BEAM)
│ ├── pon_matrix.c # Motor PON (MCE): nós, premisas, condições
│ ├── pon_virtual.c # PIDs virtuais: ring MPSC, roteamento
│ ├── pon_premise.c # Bookkeeping de premisas + parity mode
│ ├── pon_condition.c # ErtsCondition (eventfd+epoll) — Fase 4
│ ├── pon_ets.c # Watcher lateral PON-ETS — Fase 5 (funcional)
│ └── pon_gc.c # Hooks (instrumentação stats only)
├── pon-engine/ # Protótipo C standalone do motor PON (ASan/TSan)
├── formal/ # TLA+ | Coq | Frama-C | PropEr
├── harness/ # Harness comparativo (JSONs + HTML diff)
│ ├── config/ # ERTS paths (baseline.sh, ponbeam.sh)
│ ├── benchmarks/ # Cenários (fair_*, fase*, realworld_*, bench_stock_*)
│ │ └── pon_experiments/ # Experimentos PON (bench_*_vs_ponserver, smokes, pon_server)
│ ├── debug/ # Traces de depuração (bpftrace, etc.)
│ └── results/latest/ # Último snapshot: baseline/, ponbeam/, diff/
├── docs/ # Especificações, planos e relatórios (RPT-*)
│ ├── RPT-04-pon-scheduler.md # Fase 4 fechada por paridade + instigação causal
│ ├── RPT-05-pon-ets.md # Fase 5 fechada (watcher lateral funcional)
│ ├── RPT-09-pon-fair-comparison.md # Mediana 5 amostras (grupo controle)
│ ├── RPT-12-pon-etapa3-routing-e-snapshot-benchmark.md # Snapshot suíte
│ ├── RPT-16-pon-formal-validacao-suite.md # Suíte formal 4 pilares
│ ├── ART-01-validacao-formal-matematica.md # Artigo matemático da validação
│ └── EX-38-pon-beam-plano-de-engenharia.md # Plano de engenharia
├── Makefile
└── AGENTS.md
- 📋 Engineering Plan — plano de fases e critérios de aceitação
- 📊 RPT-04 — Fase 4 Scheduler — fechada por paridade + instigação causal
- 📊 RPT-05 — Fase 5 ETS — watcher lateral funcional (instigação causal)
- 📊 RPT-09 — Grupo controle fair — medição honesta da mediana de 5 amostras
- 📊 RPT-12 — Snapshot da suíte — roteamento + suíte completa
- 🔬 RPT-13 — Investigação do hang do receive — falsa positiva de driver de teste
- 🛡️ RPT-16 — Suíte formal 4 pilares — TLA+ 11/11 · Coq 4/4 · Frama-C 23/23 · PropEr 14/14
- 📐 ART-01 — Validação formal e empírica — artigo matemático da validação
- 🎓 Fundamento teórico: Notification-Oriented Paradigm (PON) — Simão & Stadzisz (2008–2009); tese base em
docs/EX-37-pon-beam-arquitetura-orientada-a-notificacoes.md
Licenciado sob a Apache License 2.0 (mesma licença do Erlang/OTP).