Compose the manifest and GC specs, model termination, check larger sizes#102
Merged
Conversation
All three hooks ended in `|| echo`, which forces exit status zero. For the post-* hooks that is defensible: git has already committed its ref and index updates, so failing helps nobody. They now report loudly on stderr and still exit zero. For pre-push it is not defensible. That hook uploads the content the manifest being pushed refers to, and it is the last point at which a bad push can be stopped. Masking a failed upload publishes a manifest whose hashes have no objects behind them, and every collaborator's checkout 404s. It now aborts the push and points at --no-verify for the case where the user knows better. This contradicts an existing test that asserted `|| echo` for all three hooks, which has been updated. That test encoded the current behaviour as intended, so the change is deliberate rather than incidental: reviewers who disagree should look here first. The risk is that a push is now blocked when `s3lfs track --modified` fails for an unrelated reason, such as absent credentials, on a branch that touches no large files. Hook install and uninstall also wrote through write_text, which truncates before writing: an interrupt part-way through leaves a user's pre-existing hook truncated and executable. Both now write to a sibling temp file and rename. Three of the eight new tests fail on the parent commit. Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after. Failure set identical. Fixes #88 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The @Retry decorator was applied at exactly two call sites. The chunked pipeline -- which handles the largest files, where transient failures are most likely -- had none, so a single blip aborted the whole file. _upload_chunk, _download_chunk, and _discover_chunks_for_file are now retried. _upload_chunk needed restructuring first: it removed its chunk file in a finally that ran on the first failure, so a retry would have found nothing to read and failed with FileNotFoundError. The PUT is now a separate retried call and the cleanup happens once, after all attempts. _download_chunk reopens its target with "wb" each attempt and discovery is a list call, so both were already idempotent. Backoff gains full jitter. A fixed 2/4/8 schedule means every worker that failed at the same moment retries at the same moment, turning a transient blip into a synchronised stampede against the endpoint that just failed. Errors that cannot succeed on a second attempt are no longer retried: permission failures, missing buckets, and 4xx responses other than throttling and request timeout. Previously a 403 took three attempts and two sleeps before surfacing. Measured on a chunk upload whose first PUT fails with a 500: before, one attempt and a hard failure; after, two attempts and success. An existing test asserted the exact fixed delays 2/4/8 and now asserts each delay falls within [0, ceiling]. That test encoded the old schedule as intended behaviour, so the change is deliberate. Test suite: 61 failed / 577 passed before, 61 failed / 589 passed after. Failure set identical; the 61 are the missing-"python"-binary failures. Fixes #89 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Only the drain loops checked _shutdown_requested, so every chunk already submitted to the thread pool ran to completion after Ctrl-C. On a large transfer that makes the interrupt look like a hang. _upload_chunk and _download_chunk now decline to start once shutdown has been requested, raising ShutdownRequested so the drain loops can tell cancelled work from work that genuinely failed and stay quiet about the former rather than printing an error for every queued task. A cancelled upload still removes its temp chunk. The max_concurrency item from the same issue is NOT changed. boto3 spawns max_concurrency threads per transfer while s3lfs runs self.workers transfers at once, so in the worst case they multiply -- but dividing the budget across the pool would leave a single large asset with no multipart parallelism at all, which is the case s3lfs exists for. An existing test documents that intent. I had listed this as a defect in the issue; it is a deliberate trade-off and I was wrong to call it out. A comment now records the reasoning. Test suite: 61 failed / 589 passed before, 61 failed / 593 passed after. Failure set identical. Refs #91 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Three modelling gaps, all raised when the specs were first reviewed. The specs were per-protocol silos, and each assumed the others' properties held: S3lfsGC assumed mutual exclusion, which was false until the lock path was fixed, and S3lfsManifest assumed paths did not matter, which hid the namespace defect. S3lfsCombined puts an uploader, a remover and a collector against one manifest so both safety properties are checked against the same behaviours. It reproduces both single-protocol findings and adds NoOrphanedObjectSurvivesGC, which neither spec could state alone: a lost update orphans an object and the collector then deletes it, so a manifest bug becomes data loss only when GC is also in play. Reachability is keyed on hash and path, tracking the path-aware GC the code now implements. Every configuration previously set CHECK_DEADLOCK FALSE, because a finished behaviour looks like a deadlock to TLC. That also switched off detection of real deadlocks, which mattered: _lock_context is not reentrant, and the question of whether widening a critical section self-deadlocks ended up being answered by instrumenting the lock rather than by the model. Each spec now has an explicit Terminating stutter and CHECK_DEADLOCK is TRUE everywhere; all clean configurations pass with it enabled. The verified-good configurations were also re-run larger -- 3 paths and 3 hashes for the combined model, 3 processes for the manifest model, 6 chunks for the chunk model. Nothing new appears. That is not a proof, but it removes the "only ever checked at the smallest interesting size" caveat. No production code changes; the test suite is untouched at 61 failed / 592 passed. Fixes #92 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
kmatzen
added a commit
that referenced
this pull request
Jul 19, 2026
…zes (#102) * Let pre-push abort the push, and install hooks atomically All three hooks ended in `|| echo`, which forces exit status zero. For the post-* hooks that is defensible: git has already committed its ref and index updates, so failing helps nobody. They now report loudly on stderr and still exit zero. For pre-push it is not defensible. That hook uploads the content the manifest being pushed refers to, and it is the last point at which a bad push can be stopped. Masking a failed upload publishes a manifest whose hashes have no objects behind them, and every collaborator's checkout 404s. It now aborts the push and points at --no-verify for the case where the user knows better. This contradicts an existing test that asserted `|| echo` for all three hooks, which has been updated. That test encoded the current behaviour as intended, so the change is deliberate rather than incidental: reviewers who disagree should look here first. The risk is that a push is now blocked when `s3lfs track --modified` fails for an unrelated reason, such as absent credentials, on a branch that touches no large files. Hook install and uninstall also wrote through write_text, which truncates before writing: an interrupt part-way through leaves a user's pre-existing hook truncated and executable. Both now write to a sibling temp file and rename. Three of the eight new tests fail on the parent commit. Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after. Failure set identical. Fixes #88 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Retry chunked transfers, add jitter, stop retrying hopeless errors The @Retry decorator was applied at exactly two call sites. The chunked pipeline -- which handles the largest files, where transient failures are most likely -- had none, so a single blip aborted the whole file. _upload_chunk, _download_chunk, and _discover_chunks_for_file are now retried. _upload_chunk needed restructuring first: it removed its chunk file in a finally that ran on the first failure, so a retry would have found nothing to read and failed with FileNotFoundError. The PUT is now a separate retried call and the cleanup happens once, after all attempts. _download_chunk reopens its target with "wb" each attempt and discovery is a list call, so both were already idempotent. Backoff gains full jitter. A fixed 2/4/8 schedule means every worker that failed at the same moment retries at the same moment, turning a transient blip into a synchronised stampede against the endpoint that just failed. Errors that cannot succeed on a second attempt are no longer retried: permission failures, missing buckets, and 4xx responses other than throttling and request timeout. Previously a 403 took three attempts and two sleeps before surfacing. Measured on a chunk upload whose first PUT fails with a 500: before, one attempt and a hard failure; after, two attempts and success. An existing test asserted the exact fixed delays 2/4/8 and now asserts each delay falls within [0, ceiling]. That test encoded the old schedule as intended behaviour, so the change is deliberate. Test suite: 61 failed / 577 passed before, 61 failed / 589 passed after. Failure set identical; the 61 are the missing-"python"-binary failures. Fixes #89 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Stop queued transfers after an interrupt Only the drain loops checked _shutdown_requested, so every chunk already submitted to the thread pool ran to completion after Ctrl-C. On a large transfer that makes the interrupt look like a hang. _upload_chunk and _download_chunk now decline to start once shutdown has been requested, raising ShutdownRequested so the drain loops can tell cancelled work from work that genuinely failed and stay quiet about the former rather than printing an error for every queued task. A cancelled upload still removes its temp chunk. The max_concurrency item from the same issue is NOT changed. boto3 spawns max_concurrency threads per transfer while s3lfs runs self.workers transfers at once, so in the worst case they multiply -- but dividing the budget across the pool would leave a single large asset with no multipart parallelism at all, which is the case s3lfs exists for. An existing test documents that intent. I had listed this as a defect in the issue; it is a deliberate trade-off and I was wrong to call it out. A comment now records the reasoning. Test suite: 61 failed / 589 passed before, 61 failed / 593 passed after. Failure set identical. Refs #91 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Compose the manifest and GC specs, model termination, check larger sizes Three modelling gaps, all raised when the specs were first reviewed. The specs were per-protocol silos, and each assumed the others' properties held: S3lfsGC assumed mutual exclusion, which was false until the lock path was fixed, and S3lfsManifest assumed paths did not matter, which hid the namespace defect. S3lfsCombined puts an uploader, a remover and a collector against one manifest so both safety properties are checked against the same behaviours. It reproduces both single-protocol findings and adds NoOrphanedObjectSurvivesGC, which neither spec could state alone: a lost update orphans an object and the collector then deletes it, so a manifest bug becomes data loss only when GC is also in play. Reachability is keyed on hash and path, tracking the path-aware GC the code now implements. Every configuration previously set CHECK_DEADLOCK FALSE, because a finished behaviour looks like a deadlock to TLC. That also switched off detection of real deadlocks, which mattered: _lock_context is not reentrant, and the question of whether widening a critical section self-deadlocks ended up being answered by instrumenting the lock rather than by the model. Each spec now has an explicit Terminating stutter and CHECK_DEADLOCK is TRUE everywhere; all clean configurations pass with it enabled. The verified-good configurations were also re-run larger -- 3 paths and 3 hashes for the combined model, 3 processes for the manifest model, 6 chunks for the chunk model. Nothing new appears. That is not a proof, but it removes the "only ever checked at the smallest interesting size" caveat. No production code changes; the test suite is untouched at 61 failed / 592 passed. Fixes #92 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
kmatzen
added a commit
that referenced
this pull request
Jul 19, 2026
* Make garbage collection reachability path-aware
Objects are stored at assets/{hash}/{manifest_key}.gz, so the storage unit
is hash plus path. Garbage collection judged reachability on the hash
alone, which leaked in both directions: an object stayed reachable as long
as any path shared its content, so removing one of two identical files
never freed the removed path's object, and renaming a file left its old
object reachable forever though nothing could address it.
Reachability is now computed as the set of base keys the manifest implies,
and a key is live if it is one of those or a .chunkN belonging to one. The
in-flight registry moves from hashes to the same base keys, so a claim on
one path no longer protects a different path that happens to share content.
remove_file and remove_subtree deleted only the base .gz key, orphaning
every chunk of a large file. They now delete the chunks too.
This keeps the existing layout rather than moving to content-addressed
storage, so no migration is needed. It does mean deduplication remains
per-path: two identical files at different paths still occupy two objects,
contrary to what the README implies. That claim should be corrected or the
layout changed; both are out of scope here.
An existing test caught a regression in an earlier draft: keys under the
prefix that do not have the shape of an asset were being collected. They
are now explicitly skipped, since s3lfs did not put them there in a form it
recognises and they are not ours to delete.
Five of the seven new tests fail on the parent commit. Three tests from the
in-flight registry change were updated for the key-based API.
Test suite: 61 failed / 561 passed before, 61 failed / 568 passed after.
Failure set identical.
Fixes #87
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Let pre-push abort the push, and install hooks atomically (#98)
All three hooks ended in `|| echo`, which forces exit status zero. For the
post-* hooks that is defensible: git has already committed its ref and
index updates, so failing helps nobody. They now report loudly on stderr
and still exit zero.
For pre-push it is not defensible. That hook uploads the content the
manifest being pushed refers to, and it is the last point at which a bad
push can be stopped. Masking a failed upload publishes a manifest whose
hashes have no objects behind them, and every collaborator's checkout 404s.
It now aborts the push and points at --no-verify for the case where the
user knows better.
This contradicts an existing test that asserted `|| echo` for all three
hooks, which has been updated. That test encoded the current behaviour as
intended, so the change is deliberate rather than incidental: reviewers who
disagree should look here first. The risk is that a push is now blocked
when `s3lfs track --modified` fails for an unrelated reason, such as absent
credentials, on a branch that touches no large files.
Hook install and uninstall also wrote through write_text, which truncates
before writing: an interrupt part-way through leaves a user's pre-existing
hook truncated and executable. Both now write to a sibling temp file and
rename.
Three of the eight new tests fail on the parent commit.
Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after.
Failure set identical.
Fixes #88
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
* Retry chunked transfers, add jitter, stop retrying hopeless errors (#100)
* Let pre-push abort the push, and install hooks atomically
All three hooks ended in `|| echo`, which forces exit status zero. For the
post-* hooks that is defensible: git has already committed its ref and
index updates, so failing helps nobody. They now report loudly on stderr
and still exit zero.
For pre-push it is not defensible. That hook uploads the content the
manifest being pushed refers to, and it is the last point at which a bad
push can be stopped. Masking a failed upload publishes a manifest whose
hashes have no objects behind them, and every collaborator's checkout 404s.
It now aborts the push and points at --no-verify for the case where the
user knows better.
This contradicts an existing test that asserted `|| echo` for all three
hooks, which has been updated. That test encoded the current behaviour as
intended, so the change is deliberate rather than incidental: reviewers who
disagree should look here first. The risk is that a push is now blocked
when `s3lfs track --modified` fails for an unrelated reason, such as absent
credentials, on a branch that touches no large files.
Hook install and uninstall also wrote through write_text, which truncates
before writing: an interrupt part-way through leaves a user's pre-existing
hook truncated and executable. Both now write to a sibling temp file and
rename.
Three of the eight new tests fail on the parent commit.
Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after.
Failure set identical.
Fixes #88
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Retry chunked transfers, add jitter, stop retrying hopeless errors
The @Retry decorator was applied at exactly two call sites. The chunked
pipeline -- which handles the largest files, where transient failures are
most likely -- had none, so a single blip aborted the whole file.
_upload_chunk, _download_chunk, and _discover_chunks_for_file are now
retried. _upload_chunk needed restructuring first: it removed its chunk
file in a finally that ran on the first failure, so a retry would have
found nothing to read and failed with FileNotFoundError. The PUT is now a
separate retried call and the cleanup happens once, after all attempts.
_download_chunk reopens its target with "wb" each attempt and discovery is
a list call, so both were already idempotent.
Backoff gains full jitter. A fixed 2/4/8 schedule means every worker that
failed at the same moment retries at the same moment, turning a transient
blip into a synchronised stampede against the endpoint that just failed.
Errors that cannot succeed on a second attempt are no longer retried:
permission failures, missing buckets, and 4xx responses other than
throttling and request timeout. Previously a 403 took three attempts and
two sleeps before surfacing.
Measured on a chunk upload whose first PUT fails with a 500: before, one
attempt and a hard failure; after, two attempts and success.
An existing test asserted the exact fixed delays 2/4/8 and now asserts each
delay falls within [0, ceiling]. That test encoded the old schedule as
intended behaviour, so the change is deliberate.
Test suite: 61 failed / 577 passed before, 61 failed / 589 passed after.
Failure set identical; the 61 are the missing-"python"-binary failures.
Fixes #89
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
* Stop queued transfers after an interrupt (#101)
* Let pre-push abort the push, and install hooks atomically
All three hooks ended in `|| echo`, which forces exit status zero. For the
post-* hooks that is defensible: git has already committed its ref and
index updates, so failing helps nobody. They now report loudly on stderr
and still exit zero.
For pre-push it is not defensible. That hook uploads the content the
manifest being pushed refers to, and it is the last point at which a bad
push can be stopped. Masking a failed upload publishes a manifest whose
hashes have no objects behind them, and every collaborator's checkout 404s.
It now aborts the push and points at --no-verify for the case where the
user knows better.
This contradicts an existing test that asserted `|| echo` for all three
hooks, which has been updated. That test encoded the current behaviour as
intended, so the change is deliberate rather than incidental: reviewers who
disagree should look here first. The risk is that a push is now blocked
when `s3lfs track --modified` fails for an unrelated reason, such as absent
credentials, on a branch that touches no large files.
Hook install and uninstall also wrote through write_text, which truncates
before writing: an interrupt part-way through leaves a user's pre-existing
hook truncated and executable. Both now write to a sibling temp file and
rename.
Three of the eight new tests fail on the parent commit.
Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after.
Failure set identical.
Fixes #88
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Retry chunked transfers, add jitter, stop retrying hopeless errors
The @Retry decorator was applied at exactly two call sites. The chunked
pipeline -- which handles the largest files, where transient failures are
most likely -- had none, so a single blip aborted the whole file.
_upload_chunk, _download_chunk, and _discover_chunks_for_file are now
retried. _upload_chunk needed restructuring first: it removed its chunk
file in a finally that ran on the first failure, so a retry would have
found nothing to read and failed with FileNotFoundError. The PUT is now a
separate retried call and the cleanup happens once, after all attempts.
_download_chunk reopens its target with "wb" each attempt and discovery is
a list call, so both were already idempotent.
Backoff gains full jitter. A fixed 2/4/8 schedule means every worker that
failed at the same moment retries at the same moment, turning a transient
blip into a synchronised stampede against the endpoint that just failed.
Errors that cannot succeed on a second attempt are no longer retried:
permission failures, missing buckets, and 4xx responses other than
throttling and request timeout. Previously a 403 took three attempts and
two sleeps before surfacing.
Measured on a chunk upload whose first PUT fails with a 500: before, one
attempt and a hard failure; after, two attempts and success.
An existing test asserted the exact fixed delays 2/4/8 and now asserts each
delay falls within [0, ceiling]. That test encoded the old schedule as
intended behaviour, so the change is deliberate.
Test suite: 61 failed / 577 passed before, 61 failed / 589 passed after.
Failure set identical; the 61 are the missing-"python"-binary failures.
Fixes #89
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Stop queued transfers after an interrupt
Only the drain loops checked _shutdown_requested, so every chunk already
submitted to the thread pool ran to completion after Ctrl-C. On a large
transfer that makes the interrupt look like a hang.
_upload_chunk and _download_chunk now decline to start once shutdown has
been requested, raising ShutdownRequested so the drain loops can tell
cancelled work from work that genuinely failed and stay quiet about the
former rather than printing an error for every queued task. A cancelled
upload still removes its temp chunk.
The max_concurrency item from the same issue is NOT changed. boto3 spawns
max_concurrency threads per transfer while s3lfs runs self.workers
transfers at once, so in the worst case they multiply -- but dividing the
budget across the pool would leave a single large asset with no multipart
parallelism at all, which is the case s3lfs exists for. An existing test
documents that intent. I had listed this as a defect in the issue; it is a
deliberate trade-off and I was wrong to call it out. A comment now records
the reasoning.
Test suite: 61 failed / 589 passed before, 61 failed / 593 passed after.
Failure set identical.
Refs #91
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
* Compose the manifest and GC specs, model termination, check larger sizes (#102)
* Let pre-push abort the push, and install hooks atomically
All three hooks ended in `|| echo`, which forces exit status zero. For the
post-* hooks that is defensible: git has already committed its ref and
index updates, so failing helps nobody. They now report loudly on stderr
and still exit zero.
For pre-push it is not defensible. That hook uploads the content the
manifest being pushed refers to, and it is the last point at which a bad
push can be stopped. Masking a failed upload publishes a manifest whose
hashes have no objects behind them, and every collaborator's checkout 404s.
It now aborts the push and points at --no-verify for the case where the
user knows better.
This contradicts an existing test that asserted `|| echo` for all three
hooks, which has been updated. That test encoded the current behaviour as
intended, so the change is deliberate rather than incidental: reviewers who
disagree should look here first. The risk is that a push is now blocked
when `s3lfs track --modified` fails for an unrelated reason, such as absent
credentials, on a branch that touches no large files.
Hook install and uninstall also wrote through write_text, which truncates
before writing: an interrupt part-way through leaves a user's pre-existing
hook truncated and executable. Both now write to a sibling temp file and
rename.
Three of the eight new tests fail on the parent commit.
Test suite: 61 failed / 568 passed before, 61 failed / 577 passed after.
Failure set identical.
Fixes #88
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Retry chunked transfers, add jitter, stop retrying hopeless errors
The @Retry decorator was applied at exactly two call sites. The chunked
pipeline -- which handles the largest files, where transient failures are
most likely -- had none, so a single blip aborted the whole file.
_upload_chunk, _download_chunk, and _discover_chunks_for_file are now
retried. _upload_chunk needed restructuring first: it removed its chunk
file in a finally that ran on the first failure, so a retry would have
found nothing to read and failed with FileNotFoundError. The PUT is now a
separate retried call and the cleanup happens once, after all attempts.
_download_chunk reopens its target with "wb" each attempt and discovery is
a list call, so both were already idempotent.
Backoff gains full jitter. A fixed 2/4/8 schedule means every worker that
failed at the same moment retries at the same moment, turning a transient
blip into a synchronised stampede against the endpoint that just failed.
Errors that cannot succeed on a second attempt are no longer retried:
permission failures, missing buckets, and 4xx responses other than
throttling and request timeout. Previously a 403 took three attempts and
two sleeps before surfacing.
Measured on a chunk upload whose first PUT fails with a 500: before, one
attempt and a hard failure; after, two attempts and success.
An existing test asserted the exact fixed delays 2/4/8 and now asserts each
delay falls within [0, ceiling]. That test encoded the old schedule as
intended behaviour, so the change is deliberate.
Test suite: 61 failed / 577 passed before, 61 failed / 589 passed after.
Failure set identical; the 61 are the missing-"python"-binary failures.
Fixes #89
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Stop queued transfers after an interrupt
Only the drain loops checked _shutdown_requested, so every chunk already
submitted to the thread pool ran to completion after Ctrl-C. On a large
transfer that makes the interrupt look like a hang.
_upload_chunk and _download_chunk now decline to start once shutdown has
been requested, raising ShutdownRequested so the drain loops can tell
cancelled work from work that genuinely failed and stay quiet about the
former rather than printing an error for every queued task. A cancelled
upload still removes its temp chunk.
The max_concurrency item from the same issue is NOT changed. boto3 spawns
max_concurrency threads per transfer while s3lfs runs self.workers
transfers at once, so in the worst case they multiply -- but dividing the
budget across the pool would leave a single large asset with no multipart
parallelism at all, which is the case s3lfs exists for. An existing test
documents that intent. I had listed this as a defect in the issue; it is a
deliberate trade-off and I was wrong to call it out. A comment now records
the reasoning.
Test suite: 61 failed / 589 passed before, 61 failed / 593 passed after.
Failure set identical.
Refs #91
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* Compose the manifest and GC specs, model termination, check larger sizes
Three modelling gaps, all raised when the specs were first reviewed.
The specs were per-protocol silos, and each assumed the others' properties
held: S3lfsGC assumed mutual exclusion, which was false until the lock path
was fixed, and S3lfsManifest assumed paths did not matter, which hid the
namespace defect. S3lfsCombined puts an uploader, a remover and a collector
against one manifest so both safety properties are checked against the same
behaviours. It reproduces both single-protocol findings and adds
NoOrphanedObjectSurvivesGC, which neither spec could state alone: a lost
update orphans an object and the collector then deletes it, so a manifest
bug becomes data loss only when GC is also in play. Reachability is keyed
on hash and path, tracking the path-aware GC the code now implements.
Every configuration previously set CHECK_DEADLOCK FALSE, because a finished
behaviour looks like a deadlock to TLC. That also switched off detection of
real deadlocks, which mattered: _lock_context is not reentrant, and the
question of whether widening a critical section self-deadlocks ended up
being answered by instrumenting the lock rather than by the model. Each
spec now has an explicit Terminating stutter and CHECK_DEADLOCK is TRUE
everywhere; all clean configurations pass with it enabled.
The verified-good configurations were also re-run larger -- 3 paths and 3
hashes for the combined model, 3 processes for the manifest model, 6 chunks
for the chunk model. Nothing new appears. That is not a proof, but it
removes the "only ever checked at the smallest interesting size" caveat.
No production code changes; the test suite is untouched at 61 failed / 592
passed.
Fixes #92
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #92. Stacked on #101. No production code changes.
Three modelling gaps, all raised when the specs were first reviewed.
1. The specs were silos
Each assumed the others' properties held —
S3lfsGCassumed mutual exclusion (false until the lock path was fixed),S3lfsManifestassumed paths didn't matter (which hid the namespace defect). Cross-cutting defects live in exactly those seams.S3lfsCombinedputs an uploader, a remover and a collector against one manifest, so both safety properties are checked against the same behaviours:RELOADINFLIGHTGC_REVALIDATEBrokenNoLostUpdateviolatedReloadOnlyNoDanglingReferenceviolatedRevalOnlyNoDanglingReferencestill violatedFixedRevalOnlyconfirms in the composed model whatS3lfsGCfound in isolation: re-validating before deleting does not close the race.It also adds
NoOrphanedObjectSurvivesGC, which neither single-protocol spec could state — it needs the remover and the collector in one behaviour. A lost update orphans an object and the collector then deletes it, so a manifest bug becomes data loss only when GC is also in play.2.
CHECK_DEADLOCKwas off, and that hid something realEvery config set
CHECK_DEADLOCK FALSE, because a finished behaviour looks like a deadlock to TLC. Expedient, and wrong: it also switched off detection of real deadlocks.That mattered concretely.
_lock_contextis not reentrant, so widening a critical section risks a self-deadlock — and when #84 did widen one, the question had to be answered by instrumenting the lock with a depth counter, because the model had nothing to say. The check I'd disabled was exactly the one I needed.Each spec now has an explicit
Terminatingstutter, so termination is a legitimate self-loop, andCHECK_DEADLOCK TRUEis set everywhere. All clean configurations pass with it enabled.3. Only ever checked at the smallest interesting size
The counterexamples all appear at 2 processes / 2 paths / 3 chunks, but a clean result at that size establishes little. Re-run larger:
S3lfsCombined_FixedLargeS3lfsManifest_Reload_Lock_LargeS3lfsChunks_CommitAndVerifyLargeNothing new appears. Still not a proof — TLC checks the model it is given — but the caveat is narrower now.
Still not modelled
S3lfsCombinedhas one of each role, so it cannot speak to two uploads racing on the same path.🤖 Generated with Claude Code
https://claude.ai/code/session_019UrDtdFKGwQZp8oYGwL2rj