# A race between check and acquisition

KL-FCS-053 · Distributed protocols · version 1.0.0

## Problem

Check mutual exclusion over all one-shot lock-acquisition interleavings.

## Context

Treat atomicity and scheduling as part of a protocol model. A small interleaving can refute a plausible safety claim.

## Definitions

- **Atomic step**: An action observed as indivisible by other processes.
- **Mutual exclusion**: At most one process occupies its critical section.
- **Interleaving**: A sequence choosing one enabled process action at a time.

## Checked result

Mutual exclusion holds: no.

An atomic acquisition prevents simultaneous entry. A split acquisition can let both processes remember a free lock before either marks it occupied.

## Checker reasoning

1. Start all processes outside the critical section with a free lock.
2. Explore every enabled interleaving to a complete reachable closure.
3. Check the number of processes in the critical section at each state.
4. For a failure, replay the provided schedule to the unsafe state.

## Dataset construction

{
  "family": "protocols",
  "task": "Check mutual exclusion over all one-shot lock-acquisition interleavings.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete reachable interleaving graph",
  "acceptance": [
    "Start all processes outside the critical section with a free lock.",
    "Explore every enabled interleaving to a complete reachable closure.",
    "Check the number of processes in the critical section at each state.",
    "For a failure, replay the provided schedule to the unsafe state."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "processes": 2,
    "mode": "split",
    "state_encoding": "process PCs, lock bit, process saved-free bits; PC 0=start, 1=checked, 2=critical, 3=done",
    "atomicity": "Atomic mode tests and acquires together; split mode tests then acquires in separate steps."
  },
  "claim": {
    "mutual_exclusion": false
  },
  "witness": {
    "counterexample": [
      [
        0,
        0,
        0,
        0,
        0
      ],
      [
        1,
        0,
        0,
        1,
        0
      ],
      [
        1,
        1,
        0,
        1,
        1
      ],
      [
        2,
        1,
        1,
        1,
        1
      ],
      [
        2,
        2,
        1,
        1,
        1
      ]
    ]
  }
}
```

## Complexity

The finite state space is exponential in the number of processes; this family uses two or three one-shot processes.

## Limits

This is a shared-memory mutual-exclusion model. It does not verify a network protocol, message loss, liveness, or fairness.

## Common error and further work

Separating a lock check from acquisition allows another process to observe the same free lock.

Extend from shared-memory concurrency to bounded message queues and explicit network faults.

## Verification

Complete reachable interleaving graph. 26 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://lamport.azurewebsites.net/tla/tutorial/session6.html)