Put the network in the state

The client cannot distinguish two worlds after a timeout. In one world, the service never applied the deposit. In the other, the service applied it and the reply was lost. A model that treats timeout as proof of failure erases the second world before a checker can explore it.

---------------------------- MODULE RetryLedger -----------------------------
EXTENDS Naturals

VARIABLES requests, balance, replyLost, lastAction
vars == <<requests, balance, replyLost, lastAction>>

Init ==
  /\ requests = {}
  /\ balance = 0
  /\ replyLost = FALSE
  /\ lastAction = "init"

ApplyBug ==
  /\ balance' = balance + 1
  /\ requests' = requests
  /\ replyLost' = TRUE
  /\ lastAction' = "apply"

RetryBug ==
  /\ replyLost
  /\ balance' = balance + 1
  /\ UNCHANGED <<requests, replyLost>>
  /\ lastAction' = "retry"

ApplyFixed ==
  /\ requests = {}
  /\ requests' = {"deposit-7"}
  /\ balance' = balance + 1
  /\ replyLost' = TRUE
  /\ lastAction' = "apply"

RetryFixed ==
  /\ replyLost
  /\ requests' = requests
  /\ balance' = IF "deposit-7" \in requests THEN balance ELSE balance + 1
  /\ UNCHANGED replyLost
  /\ lastAction' = "retry"

NextBug == ApplyBug \/ RetryBug
NextFixed == ApplyFixed \/ RetryFixed

AtMostOnce == balance <= 1
TypeOK ==
  /\ requests \subseteq {"deposit-7"}
  /\ balance \in 0..2
  /\ replyLost \in BOOLEAN
  /\ lastAction \in {"init", "apply", "retry"}

=============================================================================

Run the known defect:

java -jar tla2tools.jar -config RetryBug.cfg RetryLedger.tla

The negative control expects TLC to violate AtMostOnce. The shortest trace is ApplyBug followed by RetryBug. balance becomes two even though the user asked for one logical deposit.

Bind identity to the effect

ApplyFixed records deposit-7 and increments balance in the same modeled step. RetryFixed checks the request set before changing the balance. Run the repaired protocol:

java -jar tla2tools.jar -config RetryFixed.cfg RetryLedger.tla

The model makes the atomicity requirement visible. A production database must store the request identity and the business mutation in one transaction or in an equivalent indivisible operation. Writing the identity after the balance would create a crash window in which the retry still duplicates the effect.

Google Cloud Datastore transactions, Spanner transactions, a SQL uniqueness constraint, or a compare-and-set record can implement that indivisibility under different assumptions. The model does not inherit a product guarantee merely because a product name appears in the design. The implementation review must cite the exact transaction and durability contract it uses.

Beyond one request

The lab fixes one identity and permits a balance of at most two. A real model needs a finite set of request identifiers, payloads, clients, retry counts, and crash points. The safety property usually changes from balance < 1= to a relation: every applied effect has exactly one logical request identity, and replays of that identity return a stable receipt.

Liveness needs another workshop. The service cannot promise that every request finishes unless the model names delivery, retry, storage, and scheduling assumptions. At-most-once effect is a safety claim. Eventual response is a progress claim.

Practice

1. Insert a Crash action between updating balance and recording the identity. Predict the duplicate trace.
2. Explain why a random UUID reduces collision risk but does not itself make two writes atomic.
3. State one safety claim and one liveness claim for the repaired service.

Worked answer

1. Apply the balance change, crash before identity storage, restart with no recorded identity, then retry and apply again.
2. UUID uniqueness distinguishes requests. Atomic storage determines whether the identity and effect survive together.
3. Safety example: no request identity contributes more than one effect. Liveness example: every admitted request eventually receives a stable receipt under named delivery and service fairness assumptions.

Lessons

• A timeout reports missing observation, not remote failure.
• The network and reply status belong in the state when they affect retries.
• Durable request identity turns retry into lookup rather than repeated effect.
• Identity and mutation must share one atomic durability boundary.
• Safety and liveness need different properties and assumptions.

References

1. Google Cloud. “Transactions.” Firestore in Datastore mode. — transaction behavior and retry guidance.
2. Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — safety, liveness, and temporal specifications.