|
| 1 | +# File replacement and restart model |
| 2 | + |
| 3 | +`scripts/check-file-replacement-restart.ts` is an independent bounded submodel |
| 4 | +under `pnpm lifecycle:model-check`. It preserves the completion-readiness model's |
| 5 | +separate scope. It checks three files, one initial publication per file, one later |
| 6 | +replacement of any one file, and one process crash at every publication or |
| 7 | +replacement boundary. Exploration runs to a fixed point with a 10,000-state cap. |
| 8 | + |
| 9 | +## Contract and production mapping |
| 10 | + |
| 11 | +| Model action | Production boundary | |
| 12 | +| ---------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | |
| 13 | +| `publish-ui`, `publish-api`, `publish-history` | Successful writes of `ui_messages.json`, `api_conversation_history.json`, and `history_item.json` | |
| 14 | +| `acknowledge-all-three-files` | Explicit readiness conjunction in the restart E2E: `hasTaskUiMessageText`, `hasTaskApiConversationHistorySequence`, and `getTaskHistoryItem`. For a newly created task, `TaskHistoryStore.upsertCore` publishes its cache entry after `writeTaskFile` succeeds. This is a test readiness boundary, not a new public runtime event. | |
| 15 | +| `stage-replacement-*` | `safeWriteJson` writes and flushes a `.new_*.tmp` file under the advisory lock | |
| 16 | +| `atomic-commit` | Single temp-to-canonical rename | |
| 17 | +| `eperm-backup-rename`, `fallback-commit` | Windows-compatible EPERM fallback: canonical-to-backup, then temp-to-canonical | |
| 18 | +| `process-crash` | Process exits without rollback, cleanup, or lock release | |
| 19 | +| `lock-becomes-stale` | `proper-lockfile` staleness check using the shared 31-second window | |
| 20 | +| `fresh-host-startup`, `locked-reader-recovery` | `TaskHistoryStore.reconcile` recovers a missing history record before stat/read; `readFileWithMissingRetry` invokes the same recovery after a second ENOENT for UI/API reads | |
| 21 | +| `recovery-io-failure` | Recovery scan, access, stat, or restore fails; rejection preserves committed backups for a later retry | |
| 22 | +| `explicit-delete-under-lock` | `deleteJsonFile` removes matching replacements/backups before the canonical file, serialized with writers and recovery; store deletion remains best effort | |
| 23 | + |
| 24 | +The UI marker can become visible while history publication is still pending. |
| 25 | +`Task.saveClineMessages` persists UI messages before updating metadata, and logs |
| 26 | +metadata failures independently. Neither `TaskCompleted` nor UI-marker visibility |
| 27 | +promises that all three files exist. The model explicitly reaches that partial |
| 28 | +publication state and permits interruption there. It requires restart discovery |
| 29 | +only after the readiness conjunction, not after an unfinished first write. |
| 30 | + |
| 31 | +After acknowledgment, the latest committed version of each required file must |
| 32 | +remain in either the canonical file or its backup until explicit deletion. |
| 33 | +Completed fresh reads must return those committed versions and find the history |
| 34 | +record without a new write. A failed recovery must preserve every file version. |
| 35 | +Successful explicit deletion must leave no recoverable version to resurrect. |
| 36 | +The model requires reachable atomic and fallback successes, restart recovery, |
| 37 | +recovery after failure, partial publication, and reads after deletion. |
| 38 | + |
| 39 | +The checker first runs the old two-rename protocol without reader recovery and |
| 40 | +requires a #2130 counterexample. It then exhaustively checks the fixed protocol. |
| 41 | +This is an abstract protocol check, not execution of the production writer. |
| 42 | + |
| 43 | +## Refinement evidence |
| 44 | + |
| 45 | +`src/utils/__tests__/safeWriteJson.interruption.test.ts` runs the real bundled |
| 46 | +writer in a child process, terminates it with SIGKILL, and exercises both commit |
| 47 | +paths before and after the replacement rename for all three filenames. Initial |
| 48 | +publication uses the production writer. UI/API tests call production readers; |
| 49 | +history-record cases initialize a fresh `TaskHistoryStore` before any recovery |
| 50 | +write. One case leaves the crash lock's timestamp unchanged, proving the fresh |
| 51 | +store can wait for staleness instead of requiring the test to age the lock. |
| 52 | + |
| 53 | +`safeWriteJson.test.ts` injects directory scan, access, backup stat, and restore |
| 54 | +failures, checking backup preservation and retry. The store deletion tests cover |
| 55 | +single and batch deletion, leftover cleanup, unrelated-file preservation, and |
| 56 | +cleanup failure retaining the canonical copy. The existing two-extension-host |
| 57 | +restart E2E remains the production activation/rehydration boundary check. |
| 58 | + |
| 59 | +## Assumptions and limits |
| 60 | + |
| 61 | +This is process-crash safety on filesystems with atomic same-directory rename, |
| 62 | +not power-loss safety. Parent directories are not fsynced. Locks are advisory; |
| 63 | +all writers, recoverers, and history-file deleters must use the shared protocol. |
| 64 | +Live holders refresh their locks and must not be mistaken for crashed holders; |
| 65 | +filesystem clock behavior and lock compromise are outside the model. Recovery |
| 66 | +waits up to 35 lock retries at one-second intervals, then reports a lock failure. |
| 67 | +An indefinitely active writer or persistent filesystem fault can still prevent |
| 68 | +recovery; no liveness guarantee is claimed under such faults. |
| 69 | + |
| 70 | +Recovery is abstracted as a locked restore and cleanup; repeated crashes during |
| 71 | +recovery, multiple orphaned versions, external file removal, arbitrary overlapping |
| 72 | +writers, and deletion interrupted between individual unlinks are not exhaustively |
| 73 | +modeled. Focused tests cover newest-backup selection and filesystem failures. |
| 74 | +Deletion does not prohibit an explicit later creation of a task at the same path |
| 75 | +or a stale writer that deliberately publishes new data after deletion. The |
| 76 | +no-resurrection property concerns recovery from leftovers after successful |
| 77 | +deletion. Lifecycle status/delegation reducers and completion-event semantics |
| 78 | +are unchanged. |
0 commit comments