This tracks the checklocks work described in the discussion on #14345. The work is separated by review burden:
- Add contracts for accesses that are already correct, in owner-cohesive batches without a checker dependency.
- Harden the checker, investigating newly exposed misuse rather than adding compatibility exceptions.
- Keep runtime fixes and their regression coverage focused enough to review carefully.
The current review set is 23 proposals: five independent contract batches, one checker PR and seventeen focused runtime/test fixes. Six dependent follow-ups remain unopened.
Proof-only refactors are identified separately from behavioral fixes. A comment or narrow exception remains only where the actual ownership or lifetime relationship cannot be represented.
Already-correct contracts
| Scope |
Pull request |
| Shared infrastructure and metric/verifier contracts |
#14350 |
| Memory-manager and accounting contracts |
#14351 |
| Kernel, auth and IPC contracts |
#14352 |
| Filesystem contracts |
#14353 — conflicts resolved |
| Network contracts |
#14354 — approved; conflicts resolved |
Checker hardening
Implicit-return/recovery handling with unresolved mutable-owner identity remains outside this proposal; the known diagnostics are not hidden by new filters.
Runtime and test fixes
| Scope |
Pull request |
| ARM64 race-build compare-and-swap |
#14355 |
| Compression and shared-utility ownership |
#14356 |
| Clock calibration and watchdog behavior |
#14357 |
| Runtime control and port-forward ownership |
#14358 |
| Metric shutdown, savings and state-load retries |
#14359 |
| Async restore and checkpoint registration |
#14360 |
| LisaFS node and socket lifetimes |
#14361 |
| Virtual host-file ownership |
#14362 |
| Mountinfo option snapshots |
#14363 — conflicts resolved |
| IPC removal errors |
#14364 |
| Shared key permissions |
#14365 |
| TCP atomic state and probe snapshots |
#14366 — merged |
| UDP receive-state synchronization |
#14367 — merged |
| Fragment reassembly unlock |
#14368 — approved; internal safe review pending |
| Network sysctl synchronization |
#14369 — merged |
| Plugin readiness cache |
#14370 |
| Gonet, FIFO and TUN ownership |
#14371 — approved; internal checks passed |
Dependent follow-ups
These six branches are prepared but remain unopened; they are not duplicate cumulative PRs to review now. After the real prerequisites land, their comparisons need to be rebased, reconciled and revalidated.
| Scope |
Prerequisites |
| FD-table, TPU and PIDFD ownership |
#14237 and #14352 |
| TMPFS/VFS ownership adaptations |
#14237 |
| Native futex atomic pointers |
#14237 and #14352 |
| Unix transport ownership and unsupported-stream handling |
#14237 |
| Allocator atomic-pointer contracts |
#14237 and #14360 |
| Kernel runtime and TaskSet contracts |
#14237 and #14352 |
Earlier proposals
| Original |
Replacements and disposition |
| #14289 |
Closed; #14350, #14355, #14356 |
| #14313 |
Closed; #14350, #14359, #14237 |
| #14339 |
Closed; #14351, #14357 |
| #14342 |
Closed; #14350, #14358 |
| #14338 |
Partial: #14354, #14366–#14371; Unix and FD-table/TPU follow-ups remain |
| #14343 |
Partial: #14353, #14361–#14363; TMPFS/VFS and FD-table follow-ups remain |
| #14345 |
Partial: #14352, #14364, #14365; kernel-runtime/TaskSet and futex follow-ups remain |
| #14348 |
Partial: #14351, #14360, #14237; allocator contracts remain |
The four partially replaced originals remain open to retain their deferred scope, not as additional review units. Please use the linked replacements for work ready to review now. #14240 has merged and is excluded from this reorganization.
Validation and automation notes
Existing validation limitations remain explicit on the affected changes: the independent infrastructure branch reproduces the stock NaN-bucketer failure (fixed in the metrics runtime branch); standalone TCP full-race results have unresolved failures; namespace/capability-dependent runtime coverage is limited by the local environment. These are not reasons to suppress diagnostics or claim unexecuted coverage.
The initial GitHub status rollup is not a substitute for the recorded build and runtime evidence. The reviewer-assignment jobs for #14361 and #14371 failed with HTTP 422 because one or more bot-selected reviewers were not repository collaborators. Scoped r? comments are posted on every current proposal; no assignment bypass or retry was attempted.
Assisted-by: Codex
This tracks the checklocks work described in the discussion on #14345. The work is separated by review burden:
The current review set is 23 proposals: five independent contract batches, one checker PR and seventeen focused runtime/test fixes. Six dependent follow-ups remain unopened.
Proof-only refactors are identified separately from behavioral fixes. A comment or narrow exception remains only where the actual ownership or lifetime relationship cannot be represented.
Already-correct contracts
Checker hardening
Implicit-return/recovery handling with unresolved mutable-owner identity remains outside this proposal; the known diagnostics are not hidden by new filters.
Runtime and test fixes
Dependent follow-ups
These six branches are prepared but remain unopened; they are not duplicate cumulative PRs to review now. After the real prerequisites land, their comparisons need to be rebased, reconciled and revalidated.
Earlier proposals
The four partially replaced originals remain open to retain their deferred scope, not as additional review units. Please use the linked replacements for work ready to review now. #14240 has merged and is excluded from this reorganization.
Validation and automation notes
Existing validation limitations remain explicit on the affected changes: the independent infrastructure branch reproduces the stock NaN-bucketer failure (fixed in the metrics runtime branch); standalone TCP full-race results have unresolved failures; namespace/capability-dependent runtime coverage is limited by the local environment. These are not reasons to suppress diagnostics or claim unexecuted coverage.
The initial GitHub status rollup is not a substitute for the recorded build and runtime evidence. The reviewer-assignment jobs for #14361 and #14371 failed with HTTP 422 because one or more bot-selected reviewers were not repository collaborators. Scoped
r?comments are posted on every current proposal; no assignment bypass or retry was attempted.Assisted-by: Codex