SKILL.md — Distributed Algorithms (Lynch)
license: Apache-2.0
name: distributed-algorithms-lynch
description: >
Reasoning framework for distributed systems design, correctness, and
impossibility — grounded in Lynch's formal automata-theoretic treatment.
Covers synchronous/asynchronous/partially-synchronous models, failure
models, consensus, and impossibility results as engineering constraints.
version: 1.0
activation_triggers:
- distributed systems design or architecture questions
- consensus, leader election, or coordination problems
- "is this possible?" questions about distributed guarantees
- fault tolerance and replication design
- debugging liveness or safety violations in distributed systems
- CAP theorem, FLP, Byzantine fault tolerance mentions
- questions about consistency models (linearizability, serializability)
- concurrent/shared-memory synchronization hierarchy questions
- formal verification of distributed protocols
- questions about timeouts, clocks, and timing assumptions
When to Use This Skill
Load this skill when someone is:
- Designing a distributed protocol and needs to know what's achievable
- Debugging a distributed system that "should work" but doesn't — often because they're attempting something impossible
- Evaluating claims that a system tolerates f failures, achieves consensus, or provides strong consistency
- Choosing between architectural options where the right choice depends on the timing or failure model
- Proving (or needing to prove) correctness of a concurrent or distributed algorithm
- Hitting a wall — when more engineering effort isn't fixing a fundamental problem
Signal phrases: "eventually consistent," "we can't get all nodes to agree," "our leader election is flaky," "we need linearizability," "how many failures can we tolerate," "is this CAP-related?"
Core Mental Models
1. The Four-Dimensional Design Space
Every distributed algorithm lives at a point defined by:
| Dimension | Options | Effect on Solvability |
|---|
| Communication | Shared memory / Message passing | Changes primitive power; most results translate via simulation |
| Timing | Synchronous / Asynchronous / Partially synchronous | Most consequential — determines what's provably achievable |
| Failure model | None / Crash / Omission / Byzantine | Determines n > kf thresholds and algorithm complexity |
| Problem class | Consensus / Election / Broadcast / Allocation | Different hardness in each timing+failure combination |
Practical implication: Before writing a line of code, identify where you are in this space. Moving even one dimension can flip a problem from unsolvable to trivial — or vice versa.
2. Impossibility Results Are Engineering Constraints
The foundational negative results are not academic — they are the most useful theorems in the book:
- FLP (Fischer-Lynch-Paterson): Consensus is impossible in a fully asynchronous system with even one crash failure
- Byzantine threshold: Consensus with Byzantine failures requires n > 3f processes
- Leader election lower bound: Any leader election algorithm requires Ω(n log n) messages
These mean: if you are in that regime and your protocol isn't working, no amount of debugging will fix it. The correct response is to relax an assumption — add a timeout (partial synchrony), strengthen failure detection, reduce the failure tolerance requirement.
3. Formal Models Are the Minimum Viable Reasoning Tool
Informal reasoning about concurrent systems fails — systematically and silently. Lynch's warning:
"Without such care, it is difficult to avoid mistakes."
The tools that work: state machines (I/O automata), invariant assertions, simulation relations, execution traces. Informal prose about distributed behavior is unreliable at the intersection of interleaving, timing, and failure modes. Use formal reasoning whenever correctness matters — not as gold-plating but as the minimum that actually works.
4. Modularity Through Atomic Abstraction
The atomicity composition theorem (Theorem 13.7): if each layer atomically implements its interface, the composed system is atomic. This enables:
- Prove correctness at layer N once
- All higher layers inherit it
- Replace implementations without re-proving upper layers
This is why atomicity/linearizability is the right correctness condition for building composable systems. Weaker conditions (sequential consistency, eventual consistency) don't compose cleanly. See references/reference-atomicity-and-consistency.md for the full treatment.
5. Every Tradeoff Is Quantifiable
Relaxations have measurable, provable benefits:
- k-set agreement (allow k distinct values) → round complexity divides by k
- Adding timing bounds → consensus achievable in Ld + (f−1)d time
- Crash vs. Byzantine tolerance → Byzantine costs a factor of n in message complexity
- Synchronous vs. asynchronous → same problem can be O(f) rounds vs. impossible
When someone says "we'll just relax consistency a bit," the Lynch framework demands: which relaxation, by exactly how much, and what do you gain?
Decision Frameworks
When someone asks "can we solve X in our distributed system?"
1. Identify timing model: Is there a bound on message delay? Process speed?
→ Synchronous: most problems solvable
→ Asynchronous: check impossibility results FIRST
→ Partially synchronous: consensus achievable, with caveats
2. Identify failure model: What failures must be tolerated?
→ Crash: n > 2f for most consensus variants
→ Byzantine: n > 3f required, no exceptions
3. Check known impossibility results:
→ Async + any crash failure + consensus = IMPOSSIBLE (FLP)
→ Byzantine + n ≤ 3f = IMPOSSIBLE
→ If impossible, ask: which assumption can we relax?
4. If possible: what are the complexity costs?
→ Time complexity: rounds or real-time bounds?
→ Message complexity: O(n²) or O(n log n)?
→ Is that acceptable for the use case?
When a distributed protocol "isn't working"
If the system seems correct but non-terminating (liveness issue):
→ Check: are you in an asynchronous model with failures? (→ FLP applies)
→ Check: is your failure detector strong enough? (eventually perfect ◇P?)
→ Check: are timing assumptions actually met in deployment?
If the system terminates but produces wrong values (safety issue):
→ Check: is your failure threshold n > 2f (crash) or n > 3f (Byzantine)?
→ Check: are atomic operations actually atomic? (linearizability)
→ Formalize executions as state traces; find the invariant violation
If behavior is inconsistent across nodes:
→ Check: which consistency model are you actually implementing?
→ Linearizability ≠ sequential consistency ≠ eventual consistency
→ These do not compose interchangeably
When choosing a consistency/coordination model
Need strong composability? → Linearizability (atomic objects)
Need only single-object correctness? → Sequential consistency (weaker, cheaper)
Tolerating staleness? → Eventual consistency (but: no FLP escape
without also giving up something else)
Need consensus specifically? → Must be partially synchronous at minimum;
identify failure detector class needed
When designing for fault tolerance
f failures to tolerate:
Crash stop → need n > 2f, use crash-tolerant consensus (Paxos-family)
Byzantine → need n > 3f, use BFT protocol (cost: O(n) factor overhead)
Failure detector availability:
Perfect P → synchronous system or unrealistic assumption
Eventually ◇P → achievable in partially synchronous systems; sufficient for consensus
If you can't afford n > 3f:
→ Reduce f (tolerate fewer failures)
→ Use cryptographic authentication to convert Byzantine → authenticated Byzantine
(reduces to n > 2f with authentication)
Reference Files
Load these on demand based on what's needed:
| File | When to Load |
|---|
references/impossibility-results-as-engineering-constraints.md | Someone is attempting something that might be provably impossible; FLP, Byzantine thresholds, or lower bounds are relevant; need to justify stopping or changing approach |
references/timing-models-and-their-consequences.md | Choosing between synchronous/asynchronous/partially-synchronous architectures; timeouts and failure detectors are in scope; "why does consensus work here but not there?" |
references/failure-models-and-fault-tolerance.md | Designing fault-tolerant systems; evaluating how many failures a system can handle; Byzantine vs. crash fault distinction matters |
references/distributed-consensus-the-complete-picture.md | Consensus, Paxos, Raft, leader election, atomic broadcast, or any agreement protocol is under discussion; need the complete problem taxonomy |
references/formal-proof-methods-for-distributed-systems.md | Proving correctness; finding subtle bugs via formal reasoning; invariant-based arguments; simulation relations needed |
references/synchronization-primitives-and-atomic-objects.md | Shared-memory concurrency; compare-and-swap power hierarchy; wait-free vs. lock-free; building atomic objects from weaker primitives |
references/algorithm-design-patterns-and-canonical-problems.md | Need a known algorithm for a canonical problem (broadcast, election, snapshot); looking for a design pattern; connecting a new problem to a known one |
references/reference-impossibility-results.md | Need the full theoretical treatment of impossibility at Lynch's level of rigor — complete landscape of what cannot be built and why |
references/reference-timing-and-partial-synchrony.md | Need deep formal treatment of the three timing models; partial synchrony, GST, and real-time bounds on specific protocol guarantees |
references/reference-formal-models-and-proof-methods.md | Need the foundational I/O automata model and full formal proof machinery for reasoning about interleaved executions |
references/reference-atomicity-and-consistency.md | Building composable services from atomic objects; atomicity composition theorem in depth; what shared state can and cannot do |
references/reference-algorithm-families-and-patterns.md | Want the full taxonomy of algorithm families by problem class — why canonical solutions are minimal and their complexity signatures |
Anti-Patterns
These are mistakes Lynch's framework directly prevents:
1. Trying to solve consensus in a pure async system
Spending weeks tuning a consensus protocol that will never terminate under failures. FLP says: relax the timing model, don't add more retries.
2. Under-counting processes needed for Byzantine tolerance
Assuming n > 2f suffices when Byzantine failures are possible. The correct threshold is n > 3f. Systems with n = 3 tolerating 1 Byzantine fault are unsound.
3. Treating consistency models as interchangeable
Mixing linearizable and sequentially consistent components assuming the result is linearizable. Atomicity composes; weaker conditions don't.
4. Informal reasoning about interleaving
Writing prose arguments about why "this can't happen" in concurrent execution. Informal concurrent reasoning fails silently. The fix: state machines and invariant assertions.
5. Conflating safety and liveness failures
Treating a liveness bug (system halts) the same as a safety bug (system produces wrong result). They have different causes, different impossibility results, and different fixes.
6. Ignoring the failure detector requirement
Implementing consensus in a "partially synchronous" system without specifying what failure detector is available and whether it's sufficient (◇P is the minimum for consensus).
7. Assuming relaxed consistency is "free"
Choosing eventual consistency to escape CAP/FLP constraints without accounting for what application-level invariants now become the programmer's problem.
Shibboleths
How to tell if someone has actually internalized Lynch vs. just read the summary:
✓ Internalized: When told "our consensus is broken," their first question is "what's your timing model and failure model?" — not "what algorithm are you using?"
✓ Internalized: They know FLP is about asynchronous systems specifically, and immediately ask "so what synchrony assumption does your system actually make?" rather than concluding "consensus is impossible."
✓ Internalized: They distinguish between the possibility result (can we solve this at all?) and the complexity result (at what cost?) as two separate questions requiring separate answers.
✓ Internalized: When someone says "we use eventual consistency," they ask "eventual consistency of what? Under what conflict resolution rule? With what convergence guarantee?" — not just nod.
✓ Internalized: They know the synchronizer doesn't make async systems synchronous — it provides a simulation that preserves certain properties, and they know which properties are and aren't preserved.
How to spot someone who only read the summary:
✗ They cite FLP as a reason consensus is "basically impossible" without specifying the async model assumption.
✗ They say "Byzantine fault tolerance requires 3x the nodes" without knowing why 3f+1 and not 2f+1 (the triangle argument: can't distinguish which third is lying).
✗ They treat "linearizable" and "serializable" as synonyms.
✗ They believe adding more replicas always increases fault tolerance (it does for availability; for Byzantine tolerance it requires n > 3f which is a different constraint).
✗ They argue informally that "the race condition can't happen in practice" rather than proving it can't happen via invariant.
Bundled Assets
See references/INDEX.md for the complete listing of all twelve reference documents with per-document loading triggers.
Load reference files from the table above when deeper treatment of a specific topic is needed.