transaction-protocol-reasoning

name	transaction-protocol-reasoning
description	Teaches how to reason from a transaction protocol’s rules to a working model. Use when analyzing a concurrency-control paper, spec, or algorithm to identify state, metadata, invariants, operation rules, examples, counterexamples, guarantees, false aborts, unsafe commits, or tradeoffs before inspecting concrete traces.

Transaction Protocol Reasoning

Use this skill when a protocol is already given (paper, spec, pseudocode, implementation notes) and you need to understand what it guarantees and how its rules imply commit/abort behavior.

This skill does not ask you to invent a protocol. It teaches how to read a protocol description as a set of rules, turn those rules into checkable predicates/invariants, and then reason about safety vs conservatism.

What “done” looks like

By the end you should have:

• a one-page Protocol Ledger (state + rules + invariants)
• a minimal example pack (3–6 tiny histories) that exercises boundaries
• a clear statement of:
  • the protocol’s proof object (what metadata it relies on), and
  • its likely false-abort and unsafe-commit failure modes

Quick Reference (pick the next file to read)

If you need…	Read
A step-by-step protocol reading workflow	protocol-analysis-workflow.md
Inventory protocol state + what each field proves	state-and-metadata-modeling.md
Restate read/write/validate/commit/abort as explicit rules	operation-rule-analysis.md
Extract invariants from rules (and distinguish conservative ones)	invariant-extraction.md
Build a small history suite that hits boundary behavior	example-construction.md
Build minimal counterexamples (unsafe commit vs conservative abort)	counterexample-construction.md
Compare two protocols by guarantees + metadata + allowed histories	protocol-comparison.md

Protocol Ledger (the “shape ledger” equivalent)

Before you chase details, build a one-page protocol ledger:

Claimed guarantee:

Global state:
  - per-object metadata: ...
  - global clock/counters: ...

Per-transaction state:
  - read set entries: (key, version-id?, local ts fields?, ...)
  - write set entries: (key, buffered value?, lock?, ...)
  - timestamps: start_ts?, commit_ts?, bounds?

Operations (as rules/predicates):
  read(key): preconditions, version selection, metadata recorded/updated, failure modes
  write(key): ...
  validate(txn): ...
  commit(txn): ...
  abort/retry(txn): ...

Proof object:
  - what metadata/rules constitute the correctness argument?
  - what does the protocol “check” to justify commits?

If you cannot fill a ledger line item without hand-waving (“it probably…”), you have found an underspecified part of the protocol. That is often where conservative aborts come from.

Workflow (operational)

1. Extract the contract: what does “correct” mean and what is in-scope?
2. Inventory state: list each field, its scope, and what history fact it is intended to prove.
3. Restate rules: convert prose/pseudocode into explicit “if … then … else abort/block” rules.
4. Derive invariants: state what must always be true if the rules are correct.
5. Run the example pack: step through 3–6 tiny histories and apply the rules mechanically.
6. Locate conservative vs unsafe edges:
   • conservative: rules reject a safe history (false abort / blocking)
   • unsafe: rules accept a history that violates the contract

Common Failure Modes To Look For

• Metadata insufficiency: protocol needs old-version validity but stores only latest.
• Scope mismatch: uses per-key evidence to enforce cross-key ordering claims.
• Over-approx validation: uses a sufficient condition (safe) that is not necessary (causes false aborts).