Concurrency: reported-*.json lost ack — lock-free read-merge-write double-counts sessions

[jeff-r2026]

Summary

The reported-*.json snapshots (interventions / prompt-tokens / daily-sessions) are updated with a lock-free read-merge-write: read the snapshot, spread-merge this session's ack, write the whole object back with a non-atomic writeJson. When two auto-reports from two agent sessions interleave read-read-write-write, the first writer's ack is clobbered by the second (which merged onto a stale read). The dropped session then double-counts on the next report cycle, because it is no longer recorded as already-reported.

Same root cause as the usage.jsonl lost-update defect (sibling issue): a lock-free RMW of a globally shared ~/.teamai file.

Where

src/team-push.ts @ 48b3dcb

• writeReportedInterventions() — line 149, writeJson(getReportedInterventionsPath(), data) (line 151)
• interventions ack merge — line 587, writeReportedInterventions({ ...existingIv, ...nextReported })
• prompt-tokens twin — writeFile(p, JSON.stringify(data)) (line 230)
• daily-sessions twin — writeJson(getReportedDailySessionsPath(), data) (line 296)

All three files live under ~/.teamai/dashboard/ — global, one file each, scope-independent. writeJson is a plain (non-atomic) writeFile. None of these take a lock.

Why it is reachable in practice

• Within a single pull(), the auto-report loop is serial (for … await), so it does not self-collide.
• The collision is cross-process: two SessionStart auto-pulls from two agent sessions on one machine, each carrying an ack for a different session id.
• The per-scope .sync-lock does not help — it guards the team clone, not ~/.teamai/dashboard/. Auto-report can even outlive the lock: it runs under a 5s withTimeout, so pull() may return and release the lock while auto-report keeps running.
• The read→write gap spans a git push, which is long, widening the window for a read-read-write-write interleaving.

Counterexample (TLA+ / TLC 2.19)

Modelled the snapshot as a set of acknowledged session ids. Two writers P and Q each add their own id; the correct final state is {p, q}. BothAcked states that once both writers finish, both acks are present. TLC finds a violation:

State 1: Init       — snap = {}
State 2: P.read     — writer P reads the snapshot           (pView = {})
State 3: Q.read     — writer Q reads the same snapshot      (qView = {})
State 4: P.write    — P writes its view + its own ack "p"   (snap = {p})
State 5: Q.write    — Q writes its STALE view + "q"         (snap = {q})
                      -> "p" is gone. BothAcked VIOLATED.

Consequence: session p's ack is lost, so on the next report cycle its interventions/prompts/tokens are counted again and pushed to the team — a double-report.

Suggested fix (smallest correct)

Same remedy as the usage.jsonl issue: serialize each snapshot's read-merge-write under a per-file lock (reuse acquireLock/releaseLock from src/update.ts), and use writeFileAtomic (or a writeJsonAtomic) for the write so a crash mid-write cannot truncate the snapshot either. Structurally identical to the usage.jsonl defect — a shared "locked JSON read-modify-write" helper covers both, plus the events.jsonl compaction.

Severity

High — corrupts the team's aggregated stats (double-counted sessions), and the corruption is pushed to the shared repo. Less easily triggered than the usage.jsonl race (needs two near-simultaneous auto-pulls), but the damage is durable and team-visible.

---

Found via TLA+/TLC concurrency audit of the sync/state layer. Sibling defects: usage.jsonl lost update (Critical), events.jsonl compaction race (Medium).

[SaulMoro]

The read-read-write-write race looks closed on main (8cee7ab). It was real at 48b3dcb.

• Per-scope snapshots (fix(report): each scope keeps its own reported dashboard snapshots (#786) #795, 352cfc4). Each scope writes its own reported-*.json under its data home (the user scope uses ~/.teamai/dashboard/user-reported-*.json), through scopeSnapshotPath in src/team-push.ts. At 48b3dcb all scopes shared one file, so a user-scope pull and a project-scope pull (each holding a different sync lock) could clobber each other's ack.
• One writer per file, under that scope's sync lock. reportUsageToTeam is the only caller of the three writeReported* functions, and pull is its only caller (src/pull.ts:2049). http scopes are not report targets.
• The lock is held until the report finishes. The summary says auto-report can outlive the lock, but src/pull.ts:2092-2104 releases the sync locks only after usageReport settles (since fix(stats): finish report bookkeeping after pull timeout #562), even when pull stops waiting at 5 s.

Still open, both narrow:

1. readSnapshot (src/team-push.ts:171-181) creates the scope's snapshot, seeded from the shared file, with a plain writeJson and no lock. With fix(stats): await the async dashboard scope filter (#795) #806, teamai stats calls these readers. If stats and a pull both make that first read at the same time, stats can overwrite the ack the pull just wrote. This happens at most once per scope. Creating the file with flag: 'wx' closes it.
2. writeJson is not atomic, so a crash mid-write can truncate a snapshot. That is the crash-safety half of the suggested fix, not the race.

Checked by reading the code on 8cee7ab; I did not run a repro for this one. If you agree, this could be retitled to the two items above, or closed and those tracked separately.