sec-asynchronous-safety
13.3 Running example: stale authority under asynchronous execution
The asynchronous minimization example becomes a safety problem when the updated coordinates encode capabilities, approvals, budgets, or revocations. At an event \(e\), an agent can condition only on \(\mathord \downarrow e\). An external log may later place another event \(f\) before \(e\), but that serialization does not retroactively make \(f\) visible to the agent.
Let \(e\) be a capability-use event and \(f\) a revocation event in an event category \(\mathbb E\). If \(e\) and \(f\) are incomparable, then a decision rule at \(e\) determined only by \(\mathord \downarrow e\) cannot guarantee the external-clock property “a revocation serialized before a use prevents that use” for every linearization of \(\mathbb E\). Such a guarantee requires a causal path \(f\to e\), a synchronization barrier, or a conservative rule that abstains without a sufficiently current authorization witness.
There are linearizations placing \(f\) before \(e\) and placing \(e\) before \(f\). Because \(f\notin \mathord \downarrow e\), the local information supplied to the rule at \(e\) is identical in both. The rule must therefore make the same decision, so it cannot both permit the pre-revocation use and forbid the externally later use solely from its local past.
This is the safety analogue of stale-gradient computation, but the acceptable repair is different. Optimization may tolerate bounded staleness because a contraction eventually absorbs the error. Irreversible external actions may require freshness types, causal revocation delivery, or abstention. Thus a bound that is adequate for convergence need not be adequate for safety.