PON-BEAM — Notification-Oriented BEAM Virtual Machine

⚠️ 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 (receive O(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.

---

📋 Estado real por fase

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.

---

🔬 O que existe de verdade hoje

• 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,3 roteado, send_after, drain FIFO, inventário de BIFs — tudo validado por smokes e stress.
• Telemetria real no ERTS: erlang:system_info(pon_stats) retorna premises_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): ErtsCondition real com eventfd+epoll, FIFO estrita com node próprio PonSchedNode, notify no add2runq e drain no scheduler_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 polling ets:lookup; fechado por instigação causal funcional + paridade (RPT-05).
• Suíte formal: TLA+/TLC 11/11 modelos, provas Coq 4/4 verificadas com coqc 8.20 (sem admit), Frama-C/WP 23/23 goals provados (Frama-C 33.0 + Alt-Ergo), PropEr 14/14 propriedades — 4 pilares verdes (RPT-16, ART-01).

---

🏛 Arquitetura (visão de projeto — nem tudo implementado)

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).

---

📊 Medições honestas

Placar em 30 segundos (mediana de 5 amostras, +S 8:8 — RPT-09, atualizado 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.

Detalhe 1 — Grupo controle fair (mediana de 5 amostras, +S 8:8, RPT-09, 2026-08-06)

Cenários de fortaleza da BEAM original (não selecionados a favor do PON). Razão stock/pon: >1 = PON mais rápido.

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.

Detalhe 2 — Snapshot da suíte completa (1 amostra/cenário — RPT-12, 2026-08-11)

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 em fase1_receive* (0.27–0.62×) (pré-fix do head, errata RPT-12 §5.2), fair_memory 0.58×, fair_spawn 0.36× (pré-gates; paridade em RPT-15), fifo_pingpong 0.49×, fair_compute 0.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 caminho receive sob 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 de harness/results/latest e, 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

---

🛠 System Requirements

• 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.

---

🚀 Building PON-BEAM

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-debug

Iteração rápida no C do emulador:

make emulator-pon    # recompila só o ERTS PON (~1–3 min)
make emulator-stock  # recompila o ERTS stock

---

📊 Benchmark Harness & Relatórios

Harness 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 diferencial

---

🛡️ 4-Pillar Formal Verification Suite

graph 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 ACSL

Estado 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.

---

🐳 Docker

make docker-build     # imagem com Stock OTP 30 + PON-BEAM (~30 min)
make bench-docker     # benchmarks no container; relatórios em harness/results/docker/

---

📁 Repository Structure

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

---

📚 Documentation & References

• 📋 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

---

📄 License

Licenciado sob a Apache License 2.0 (mesma licença do Erlang/OTP).