Module recover 

Crash recovery (spec §23.1).

A turn writes a phase marker as it goes, and a crash leaves that marker behind. Recovery reads it, together with the command journal, and decides which of four things to do — and the order the decision is taken in is the safety property, because two of the four would be wrong if taken first:

1. An unknown external outcome is reconciled, never retried. A command that timed out after transmission may have taken effect. Repeating it would be the duplicate the whole library exists to prevent, so this case is checked before anything else (§16.5, I15).
2. Pending commands are resumed by idempotency key. An entry in Pending or Executing was admitted and may or may not have reached the domain. Running it again is safe only through the key, which is why recovery hands back the entries rather than the plan.
3. A committed turn regenerates its response. The effects are done; what is missing is the answer. It is rebuilt from the committed events and the stored plan, and nothing is executed.
4. A turn with no journal entry restarts interpretation. Nothing was admitted, so nothing can have happened, and the turn may simply be interpreted again.

Why the answer tasks come back from the plan

§23.1 asks for the response to be regenerated “from events and stored answer tasks”. The reduction is pure, so its questions are exactly the questions of the accepted plan the replay record already stores — no separate table is needed, and re-deriving them cannot drift from what the turn actually planned. Their basis is normalized to AnswerBasis::CurrentCommittedState: after commit, “what will be true after this turn” and “what is true now” are the same state, and the second is the one that can be read.

Structs

Recovery

Reads what a crashed turn left behind and decides what to do about it.

Enums

RecoveryAction

What recovery decided to do with a turn (spec §23.1).

Functions

answer_tasks_of

The answer tasks a stored replay record implies (spec §23.1), with the question words read from the turn’s text. The basis becomes the committed state, because the turn’s commands have already committed by the time this runs.

committed_event_ids

Every event identifier a turn’s settled journal entries committed.