Tools Spin Model

---
name: tools-spin-model
description: Create a new Spin/Promela formal verification model for a system property
argument-hint: "[property-number or description of property to prove]"
---

Create a new Spin/Promela specification in `modelling/spin/<name>/` to verify a concurrency property of the Certus system.

## Input

If no argument is provided, first ask the user to define the **scope**, then present the property menu.

### Step A: Scope Selection

Ask the user to choose the modeling scope:

- **Single component** — Model the internal concurrency of one component in isolation (e.g., just the dispatcher, just the extent-manager, just the block-device actor). Threads and channels within that component are modeled explicitly; interactions with other components are abstracted as nondeterministic environment stubs.
- **Whole system** — Model the interaction between multiple components as wired together in certus-server (e.g., client → dispatcher → memory-tier → block-device → extent-manager). Includes cross-component communication channels, the gRPC thread pool, and background workers.

The scope determines:
- Which source files to read (single component = one crate's `src/`; whole system = multiple crates + `apps/certus-server/`)
- How to abstract boundaries (single = environment stubs with nondeterministic responses; whole = explicit `proctype` per component role)
- Model complexity (single = fewer processes, deeper per-component detail; whole = more processes, coarser per-component abstraction)

### Step B: Property Selection

Present the full property menu and ask the user to choose. The user may also describe a custom property.

**System-level properties** (scope: whole system recommended):

1. **Reference-count balance** — Every read_ref increment has a matching decrement on all paths. No leaked refs (memory leak) or double-decrements (use-after-free).
2. **Write-before-evict** — Models the dispatcher's populate → write-through → eviction lifecycle to verify that memory-tier eviction never produces dangling SSD references.
3. **Cold-path promotion atomicity** — At most one thread succeeds in promoting a given key from SSD to memory-tier. No double-allocation or lost updates.
4. **Populate-lookup linearizability** — After populate(key) returns Ok, a concurrent lookup(key) never observes KeyNotFound unless an explicit remove or eviction intervened.
5. **Shutdown ordering** — No NVMe command is issued after its block device shuts down. Background writer drains before drives are torn down.
6. **No lost extents** — Every reserve_extent is followed by either publish() or drop (abort). No extent is permanently allocated but uncommitted.

**Component-level properties** (scope: single component recommended):

7. **Pipeline ring slot safety** — A ring buffer slot is never resubmitted for NVMe read while its CUDA DMA transfer is still in flight. (Component: dispatcher/pipeline)
8. **Starvation freedom** — No client is starved indefinitely waiting to enqueue a write job under backpressure. (Component: dispatcher/background)
9. **Eviction fairness** — An entry touched within the last N operations is never evicted while untouched entries exist. (Component: dispatcher/eviction)
10. **Actor mailbox ordering** — Messages sent to a block-device actor are processed in FIFO order; no command reordering across the channel boundary. (Component: block-device-spdk-nvme)
11. **Extent bitmap consistency** — Concurrent reserve/publish/remove never leave the bitmap in a state where an extent is both allocated and free. (Component: extent-manager)

If the user provides a number (1-11), use that property. If they provide free text, treat it as a custom property description and ask for a short kebab-case name for the subdirectory.

## Steps

1. **Determine the property and directory name.**

   Map selections to directory names:
   - 1 → `ref-count-balance`
   - 2 → `write-before-evict`
   - 3 → `promotion-atomicity`
   - 4 → `populate-lookup-linearizability`
   - 5 → `shutdown-ordering`
   - 6 → `no-lost-extents`
   - 7 → `pipeline-ring-safety`
   - 8 → `starvation-freedom`
   - 9 → `eviction-fairness`
   - 10 → `actor-mailbox-ordering`
   - 11 → `extent-bitmap-consistency`
   - Custom → ask user for a kebab-case name

2. **Read the relevant source code** to understand the real synchronization protocol.

   Key source files by property and scope:

   **Whole-system scope** (read certus-server wiring + component internals):
   - 1,4: `components/dispatcher/src/lib.rs` (populate, lookup, evict_for_space, batch_lookup)
   - 2: `components/dispatcher/src/lib.rs` + `components/dispatcher/src/background.rs`
   - 3: `components/dispatcher/src/lib.rs` (batch_lookup cold-path promotion, lines ~1045-1215)
   - 5: `components/dispatcher/src/lib.rs` (shutdown), `components/dispatcher/src/background.rs` (BackgroundWriter::shutdown), `apps/certus-server/src/main.rs` (shutdown sequence)
   - 6: `components/dispatcher/src/lib.rs` (prepare_store, commit_store, cancel_store, process_write_job)

   **Single-component scope** (read only the target component):
   - 7: `components/dispatcher/src/pipeline.rs` (PipelineRing, pipelined_ssd_to_gpu_zero_copy)
   - 8: `components/dispatcher/src/background.rs` (channel + worker_loop)
   - 9: `components/dispatcher/src/lib.rs` (evict_for_space, mt.evict_lru, mt.oldest_keys)
   - 10: `components/block-device-spdk-nvme/src/` (actor thread, command channel, completion channel)
   - 11: `components/extent-manager/src/` (bitmap allocation, reserve_extent, publish, remove_extent)

   Also reference the existing model at `modelling/spin/write-before-evict/write_before_evict.pml` for style and conventions.

3. **Create the subdirectory** `modelling/spin/<name>/`.

4. **Write the Promela specification** `modelling/spin/<name>/<name_underscored>.pml`.

   Follow these conventions (from the existing write-before-evict model):
   - Header comment block explaining what is being verified, the scope, and how to run
   - `#define` parameters section (N_CLIENTS, N_KEYS, etc.) tuned small for tractable state space
   - Per-key or per-resource state as `mtype` enums and arrays
   - `proctype` for each thread role in the system
   - `inline` helpers for shared logic (like eviction)
   - Inline `assert()` statements for safety properties
   - `init` process that starts all proctypes, waits for completion, signals shutdown, runs final invariant checks
   - Aim for 100% state coverage (no unreached states)
   - Use `atomic{}` for operations that share a mutex in the real code
   - Use `d_step{}` for deterministic sequences (scans)
   - Use generation counters to handle key reuse across lifecycles
   - Model channels as bounded `chan` (even if real code uses unbounded)

   **Scope-specific conventions:**

   For **single component** models:
   - Abstract external interfaces as nondeterministic stubs (e.g., `if :: success :: failure fi`)
   - Focus on internal thread interactions and shared state
   - Name the header comment "Component-level model: <component-name>"
   - Document which interfaces are stubbed and what assumptions are made

   For **whole system** models:
   - One `proctype` per major thread role across components
   - Use channels to model inter-component communication (gRPC, receptacles)
   - Name the header comment "System-level model: <property-name>"
   - Document the component wiring in the header

5. **Write the Makefile** `modelling/spin/<name>/Makefile`:

   ```makefile
   MODEL = <name_underscored>.pml
   PAN   = pan
   CC    = cc
   CFLAGS = -O2
   DEPTH = 200000

   .PHONY: all safety liveness clean

   all: safety

   safety: $(PAN)
   	./$(PAN) -m$(DEPTH)

   liveness: $(PAN)-live
   	./$(PAN)-live -a -m$(DEPTH)

   $(PAN): pan.c
   	$(CC) $(CFLAGS) -DSAFETY -o $@ $<

   $(PAN)-live: pan.c
   	$(CC) $(CFLAGS) -o $@ $<

   pan.c: $(MODEL)
   	spin -a $<

   clean:
   	rm -f $(PAN) $(PAN)-live pan.* *.trail
   ```

6. **Write the README.md** `modelling/spin/<name>/README.md`:

   Structure (follow the pattern in `modelling/spin/write-before-evict/README.md`):
   - Title: `# <Property Name>`
   - **Scope**: Single component (`<component-name>`) or Whole system
   - One-paragraph description of what the model verifies
   - **Properties Verified** table (ID, Property description, Type: Safety/Liveness)
   - **System Abstraction** table (Real component → Promela process)
   - **Assumptions / Stubs** section (for single-component scope: list what is abstracted away and how)
   - **Running** section with shell commands
   - **Tuning the Model** section explaining parameters
   - **Correspondence to Source Code** table (Model location → Source file → Line range)

7. **Run the verification** by executing `make` in the new directory.

   - If Spin is not installed, inform the user and skip this step.
   - If verification fails with an assertion violation, analyze the trail (`spin -t -p <file>.pml`), fix the model, and re-run until it passes.
   - Report: number of states explored, depth reached, errors found, coverage (unreached states).

8. **Report results** to the user:
   - Scope (single component or whole system)
   - Property being verified
   - Pass/fail status
   - State space size
   - Coverage (target: 0 unreached states in all proctypes)
   - Path to the new model directory

## Notes

- Spin must be installed at `/usr/local/bin/spin` (see `modelling/spin/write-before-evict/README.md` for install instructions).
- Keep parameters small (2-3 clients, 2-4 keys, pool cap < key count) to maintain tractable state spaces (<10M states).
- The model should be self-contained — no external dependencies beyond Spin and a C compiler.
- Use the generation-counter technique from the write-before-evict model to handle key reuse without conflating lifecycles.
- Single-component models are faster to verify (fewer processes) and better for finding internal races.
- Whole-system models catch cross-component protocol violations but have larger state spaces.