BEAM VM Model Checker: Feasibility Analysis

A comparison of JMC's approach for Java with what would be needed for Erlang/Elixir on the BEAM VM.

1. Bytecode Equivalent in BEAM VM

Java (JVM)	BEAM VM
Java Bytecode (.class files)	BEAM Bytecode (.beam files)
- Stack-based instruction set	- Register-based instruction set
- Manipulated via ASM/ByteBuddy	- Manipulated via beam_lib, beam_disasm
- Well-documented format	- Less documented, but parseable

Key Difference: BEAM bytecode is designed for the actor model and message passing, not shared memory concurrency. Instructions focus on process spawning, message send/receive, and pattern matching rather than thread synchronization primitives.

2. Key Challenges

2.1 Concurrency Model Mismatch

• JMC: Controls thread scheduling via Thread.yield() interception and executor service wrapping
• BEAM: Processes are scheduled by the VM's internal scheduler; no direct API to control scheduling
• Challenge: Would need to modify the BEAM VM itself or use tracing/debugging hooks

2.2 Message Passing vs Shared Memory

• JMC: Intercepts locks, volatile reads/writes, and thread operations
• BEAM: Would need to intercept send (!) and receive operations
• Challenge: Message passing is more coarse-grained; state space might be smaller but each state is more complex

2.3 VM Internals Access

• JMC: Uses Java agents (-javaagent) with well-defined instrumentation APIs
• BEAM: Limited instrumentation support; would need:
  • NIFs (Native Implemented Functions) for deep VM access
  • Tracing (erlang:trace/3) for observability but not control
  • Potentially VM modifications (fork of OTP)

2.4 Process Isolation

• JMC: Threads share heap; can track shared state
• BEAM: Processes have isolated heaps; state is in mailboxes and process dictionaries
• Challenge: Harder to define "equivalent states" for state space reduction

2.5 Hot Code Loading

• BEAM: Supports hot code swapping during execution
• Challenge: Model checker would need to handle code version transitions

3. JMC Architecture Applicability

JMC Components

JMC Architecture:
├── Runtime: Scheduler control, state tracking
├── API: Replacement concurrent primitives (JmcExecutorService, etc.)
└── Agent: Bytecode transformation (visitors for Thread, Lock, Executor, etc.)

Direct Applicability Analysis

✅ Runtime Component - Partially Applicable

• JMC Approach: Central scheduler that decides which thread runs next
• BEAM Equivalent: Would need a "meta-scheduler" that controls BEAM's process scheduler
• Feasibility:
  • Could work if implemented as VM modification
  • Tracing alone insufficient (observe-only, not control)
  • NIF-based approach might work but would be invasive

❌ API Component - Not Directly Applicable

• JMC Approach: Provides JmcExecutorService, JmcLock, etc. that applications use
• BEAM Equivalent: Would need GenServer, Task, Agent replacements
• Problem:
  • BEAM's concurrency is built-in (spawn, send, receive are VM primitives)
  • Can't easily "replace" them like Java's library-level abstractions
  • Would require language-level changes or compiler plugins

⚠️ Agent Component - Partially Applicable

• JMC Approach: Bytecode visitors transform Thread/Executor/Lock operations
• BEAM Equivalent: Would need BEAM bytecode transformers for spawn/send/receive
• Feasibility:
  • BEAM bytecode is transformable (tools exist: beam_lib, beam_disasm)
  • Could inject hooks before/after message operations
  • Challenge: Transforming receive is complex (pattern matching, timeouts, selective receive)

Architecture Recommendation

For BEAM VM, a different architecture would be more practical:

BEAM Model Checker Architecture:
├── VM Hooks: Tracing + NIF-based scheduler control
├── Instrumentation: BEAM bytecode transformation for send/receive/spawn
└── Scheduler: External process that controls message delivery order

Why Different?

1. No API Layer: BEAM's concurrency is VM-level, not library-level
2. VM Integration Required: Need deeper VM access than Java agents provide
3. Message-Centric: Focus on message interleaving, not thread interleaving

4. Existing Work

• Concuerror: Existing model checker for Erlang that uses similar ideas
  • Uses instrumentation and controlled scheduling
  • Proves this approach is viable
• QuickCheck/PropEr: Property-based testing tools with some concurrency support
  • Don't provide full scheduling control
  • Complementary approach

5. Feasibility Verdict

Is JMC's approach directly applicable?

No, but the core ideas are transferable with significant adaptation:

Aspect	Directly Applicable?	Adaptation Needed
Bytecode instrumentation	✅ Yes	Different instruction set, focus on send/receive
Scheduling control	❌ No	Need VM hooks or modifications, not just agent
State space exploration	✅ Yes	Same algorithms work (DFS, random, DPOR)
Replay capability	✅ Yes	Record message delivery order instead of thread schedule
API replacement layer	❌ No	BEAM concurrency is VM-primitive, not library-based

Bottom Line: Building a JMC-like tool for BEAM is feasible but requires deeper VM integration than JMC needs for Java. The instrumentation approach works, but you'd need to either modify the BEAM VM or use a combination of NIFs and tracing that JMC doesn't require.