# Distributed protocols

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.

## Acceptance procedure

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.

## Complexity

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

## Common failure

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

## Extensions

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

## Instances

- KL-FCS-052: Atomic acquisition with two processes — Mutual exclusion holds: yes
- KL-FCS-053: A race between check and acquisition — Mutual exclusion holds: no
- KL-FCS-054: Atomic acquisition with three processes — Mutual exclusion holds: yes

## References

- https://lamport.azurewebsites.net/tla/tutorial/session6.html