WriterLifecycle.dfy specifies the supported serialized lifecycle after a writer has acquired exclusive ownership. Its fault model covers returned command failures and in-process disposal; process termination discards these in-memory objects and belongs to the separate recovery models. It is a verification-only state machine: no additional runtime or generated library code is introduced. The image and auxiliary-state snapshots are exact logical values. The model’s committed image is the last selected committed value; its name does not prove filesystem durability or describe intermediate physical statement spills.
Each writer has an immutable owner token and a map of scope tokens that are never reused for that writer. Tokens denote object identity, not transaction depth: a released child’s token cannot identify a later child at the same depth. Each active scope records its exact entry image and auxiliary writer-state snapshot. Public mutations are serialized by TransactionLifecycle.RunSerializedAsync; callback re-entry is refused in production. The model begins at that serialized boundary and does not verify semaphore fairness, cross-process exclusion or all asynchronous interleavings.
| State or operation | Specified behavior and production mapping |
|---|---|
| Open writer | Holds its ownership lease. Begin allocates a fresh scope at depths one through seven. Production BeginTransactionCoreAsync supplies object identity and attaches one shared PagerTransaction. |
| Database mutation | A private statement transaction supplies a root when no explicit scope exists; otherwise RunInSavepointAsync begins a statement savepoint inside the innermost explicit scope. BeginStatement admits writes only at explicit depths one through five. A successful statement keeps its new logical image and auxiliary state; a failed/cancelled statement restores its exact statement-entry snapshot without terminating its explicit scope. Resource/budget errors are outcomes of that statement contract rather than independently verified allocation bounds. |
| Child commit | Finish(..., Commit, Committed) releases the innermost savepoint, keeps its current logical image and marks that token committed. It does not select a new outer committed image or invalidate the generation. A later parent rollback still restores the parent’s entry snapshot. The child remains publicly committed even when its changes are subsequently undone by a parent. |
| Child rollback or disposal | Only the innermost active token may resolve. EndNestedTransaction restores its saved image and auxiliary state, invalidates derived state and exposes its parent. Disposing an active ancestor refuses while a child remains. Commit/rollback of an ended token refuses; disposal of that ended token is a no-op. |
| Outermost completion | Successful commit selects the complete logical view. A cancelled commit or a commit whose undo succeeds resolves as rolled back and restores the exact entry image/state. A failed preparation, failed restoration or uncertain commit decision resolves as Failed, empties the active stack and faults the writer. JetTransaction.IsCommitFailed is internal; its public committed/rolled-back flags both remain false. The I/O protocol determines which of these returned outcomes is valid. |
| Cancellation before entering a scope/rollback | Production leaves the current stack unchanged. Cancelled child commit instead rolls that child back. The model represents the former as refusal/no transition and the latter as a successful rolled-back resolution. |
| Faulted writer | Rejects new scopes and mutation. Reads can still return/retain a frame of the current generation; no exact-image claim follows while the physical image is uncertain. Disposal releases resources while preserving uncertain recovery evidence; it does not infer a committed or rolled-back image. The model permits explicit invalidation, which only discards derived state. |
| Writer disposal | StartWriterDispose prevents new mutations, then each DisposeTop rolls back the current innermost scope. A failed outer physical restoration is represented by AbandonFailedDisposal, which marks that single outer token failed and forces detachment. DisposeActiveTransactionAsync always clears the active journal/stack; LockFileCoordinator.DisposeAfterAsync drains teardown steps and releases handles even when an earlier step throws. Repeating completed writer disposal is a no-op. |
| Lease cleanup and release | Exact-generation native and receipt deletion require held authority and an empty scope stack. Normal cleanup deletes native evidence before its receipt and retains the coordinated lease until release. A failed deletion may instead retain the names and still release the handles; retained evidence requires later validated recovery. The caller receives disposal failures after all teardown steps are attempted. RecoverableWriterLock.Dispose records the attempt before deletion, so stale repeated disposal cannot delete successor evidence. Recovery leases likewise close their handles idempotently; RecoveryLease.Cleanup is a single authorized cleanup invocation, not a reusable capability after release. |
ValidInitial constructs an admitted open state from GenerationOwnership.Valid, held exact ownership and an owner object that has not started disposal. StepPreserves and TracePreserves preserve legal states, immutable writer identity, scope membership, non-reused terminal token identities and monotone generations for arbitrary finite admitted traces. ResolutionRequiresInnermostToken and DepthLimitsRefuseWithoutResolution state operation refusal. SurvivingScopeSnapshotIsImmutable, ReleasedChildDoesNotPublish, RollbackRestoresExactScopeSnapshot and FailedStatementPreservesScopeAndSnapshot establish the nested and statement contracts. The complete outer/statement effect is an explicit premise; the model does not replace the journal or replacement persistence proofs.
Pager.InvalidateAll empties retained frames and increments InvalidationGeneration. Each pending cache load/write retains a frame only if its captured generation still equals the current one. InvalidatedReadCannotRetain proves that a ticket from the old generation cannot enter the retained set after invalidation. An already-read page can still be returned to its caller; this theorem concerns retention, not linearizable reads or pinned buffer reuse. Auxiliary writer caches restore or invalidate through RestoreWriterState and DiscardCachesAfterFailedReplay; their implementation is an exact-snapshot/unknown-state contract in this model.
The separate page-frame ownership model specifies bounded producer/cache and reader references, immutable bytes and final pool return. Its retained/unretained traces cover the ownership ledger; the actual cache lookup, CAS, array identity, disposal and containing writer/controller composition still need manual correspondence and focused tests. It does not expand the serialized lifecycle theorem into a concurrent C# proof.
The actual counter is a checked signed long, not an unbounded integer. Model generations are bounded by 9,223,372,036,854,775,807, and every admitted increment requires remaining space. CompleteWriterDisposal additionally requires enough space for each remaining scope’s rollback. The schedule counts abstract lifecycle actions, not production invalidation calls or syscalls; production teardown can invalidate more than once. This is a successful-transition condition: the proof does not assert that the machine counter can advance forever or that counter overflow completes teardown normally.
TerminalDisposeIsIdempotent covers already-ended transaction tokens and completed writers. FaultedResolutionEndsScope prevents a failed commit/rollback from masquerading as successful rollback. LeaseDeletionRetainsExactAuthority connects cleanup to the existing generation model. CompleteWriterDisposal constructs a finite successful rollback, native deletion, receipt deletion and handle-release schedule with a strictly decreasing scope/name/phase rank. Early release with retained names models failed cleanup separately; infinite failures carry no availability promise. Existing GenerationOwnership.StaleOwnerCannotDelete and RepeatedDisposePreservesSuccessor supply the stale-object namespace guarantee under exclusive cooperating ownership.
The following focused tests bind observable production behavior to the named specification boundaries. They are manual conformance traces, not an automatic refinement proof of C#.
| Boundary | Focused evidence |
|---|---|
| Released token identity, failure inside a later child, generation changes, restored root and journal detachment | WriterLifecycleConformanceTests.ReleasedChild_StatementFailure_AndRollback_PreserveScopeIdentity |
| Seven unresolved scopes, an earlier committed child, complete writer unwind and repeated disposal | WriterLifecycleConformanceTests.WriterDisposal_UnwindsMaximumDepth_AndRepeatedDisposalIsInert |
| Reverse-order resolution, depth/write limits, child cancellation and exact auxiliary-state rollback | NestedTransactionTests, especially SevenLevels_RefusedEighthBegin_PreservesJournalAndScopes, ChildCancellation_PreservesParentAndRestoresChildState and ChildRollback_RestoresWriterState_AndParentCanCommit |
| Faulted current-generation reads, mutation refusal, failed-token flags and disposal without writes | WriterLifecycleConformanceTests.FailedUndo_AllowsCurrentGenerationRead_ButDisposalDoesNotWrite |
| Failed replay with successful restoration; failed/uncertain restoration and refusal | JetTransactionTests.Commit_WhenReplayWriteFails_RestoresFileAndRollsBack, Commit_WhenDurableFlushFails_RestoresFileAndRollsBack; StatementAtomicityTests, the shared StatementAtomicityTestBase sweep through StatementAtomicityJet3Tests/StatementAtomicityJet4Tests/StatementAtomicityAceTests, CommitFaultSweepTests and PagerRecoveryFailureTests retain their separate returned-I/O evidence |
| A delayed old load cannot refill the cache; failed writes discard frames | PagerFrameCacheTests.DelayedLoad_AfterInvalidation_IsNotRetained, FailedWrite_DiscardsFrames |
| Ended lease object cannot remove a new generation | RecoverableWriterLockTests.Dispose_CompletedOwner_PreservesSuccessor and the exact-receipt/refusal controls in that class |
Snapshot capture/restore, logical page effects and successful in-memory bookkeeping are premises; catastrophic allocation failures and exceptions during otherwise memory-only nested resolution are not assigned invented terminal flags. Failed disposal’s modeled forced detachment concerns the single outer physical restoration boundary, where production calls MarkCommitFailed. Fresh scope/owner identity, validated receipt/path/generation authority, lease exclusion, file-effect outcomes and the absence of generation overflow remain explicit contracts. Caller-supplied streams require their caller’s own exclusive ownership/reopen protocol; no persistent stream recovery is inferred from the abstract lease.
The separate cooperating process model specifies cross-process acquisition/recovery/cleanup interleavings under an atomic canonical-coordination contract. Refining actual coordination acquisition, OS-specific cooperation, deadlock prevention and pin/lease/copy-on-write reuse remain V10 obligations. Namespace/device durability, raw parser/hash correctness, full effectful C# control flow and Access interoperability remain separate evidence levels.