Lock inference — deciding which process-local variables share a lock, in what order the locks are acquired, and which of them can be dropped.

This module is pure analysis: it answers in variable names and lock groupings, and emits no Go. Network2Go.PlusCal reads the answer and writes the Lock[struct{…}] parameters, MkLock initializers and Acquire/Release calls from it. Keeping the two apart is what lets the inference be checked against worked examples without a Go backend in the way.

Why locks at all. A process's threads run as goroutines over shared process-local state, and an atomic block must observe that state as one indivisible step. Go offers no atomicity, so locks recover it — and then the whole question is how few locks suffice, since one global lock per process would serialize threads that never touch the same variable.

The scheme. shared is the set of process-local variables a piece of code reads or writes. A variable x dominates y (x ⪰ y) when every footprint containing y also contains x; then y can be guarded by x's lock at no cost in concurrency, because everything that had to lock y was going to lock x anyway. Merging along strict domination collapses the one-lock-per-variable assignment down without ever forcing two independent pieces of code to serialize, which is the property that makes this worth doing rather than just locking everything.

Four decisions are this compiler's own:

• Footprints are per branch, not per atomic block. The branch is what executes atomically; the block only chooses among branches, and locks are acquired per branch for that reason. See processFootprints for why the block-level reading serializes branches that should run concurrently.
• self is never locked, being read-only. Nothing special is needed for that here: self is bound by checkProcess rather than declared in localState.variables, and only declared variables are considered, so it drops out of every footprint on its own.
• A receiving thread has a footprint of its own, over its inbox. Thread.rx has no label, no branches and no statements, but it does write the inbox sequence, concurrently with the code threads that drain it — and the whole reason Guarded2Network introduced inbox is that two threads share it. Leaving it out does not break correctness (the receiving thread still acquires whatever lock holds inbox) but it merges away the concurrency: in Ping-Pong's Ping, without it every footprint containing inbox also contains tmp1, so tmp1 ≻ inbox and the two share a lock — and the receiving thread then blocks a send that touches only tmp1.
• Thread-confinement pruning is not implemented. A lock touched from only one thread does guard nothing — Network PlusCal runs at most one block of a given thread at a time, so its blocks are already mutually exclusive — but in this compilation scheme a lock is not only a mutex, it is the variable's storage: a branch function reads its variables out of the struct a lock carries, and INIT_LOCKS is the only place a variable's initial value is ever written. Dropping a lock therefore leaves its variables with nowhere to live. Pruning would need thread-confined variables to become goroutine-local state instead, which the compilation shape rules out: each atomic block is its own top-level function, so it cannot mutate a local of the thread function that started the chain. Worth revisiting only together with that.

Variable sets

Ordered lists rather than HashSets. Order is not incidental here — it becomes the locking order, and through that the order of Acquire calls in generated code — so the analysis has to be deterministic down to the sequence, not just the set.

Free variables

partial def Network2Go.exprFreeVars (bound : List String) : ComputablePlusCal.Expression → List String

The free variables of a TLA⁺ expression, in first-occurrence order, ignoring anything in bound.

Only Origin.free references count. A process-local variable, self, and a statement with local are Memory-keyed and carry .free; a .module reference is a module-level definition, a .intrinsic one a builtin, and a .bound one an expression binder's own variable — none is process state and none can be locked.

Quantifier and function-literal binders are .bound in their body and so never counted; bound still tracks their names defensively. A domain expression is evaluated outside its own binder ([x ∈ D ↦ e] may not mention x in D), so bound grows for e and not for D.

Footprints

def Network2Go.branchShared (br : ComputableNetworkPlusCal.AtomicBranch) : List String

One branch's footprint. The precondition runs first and its with bindings stay in scope for the action, which is why one Footprint is threaded through both rather than two being merged.

Equations

• One or more equations did not get rendered due to their size.

def Network2Go.blockShared (B : ComputableNetworkPlusCal.AtomicBlock) : List String

shared(B) for a whole atomic block: the union over its branches. A branch is one way the block can fire, and the block's lock set has to cover every way.

Equations

• Network2Go.blockShared B = List.foldl (fun (acc : List String) (br : ComputableNetworkPlusCal.AtomicBranch) => Network2Go.unionVars✝ acc (Network2Go.branchShared br)) [] B.branches

def Network2Go.processFootprints (p : ComputableNetworkPlusCal.Process) : List (List String)

Every footprint of a process — one per branch, plus one per receiving thread — narrowed to the process's declared variables.

Per branch, not per block. The unit that executes atomically is the branch; a block only chooses among its branches, and locks are acquired per branch for exactly that reason. Taking the block's footprint — the union over its branches — makes two branches that touch disjoint variables look like joint users of both, so those variables dominate each other, merge into one lock, and each branch then acquires a lock bundling the other's variables. That serializes precisely the pair that should stay concurrent. Branch footprints are the finer relation and merge strictly less; correctness is unaffected, since any assignment giving each variable exactly one lock is sound and every branch still acquires every lock covering what it touches.

A Thread.rx contributes one footprint over its inbox although it has neither label nor branches — see the module doc for why leaving it out would be wrong.

Narrowing here rather than inside exprFreeVars is what keeps self, quantifier binders and operator parameters out without naming any of them: none of the three is declared.

Equations

• One or more equations did not get rendered due to their size.

Lock selection

structure Network2Go.Lock : Type

One inferred lock: a Go-side name and the variables it guards.

vars is in the process's declaration order, which fixes the field order of the struct the lock holds — generated code projects those fields out after Acquire and reassembles them before Release, so the order has to be stable across every site that names the lock.

• name : String
• vars : List String

def Network2Go.instReprLock.repr : Lock → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network2Go.instReprLock : Repr Lock

Equations

• Network2Go.instReprLock = { reprPrec := Network2Go.instReprLock.repr }

@[implicit_reducible]

instance Network2Go.instInhabitedLock : Inhabited Lock

Equations

• Network2Go.instInhabitedLock = { default := Network2Go.instInhabitedLock.default }

structure Network2Go.ProcessLocks : Type

A process's whole lock assignment: the locks in locking order, and which lock (if any) each process-local variable is guarded by.

A variable missing from ofVar is one no lock protects — either nothing touches it, or its lock was pruned as thread-confined. Reading or writing it needs no Acquire at all.

The set a given piece of code acquires is derived on demand through acquiredBy rather than tabulated per block, because acquisition is per branch, not per block: a block whose two branches touch disjoint variables should let a concurrent block touching one of them run while the other branch holds only its own. Blocks are still the unit the inference runs over — shared(B) is a block-level set — so the two granularities genuinely differ and neither replaces the other.

Every generated function takes all the locks as parameters regardless, since a goto may hand control to a block with a different footprint.

• locks : List Lock
• ofVar : List (String × ℕ)

def Network2Go.instReprProcessLocks.repr : ProcessLocks → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network2Go.instReprProcessLocks : Repr ProcessLocks

Equations

• Network2Go.instReprProcessLocks = { reprPrec := Network2Go.instReprProcessLocks.repr }

@[implicit_reducible]

instance Network2Go.instInhabitedProcessLocks : Inhabited ProcessLocks

Equations

• Network2Go.instInhabitedProcessLocks = { default := Network2Go.instInhabitedProcessLocks.default }

def Network2Go.ProcessLocks.acquiredBy (ls : ProcessLocks) (shared : List String) : List ℕ

The locks a piece of code touching shared must hold, as indices into locks, ascending.

Ascending is the whole point: acquiring in one fixed order everywhere is what rules out a lock-ordering deadlock between two blocks that need the same pair. Callers acquire in list order and may release in any.

Equations

• ls.acquiredBy shared = List.filterMap (fun (x : Network2Go.Lock × ℕ) => match x with | (l, i) => if shared.any l.vars.contains = true then some i else none) ls.locks.zipIdx

def Network2Go.assignLocks {m : Type → Type} [Monad m] [MonadFresh m] (fps : List (List String)) (vars : List String) : m ProcessLocks

The merge, over footprints that have already been computed. vars is every lockable variable in declaration order.

Split out from inferLocks so that it stays callable on a bare footprint list: a worked example gives footprints directly and says nothing about the code that produced them.

Equations

• One or more equations did not get rendered due to their size.

def Network2Go.inferLocks {m : Type → Type} [Monad m] [MonadFresh m] (p : ComputableNetworkPlusCal.Process) : m ProcessLocks

The whole inference for one process: compute every block's footprint, then assign locks.

A variable no block touches gets no lock at all — it is process-local state nothing races on.

Equations

• One or more equations did not get rendered due to their size.