2.4 Ownership Models: Who Controls What, and When?

With one worker, who owns this job? has an obvious answer. Add many workers, a crash, and a sweep that reclaims abandoned work, and the same question acquires time and contention: ownership can be claimed, can expire, and can be reclaimed, and a holder that went away can return to find its claim gone. An ownership model keeps those relationships and discards the rest — who holds what, on what terms, and for how long.

2.4.1 The Canonical Move: Resource Ownership

Software engineering has a long vocabulary for control over a shared resource: locks and leases¹1. Cary G. Gray and David R. Cheriton, “Leases: An Efficient Fault-Tolerant Mechanism for Distributed File Cache Consistency,” in “Proceedings of the Twelfth ACM Symposium on Operating Systems Principles,” special issue, Proceedings of the Twelfth ACM Symposium on Operating Systems Principles (New York), 1989, 202–10, https://doi.org/10.1145/74850.74870., resource-allocation relationships, capability and claim relationships, ownership transfer, and the lifecycle of a claim from acquisition through expiry to reclamation. Ownership is the family the earlier chapters most obviously touch. A claim relates a holder to a resource, which is structural; the claim is acquired, held, and released over time, which is behavioral. That overlap is why ownership is the natural place to show one representation carrying more than one class of question (Figure 2.4-1).

A claim binds a holder to a resource and carries the facts that make contention decidable: which holder, which generation of claim, and when it expires. The generation is the fact a bare "A owns X" edge cannot express — it distinguishes a current claim from a superseded one. The properties a designer wants to state follow from that: at most one valid holder at a time, a stale holder cannot affect the current one, a release or transfer is valid only from the current claim, and abandoned work is eventually reclaimed.

The hard failures do not live in any single transition. They live in the interleavings: the orders in which concurrent claims, expiries, and reclaims can occur. So the characteristic analysis is state-space exploration over those sequences, with an invariant checked at each reachable configuration. This is the behavioral toolkit of the previous chapter pointed at a concurrency question, which is again why ownership reads as an overlap family.

2.4.2 DocAble: In-Flight Ownership

DocAble leases each in-flight job to one worker. A lease carries an owner, a monotonically increasing generation, and a lifetime; when a lease looks abandoned it can be reclaimed and the job re-leased to another worker at the next generation.

MODEL CARD

In-flight lease · Ownership

• Engineering question — Who currently owns this in-flight work, and can a returning stale owner disturb the current claim?
• Model — a claim relating a worker to a job, stamped with a generation and a lifetime; reclaim advances the generation.
• Property — a stale claim cannot clear or supersede the current one.
• Quality attribute — correctness under concurrency; crash-safety.

Start with what the model means. A job is leased exactly when it has an owner; the two are the same fact seen from two sides, so the model represents ownership as the presence of a current claim rather than as a separate flag that could disagree with it. That is a definition, not a property that could fail. It sets up the invariant that can.

The consequential invariant is about time and contention. Suppose worker A holds the claim at generation 7, appears to stall, and is reclaimed; the job is re-leased to worker B at generation 8. If A now wakes and tries to release using its generation-7 claim, that release must not clear B's current generation-8 claim. The generation makes the distinction decidable: a release carrying an old generation names a claim that no longer owns, so it is inapplicable to the current one.

Figure 2.4-2 draws the claim and its lifetime; the generation is the small addition that separates a live claim from a stale one.

As with the recovery ordering, the two layers stay separate. The generation exposes the question — is this release applicable to the current claim? — as one a checker or a release path can decide. Whether the running system holds the line — whether the release path actually compares generations and rejects the stale one — is a matter of enforcement for Part III. That guard is a hard one: the mechanism refuses the stale release rather than merely reporting it, and an exhaustive search over the interleavings serves as its verification. Here the model's job ends at making the invariant precise and checkable.

2.4.3 One Representation, Several Questions

The lease is the Part's clearest case of one representation answering several classes of question. Read it as an ownership model and it says who controls a job. Read the same claims as a behavioral model and they trace a lifecycle — claimed, held, expired, reclaimed. Count the active leases and the same representation becomes a measurement: how much work is genuinely in flight right now. Figure 2.4-3 sets the three readings side by side.

That a lease supports ownership, behavioral, and measurement questions at once is not a sign the model is under-specified. It is the point the classes have been making since the opening chapter: they sort questions, not data structures, and one purposeful representation can answer several when they share the same underlying facts. This is the observation the closing chapter builds on when it connects the models through shared identity.

The lease model makes ownership under contention precise and its key invariant checkable. It does not establish that the implementation obeys the invariant, nor decide what should happen when a stale release is attempted — surface a conflict, drop the release, raise an alarm. Modeling names the claim; Alignment determines whether and how the obligation is enforced.

Ownership introduced permission implicitly: a stale claimant may not clear a current lease. The next family makes permission the whole question.