MailBackfiller — pages older history below the window (#12)
MailPruner — deletes cached rows past the retention floor (#13)
MailMaintenanceGate (a shared Mutex) serializes exactly one of the three pairs — backfill ↔ prune — and that serialization is now asserted by MailMaintenanceGateTest.
The other two pairs are deliberately ungated: MailSyncer uses its own syncMutex and does not take the maintenance gate, so foreground sync stays responsive. From the MailMaintenanceGate KDoc:
Foreground sync / pull-to-refresh are intentionally NOT gated here (they use MailSyncer's own mutex) so the UI stays responsive.
The gap
sync ↔ backfill and sync ↔ prune have no shared lock. Their safety rests entirely on a disjoint-by-UID argument:
sync only writes/reconciles the recent-UID window — MessageDao.deleteSyncedInWindowNotIn only touches uid >= minWindowUid;
backfill only writes strictly below that window (ImapClient.fetchOlderThan bounded by MessageDao.lowestSyncedUid);
prune only deletes below the retention floor, and MailSyncer.recentWindowFor caps the fetched window to the retention count, so sync and prune can never target the same row.
This is believed correct by inspection, but:
No test exercises sync concurrently with backfill or prune. Unlike backfill↔prune, there is no interleaving test for these two pairs.
The disjointness invariant is subtle and cross-cutting. It depends on the window/floor boundaries staying aligned across recentWindowFor, deleteSyncedInWindowNotIn, the backfiller's lowestSyncedUid boundary, and the pruner's floor queries. A future change to any one of them could silently create an overlap — e.g. a foreground sync deleting a row a backfill is mid-writing, or a fetched window that dips at/below the prune floor.
Proposed work
Add JVM concurrency tests (mirroring MailMaintenanceGateTest) running MailSyncer concurrently with MailBackfiller, and with MailPruner, asserting no lost / duplicated / wrongly-deleted rows under interleaving.
Document the disjoint-window invariant explicitly (code comment or docs) — which functions maintain it and why sync is safe to leave ungated — so future edits don't break it.
(Optional) Add a cheap runtime assertion that the sync window's lowest UID never drops to/below the prune floor.
Priority
Not urgent — the design is correct by inspection and the highest-risk pair (backfill↔prune) is already gated and tested. This is defence-in-depth / regression protection for the two ungated pairs.
## Context
#46 (full-history backfill + device-only retention, #12/#13) introduces three background actors that all mutate cached `messages` rows:
- **`MailSyncer`** — keeps the recent-UID window fresh (foreground sync / pull-to-refresh)
- **`MailBackfiller`** — pages older history *below* the window (#12)
- **`MailPruner`** — deletes cached rows past the retention floor (#13)
`MailMaintenanceGate` (a shared `Mutex`) serializes exactly **one** of the three pairs — **backfill ↔ prune** — and that serialization is now asserted by `MailMaintenanceGateTest`.
The other two pairs are **deliberately ungated**: `MailSyncer` uses its own `syncMutex` and does not take the maintenance gate, so foreground sync stays responsive. From the `MailMaintenanceGate` KDoc:
> Foreground sync / pull-to-refresh are intentionally NOT gated here (they use MailSyncer's own mutex) so the UI stays responsive.
## The gap
**sync ↔ backfill** and **sync ↔ prune** have no shared lock. Their safety rests entirely on a *disjoint-by-UID* argument:
- sync only writes/reconciles the recent-UID window — `MessageDao.deleteSyncedInWindowNotIn` only touches `uid >= minWindowUid`;
- backfill only writes strictly below that window (`ImapClient.fetchOlderThan` bounded by `MessageDao.lowestSyncedUid`);
- prune only deletes below the retention floor, and `MailSyncer.recentWindowFor` caps the fetched window to the retention count, so sync and prune can never target the same row.
This is believed correct **by inspection**, but:
1. **No test exercises sync concurrently with backfill or prune.** Unlike backfill↔prune, there is no interleaving test for these two pairs.
2. **The disjointness invariant is subtle and cross-cutting.** It depends on the window/floor boundaries staying aligned across `recentWindowFor`, `deleteSyncedInWindowNotIn`, the backfiller's `lowestSyncedUid` boundary, and the pruner's floor queries. A future change to any one of them could silently create an overlap — e.g. a foreground sync deleting a row a backfill is mid-writing, or a fetched window that dips at/below the prune floor.
## Proposed work
- [ ] Add JVM concurrency tests (mirroring `MailMaintenanceGateTest`) running `MailSyncer` concurrently with `MailBackfiller`, and with `MailPruner`, asserting no lost / duplicated / wrongly-deleted rows under interleaving.
- [ ] Document the disjoint-window invariant explicitly (code comment or docs) — which functions maintain it and why sync is safe to leave ungated — so future edits don't break it.
- [ ] (Optional) Add a cheap runtime assertion that the sync window's lowest UID never drops to/below the prune floor.
## Priority
Not urgent — the design is correct by inspection and the highest-risk pair (backfill↔prune) is already gated and tested. This is defence-in-depth / regression protection for the two ungated pairs.
_Follow-up from the review of #46._
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
Context
#46 (full-history backfill + device-only retention, #12/#13) introduces three background actors that all mutate cached
messagesrows:MailSyncer— keeps the recent-UID window fresh (foreground sync / pull-to-refresh)MailBackfiller— pages older history below the window (#12)MailPruner— deletes cached rows past the retention floor (#13)MailMaintenanceGate(a sharedMutex) serializes exactly one of the three pairs — backfill ↔ prune — and that serialization is now asserted byMailMaintenanceGateTest.The other two pairs are deliberately ungated:
MailSynceruses its ownsyncMutexand does not take the maintenance gate, so foreground sync stays responsive. From theMailMaintenanceGateKDoc:The gap
sync ↔ backfill and sync ↔ prune have no shared lock. Their safety rests entirely on a disjoint-by-UID argument:
MessageDao.deleteSyncedInWindowNotInonly touchesuid >= minWindowUid;ImapClient.fetchOlderThanbounded byMessageDao.lowestSyncedUid);MailSyncer.recentWindowForcaps the fetched window to the retention count, so sync and prune can never target the same row.This is believed correct by inspection, but:
recentWindowFor,deleteSyncedInWindowNotIn, the backfiller'slowestSyncedUidboundary, and the pruner's floor queries. A future change to any one of them could silently create an overlap — e.g. a foreground sync deleting a row a backfill is mid-writing, or a fetched window that dips at/below the prune floor.Proposed work
MailMaintenanceGateTest) runningMailSyncerconcurrently withMailBackfiller, and withMailPruner, asserting no lost / duplicated / wrongly-deleted rows under interleaving.Priority
Not urgent — the design is correct by inspection and the highest-risk pair (backfill↔prune) is already gated and tested. This is defence-in-depth / regression protection for the two ungated pairs.
Follow-up from the review of #46.