M3.13f: the version-seven store's faults and recovery - #220
Conversation
ADR 0057 recorded two things as owed: fault-injection coverage of the version-seven write path, and recovery after a commit whose outcome is unknown. This is the second, and settling it corrected the first. The original code poisoned the store on any write failure, which was safe and wrong. Everything before the commit rolls back and writes nothing, so a fault there is an ordinary refusal: the durable head is the one it already was and the store stays usable. Only the commit can leave a head this process cannot name, and there the store poisons itself and then reads the file again — closing the connection, reopening it, running the same four validation steps an ordinary open runs, and adopting whatever head the file actually holds. That head is either the block's or its predecessor's, because SQLite's transaction is what decides. Recovery is `noexcept` and answers `false` rather than throwing. A store that could not read its own file back stays poisoned and refuses every later call, which is a worse state and an honest one. The seven fault points version one already defines are wired into the write path, with the two post-commit points invoked and ignored so a test can terminate the process there.
The property is the one requirement 13 names when it says "through restart *and recovery*": a fault anywhere in the write path leaves the durable head at the pre-block root or the post-block root, and never at anything between. Each of the four pre-commit faults is driven and then cleared, and the block that follows must reproduce its recorded root — which is what "the store is still usable" has to mean. A commit made to fail through the fault VFS's journal sync must recover to height zero, stay conserved, and then execute the same block to its recorded root. A commit whose recovery is also denied must refuse to read a head, refuse to hand out a payload, and refuse every later block. And the process is killed at `after_commit_before_publication` and at `after_publication` by a re-executed child. In both cases the parent must find the committed block durable at its recorded root and must be able to continue the chain to the next block's recorded root, so a process that died before it finished saying what it had done left a state some sequence of blocks produced.
ADR 0057 is amended in place, as ADR 0055 was, because the store's contract belongs in one document rather than two. The update records what rolls back and stays usable, what poisons, what recovery does and is allowed to fail at, and why the pair of termination cases is the property requirement 13 asks for rather than an extra. Both items its owed list carried are struck with the date they were delivered, and the section says plainly that the contract came out narrower than the first text implied.
VerificationPR run Local, before pushing: GCC 12 and Clang 14 at Three probes, each made to fail on purpose first and each caught by the check |
1 participant
Closes #219.
ADR 0057 recorded fault-injection coverage of the version-seven write path and
recovery after a failed commit as owed. Requirement 13 asks for scenarios
"through restart and recovery"; the restart half was evidence and the
recovery half was not built. This is both — and settling the second corrected the
first.
The contract came out narrower than the original text implied
Everything before the commit rolls back and is an ordinary refusal. A fault
at
before_transaction,after_transaction_begin,after_persistence, orbefore_commitabandons the transaction, leaves the durable head the one italready was, and leaves the store usable — the same store accepts the same
block once the fault is gone. The original code poisoned on any write failure,
which was safe and wrong: a refusal that wrote nothing is not a reason to stop
answering.
Only the commit can leave a head this process cannot name. There the store
poisons itself and then reads the file again: it closes the connection,
reopens it, runs the same four validation steps an ordinary open runs, and adopts
whatever head the file actually holds — which is either the block's or its
predecessor's, because SQLite's transaction is what decides and nothing between
is reachable. On success the poison is cleared.
Recovery is allowed to fail, and then the store stays poisoned. It is
noexceptand answersfalse. A store that could not read its own file backrefuses to read a head, refuses to hand out a payload, and refuses every later
block. Worse state, honest answer.
Evidence
version-seven-store-recovery, against the recorded roots throughout:block required to reproduce its recorded root — which is what "still usable"
has to mean.
recover to height zero, the recovered head must be conserved, and the same
block must then execute to its recorded root.
after_commit_before_publicationand atafter_publicationby a re-executed child. In both cases the parent must findthe committed block durable at its recorded root and be able to continue
the chain to the next block's recorded root. That pair is the property
requirement 13 names: a fault anywhere in the write path leaves the durable
head at the pre-block root or the post-block root, never anything between.
Probes
Three, each made to fail on purpose first and each caught by the check that names
it: a rolled-back fault that poisons the store fails the "must leave the store
usable" case; a failed commit that never attempts recovery fails the "did not
recover" case; and a recovery that does not clear the poison fails the same case
for the opposite reason. A fourth attempt did not apply cleanly and was re-aimed
rather than counted.
Documentation
ADR 0057 is amended in place, as ADR 0055 was, because the store's contract
belongs in one document rather than two. Both owed items are struck with the date
they were delivered, and the update says plainly that the contract came out
narrower than the first text assumed.
Verification
Local, before pushing: GCC 12 and Clang 14 at
-Wall -Wextra -Wpedantic -Werrorover every changed translation unit;
version-seven-store-recovery,version-seven-owning-store,version-seven-application,version-seven-transport, and version one'sstorage-sqlite-recoveryallpassing — the last because it shares the fault seams this slice wires;
test_registration_test.pyandverify_metadata.pyclean;git diff --check main HEADclean; andgit diff main -- CMakeLists.txt | grep test-vectorsshowing exactly the one intended line. The hosted matrix is the gate for this
exact commit.