Test Automation

Spin/Promela Model Checking for Concurrent Systems Testing

HelpMeTest

HelpMeTest

— 7 min read
Spin/Promela Model Checking for Concurrent Systems Testing

Concurrent systems fail in ways that test suites almost never catch. A race condition that corrupts data might require a specific interleaving of 12 operations across 4 threads — a sequence that a random test might hit once in a billion runs, but that a model checker can find in seconds by exhaustively exploring all possible orderings. SPIN (Simple Promela INterpreter) is a model checker specifically designed for concurrent systems, and Promela (Process Meta Language) is the specification language it uses. Together they have been used to verify industrial protocols, device drivers, aerospace software, and network protocols including parts of the TCP/IP stack.

Why SPIN for Concurrency

The core problem with concurrent systems testing is the state explosion: with N concurrent processes each having K states, the total number of interleavings can be K^N or worse. Testing samples a tiny fraction of this space. Model checking explores all of it.

SPIN was created by Gerard Holzmann at Bell Labs in the 1980s and has been actively developed since. It won the ACM Software System Award in 2001. Unlike TLA+, which uses mathematical notation, Promela looks more like C code with channels, making it accessible to systems programmers.

SPIN checks:

  • Safety properties: Bad states never occur (deadlock, assertion violations, double-free)
  • Liveness properties: Good things eventually happen (using Linear Temporal Logic)
  • Acceptance properties: Patterns that must or must not occur infinitely often

Installing SPIN

SPIN is available as a binary for Linux, macOS, and Windows, and can also be compiled from source on GitHub at github.com/nimble-code/Spin.

# macOS with Homebrew
brew install spin

<span class="hljs-comment"># Verify installation
spin -V

SPIN generates C code that you compile into a verifier:

spin -a model.pml      # generate verifier source pan.c
gcc -O2 -o pan pan.c   <span class="hljs-comment"># compile verifier
./pan                  <span class="hljs-comment"># run verification

For LTL properties you need to claim them as part of the model or use the -f flag to inline them.

Promela Basics

Promela has processes (proctype), channels (chan), and a few control structures. Here is a minimal example — two processes competing for a shared variable:

int shared = 0;

proctype Writer1() {
  do
  :: shared = shared + 1
  od
}

proctype Writer2() {
  do
  :: shared = shared - 1
  od
}

init {
  run Writer1();
  run Writer2();
}

This model runs forever, but it illustrates the structure. Channels are the primary communication mechanism:

chan ch = [4] of { int };  /* buffered channel, capacity 4 */
chan sync = [0] of { int }; /* rendezvous (synchronous) channel */

proctype Sender() {
  ch ! 42;  /* send */
}

proctype Receiver() {
  int val;
  ch ? val; /* receive */
  assert(val == 42);
}

init {
  run Sender();
  run Receiver();
}

Verifying Mutual Exclusion

The classic test for any concurrent correctness tool is Peterson's algorithm for mutual exclusion. Let us model it and verify it:

bool flag[2];
int turn;

#define CS  /* critical section marker */

proctype P(int id) {
  int other = 1 - id;
  
  do
  :: /* try to enter critical section */
     flag[id] = true;
     turn = other;
     /* wait until either the other is not interested or it's our turn */
     (flag[other] == false || turn == id);
     /* critical section */
     CS;
     assert(flag[other] == false || turn == id); /* mutual exclusion */
     /* leave critical section */
     flag[id] = false
  od
}

init {
  atomic {
    run P(0);
    run P(1)
  }
}

To check mutual exclusion more rigorously, we need to track who is in the critical section:

bool flag[2];
int turn;
bool in_cs[2];

proctype P(int id) {
  int other = 1 - id;
  
  do
  :: flag[id] = true;
     turn = other;
     (flag[other] == false || turn == id);
     
     /* CRITICAL SECTION */
     in_cs[id] = true;
     assert(!in_cs[other]);  /* at most one process in CS */
     in_cs[id] = false;
     /* END CRITICAL SECTION */
     
     flag[id] = false
  od
}

init {
  atomic {
    flag[0] = false; flag[1] = false;
    in_cs[0] = false; in_cs[1] = false;
    run P(0);
    run P(1)
  }
}

Save this as peterson.pml and verify:

spin -a peterson.pml
gcc -O2 -o pan pan.c
./pan -m100000  # -m sets maximum state depth

SPIN explores all interleavings and verifies the assertion never fails. If you introduce a bug — say, remove the flag[id] = true line — SPIN finds the counterexample and prints the exact sequence of steps that leads to both processes being in the critical section simultaneously.

Deadlock Detection

SPIN automatically checks for deadlock (a state where all processes are blocked and no progress is possible). This is a built-in check that requires no extra annotations.

Here is a classic deadlock: two processes each holding one resource and waiting for the other:

chan lock1 = [1] of { bool };
chan lock2 = [1] of { bool };

init {
  lock1 ! true;  /* put token in lock1 */
  lock2 ! true;  /* put token in lock2 */
  run Process1();
  run Process2();
}

proctype Process1() {
  bool t;
  lock1 ? t;  /* acquire lock1 */
  lock2 ? t;  /* try to acquire lock2 -- will deadlock! */
  /* critical section */
  lock2 ! true;  /* release lock2 */
  lock1 ! true;  /* release lock1 */
}

proctype Process2() {
  bool t;
  lock2 ? t;  /* acquire lock2 */
  lock1 ? t;  /* try to acquire lock1 -- deadlock! */
  /* critical section */
  lock1 ! true;
  lock2 ! true;
}

Run SPIN and it finds the deadlock immediately:

pan: invalid end state (at depth 5)
pan: wrote deadlock.pml.trail

$ spin -t deadlock.pml  /* replay the trail */

The trail replay shows exactly which steps led to the deadlock. In a real system with 20 locks and 10 threads, this kind of exhaustive search is invaluable.

LTL Properties

Linear Temporal Logic lets you express temporal properties. The key operators:

  • [] p — p is always true (globally)
  • <> p — p is eventually true (finally)
  • p U q — p holds until q holds
  • X p — p holds in the next state

For liveness, you want to verify that processes make progress — they are not starved:

/* LTL property: process 0 always eventually enters CS */
ltl liveness0 { [] <> in_cs[0] }

/* LTL property: mutual exclusion holds always */
ltl mutex { [] !(in_cs[0] && in_cs[1]) }

Add these to your Promela file and SPIN verifies them automatically.

For the Peterson algorithm, we can also verify starvation freedom — that neither process is permanently blocked:

ltl no_starvation {
  [] (flag[0] => <> in_cs[0]) &&
  [] (flag[1] => <> in_cs[1])
}

This says: whenever a process raises its flag (indicating desire to enter CS), it eventually does enter the CS. This is a liveness property that Peterson's algorithm satisfies.

Embedded Systems Use Cases

SPIN is widely used in embedded systems and safety-critical software for several reasons: it handles the kinds of concurrent, interrupt-driven code that embedded systems use, and it does not require a full operating system or hardware to verify.

Device driver verification: Buffer overflow and use-after-free bugs in drivers often come from concurrent access between interrupt handlers and normal execution. A Promela model of the driver's state machine, the interrupt handler, and the DMA controller can verify that these races cannot corrupt state.

Communication protocol verification: The automotive CAN bus protocol, MODBUS, and industrial Ethernet protocols have been verified with SPIN. The model captures the message ordering, acknowledgment, and timeout behavior and verifies properties like "every sent message is eventually acknowledged or an error is raised."

RTOS task scheduling: Real-time operating systems have complex priority inversion and priority inheritance rules. Modeling the scheduler in Promela and checking that high-priority tasks always meet their deadlines under worst-case load is much more rigorous than testing with specific workloads.

A minimal embedded mutex model using SPIN looks like:

/* Simulate a binary semaphore / mutex */
chan mutex = [1] of { bool };

/* ISR - interrupt service routine */
proctype ISR() {
  bool tok;
  /* Try to take mutex -- if ISR can't, it drops the interrupt */
  if
  :: mutex ? [tok] -> /* non-blocking check */
     mutex ? tok;
     /* do work */
     mutex ! true
  :: else -> skip  /* drop if busy */
  fi
}

/* Main task */
proctype MainTask() {
  bool tok;
  do
  :: mutex ? tok;  /* blocking acquire */
     /* critical work */
     mutex ! true  /* release */
  od
}

init {
  mutex ! true;  /* initialize mutex as available */
  run MainTask();
  /* simulate periodic interrupts */
  do
  :: run ISR()
  od
}

Partial Order Reduction and State Space Management

The biggest practical challenge with SPIN is state explosion — large models can have billions of states. SPIN has several techniques to manage this:

Partial order reduction: If two independent actions commute (their order does not matter), SPIN only explores one ordering. This can reduce the state space by orders of magnitude for models where most processes are independent.

Bitstate hashing: Instead of storing each state explicitly, SPIN can use a hash table with bit representation. This trades completeness (you might miss a rare violation) for scalability. Use -DBITSTATE when compiling:

gcc -DBITSTATE -O2 -o pan pan.c
./pan -w28  # hash table with 2^28 bits (32 MB)

Bounded verification: Check only up to a certain depth with -m N. Bugs in concurrent systems almost always manifest within a few dozen steps.

Slicing: Remove parts of the model that are irrelevant to the property you are checking. SPIN has a program slicer that automates this.

SPIN in CI Pipelines

SPIN verification can run in CI for models that complete within a reasonable time bound:

name: SPIN Model Checking
on: [push, pull_request]
jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
      - name: Install SPIN
        run: sudo apt-get install -y spin gcc
      - name: Verify mutex protocol
        run: |
          spin -a specs/mutex.pml
          gcc -O2 -o pan pan.c
          ./pan && echo "No violations found"
          rm -f pan pan.c pan.b pan.h pan.m pan.t
      - name: Verify communication protocol
        run: |
          spin -a specs/protocol.pml
          gcc -O2 -o pan pan.c
          ./pan -m200000 && echo "No violations found"

The key is knowing which models are feasible to run in CI. Models with 3-5 processes and bounded loops typically complete in seconds to minutes. Larger models may need to run nightly or on dedicated hardware.

From SPIN Models to Code

One of the most powerful uses of SPIN is generating test cases from counterexamples. When SPIN finds a violation, it writes a trail file. You can replay the trail to see the exact sequence of events. For concurrent code, this tells you exactly which thread needs to be at which line, with which timing, to trigger the bug.

Some teams write automated test generators that take SPIN trail files and translate them to timing-controlled tests using tools like ThreadSanitizer or custom timing barriers. The model check finds the bug, the trail tells you the exact scenario, and the test locks in that scenario so the bug can never regress.

SPIN is 40 years old and still the best tool for verifying concurrent system correctness exhaustively. For any system where the phrase "race condition" or "deadlock" is a concern, it deserves a place in your verification toolkit.

Read more