Appendix C — Model Reference

C.2 Behavior and Ownership

Behavioral models represent state, transition, and time. Ownership models represent who may act on or hold a resource. The two are distinct but often joined: behavior constrains possible transitions; ownership constrains who may perform them.

C.2.1 Lifecycle

Engineering question. What states may this object occupy, and which transitions are legal?

Representation. A minimal job lifecycle moves an item from FREE to LEASED on claim, from LEASED to DONE on completion, and from LEASED back to FREE on expiry or release. DONE is terminal.

Property. The invariants sort into safety and liveness:

Table C.2-1. Representative lifecycle invariants, by kind.
InvariantKind
Only declared transitions occurSafety
Terminal states do not re-enter processingSafety
A claimed job eventually completes or returns to an available state, under stated assumptionsLiveness

Authority and correspondence. Transition operations or checks can mediate actual state changes against the declared transition relation. Any implemented transition absent from that relation becomes a finding. Where two lifecycles interact, represent their cross-machine transitions explicitly rather than leaving those relationships implicit in code.

C.2.2 Ownership and Lease

Concurrency adds ownership and lease state to the lifecycle. The resulting model must represent not only which transitions are legal, but which actor may perform them now.

Engineering question. Who may act on this work item now, and what stays true if workers overlap, fail, or retry?

Figure C.2-1 lays the ownership overlay over the state machine.

Behavior plus ownership — a lifecycle with an ownership overlay that authorizes the worker A behavioral state machine runs left to right: FREE, then LEASED along a solid claim arrow, then DONE along a solid complete arrow. A solid expiry arrow returns LEASED to FREE. DONE is terminal: a short red X marks no re-entry. Below LEASED, an ownership overlay box records lease owner and lease until, joined to the state by a solid specializes arrow — the ownership overlay specializes the LEASED state; ownership is its own working class, shown here joined to behavior. From the overlay, a heavy bordered authorizes-action arrow, crossed by a gate glyph, reaches the worker: this is where a lease or compare-and-swap gate sits. An invariant band beneath reads LEASED implies exactly one valid owner, and FREE implies no active owner. Legend as in Figure C-1; weight, dash, and glyph carry the meaning without colour. Question: who may act on this work item now — and what holds if workers overlap or fail? BEHAVIORAL STATE FREE LEASED DONE claim complete expiry / release no re-entry specializes OWNERSHIP OVERLAY lease_owner = W17 lease_until = t authorizes action CHECKED · lease/CAS worker INVARIANT LEASED ⇒ exactly one valid owner · FREE ⇒ no active owner Legend: see Figure C-1. Ownership is a working class in its own right, shown here joined to behavior.
Figure C.2-1. Behavior plus ownership. The lifecycle FREE → LEASED → DONE is combined with a lease that records the current owner and expiry. The ownership invariant requires exactly one valid owner while LEASED and no active owner while FREE.

Property. Representative invariants:

Authority and correspondence. Some ownership facts are runtime facts and must be observed. The ownership protocol itself is authored intent. Atomic operations, leases, compare-and-swap, transition primitives, and admission checks can make selected invariants enforceable.

Concurrency limits and ownership answer different questions. A semaphore or mediator constrains how many actors may execute; single-writer ownership identifies which actor may mutate. They require distinct representations because they govern different properties.

© James C. Davis, 2026–present