cortexkit-lease: shared-mode leases (acquire_shared)#1
Merged
Conversation
Shared holders coexist with each other and block the exclusive writer (and vice versa) — reader-side protection for shared resources like the cross-module model cache: a reader takes a shared lease on a blob digest while validating/mmap-ing so GC (exclusive) can never delete under it. Shared handles do not bump the fence epoch (they are not writers); they report the last persisted writer epoch for observability. Semantics proven in tests: shared+shared coexist, shared blocks exclusive until the LAST shared holder drops, exclusive blocks shared, epoch neutrality, and a cross-process shared-vs-exclusive check (unix: python-fcntl child; Windows LockFileEx semantics are exercised by the same-process tests since its locks are per-handle). try_lock_shared is called via the fs2 trait fully-qualified: std 1.89+ added an inherent File::try_lock_shared that would shadow it.
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
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.
What
Adds
LeaseStore::acquire_shared: shared holders coexist with each other and block the exclusive writer (and vice versa). File impl via fs2'stry_lock_shared— flock(LOCK_SH) on unix, LockFileEx without LOCKFILE_EXCLUSIVE_LOCK on Windows.Why
First consumer: Synapse's cross-module model cache (~/.local/share/cortexkit/models/). Readers take a shared lease on a blob digest while validating/mmap-ing; GC takes exclusive + two-phase tombstones, so it can never delete a file under a live reader while concurrent readers never serialize each other. (Design: synapse docs/design-synapse-module.md, model-cache section; requested shape per SUBC review pm_31c3ffbf — lease-crate-only, option (a).)
Semantics pinned by tests
Notes
try_lock_sharedis called fully-qualified through the fs2 trait: std 1.89+ ships an inherentFile::try_lock_sharedreturningTryLockErrorwhich otherwise shadows the fs2 method (build error caught in this PR's development.No changes outside the lease crate. cortexkit-store untouched and green.
EOF
)
Need help on this PR? Tag
/codesmithwith what you need. Autofix is disabled.Summary by cubic
Add shared-mode leases to
cortexkit-leaseviaLeaseStore::acquire_shared, letting multiple readers coexist while blocking an exclusive writer (and vice versa). Prevents model cache GC from deleting files under live readers without forcing readers to serialize.acquire_shared: shared+shared coexist; exclusive blocks shared; exclusive waits until the last shared drops.LeaseHandle::epoch()reports the last persisted writer epoch.fs2try_lock_shared(flock LOCK_SH on Unix, shared LockFileEx on Windows); called fully qualified to avoid stdFile::try_lock_sharedshadowing.Written for commit dda5aee. Summary will update on new commits.