Compiling Network PlusCal processes into Go, on top of the TLA⁺ half (Network2Go.{Typ,Expression,Definition}) and the lock assignment (Network2Go.Locks).

The shape. An atomic block does not become a Go block. Each of its branches becomes a top-level function returning bool — "did I fire" — and the block itself becomes a scheduler function looping over them, picking one at random per iteration and stopping once one returns true. Control then leaves through goto, which spawns a goroutine running the next block's scheduler rather than calling it: a chain of blocks is unbounded, and Go's goroutine stacks are small and growable, so a tail call would eventually overflow one.

The loop is a busy-wait, and knowingly so: a failed iteration still pays for its lock acquisitions and its guard evaluation. Condition variables would avoid that and are much harder to state a correctness property about. Go's runtime also preempts on channel operations, which is exactly what Acquire/Release are, so the loop does not spin freely in practice.

Every function takes every lock, whether it acquires it or not, because a goto may hand control to a block with a different footprint and the lock has to reach it. Which locks a piece of code acquires is decided per branch, not per block: two branches of one block touching disjoint variables should not serialize against each other.

Locks are storage, not just mutual exclusion. A process-local variable exists only inside the struct its lock carries; a branch projects the variables out after Acquire and reassembles them before Release, and INIT_LOCKS in the process function is the only place an initial value is ever written. This is why Network2Go.Locks does not prune thread-confined locks.

Four choices are this compiler's own:

• Names. A readable scheduler name like SndPi, or a process function called Pong, collides with what a user-written definition of the same name compiles to — and PingPongs.tla really does have a process Ping beside a CONSTANT Ping. The synthesized names go through Naming's blockName/branchName/threadName/processName instead.
• Assignment through a reference. Compiling r ≔ e index by index would assume a TLA⁺ function is a Go map. Here it is a LazyFunction, and a sequence is 1-indexed, so x[i] := e compiles the way [x EXCEPT ![i] = e] does — through compileExcept, which already knows all three cases (function, sequence, tuple).
• LOCK/UNLOCK are locks.Acquire/locks.Release calls, not raw channel operations, so that Lock[τ] = chan τ stays inside the runtime library.
• multicast compiles to a single comm.Multicast call. The iteration lives in the runtime library rather than in emitted code: the specification fixes no order on the sends, so there is nothing for a generated loop to say that the library cannot. The payload becomes a function literal from the recipient, which is why ProcEnv carries the channels' element types — Go infers a literal's parameter types from nothing, and demands its result type outright.

Go fragments used throughout

def Network2Go.unitTyp : Go.Typ

Go's unit type, struct {} — the element type of every done channel here.

Equations

• Network2Go.unitTyp = Go.Typ.struct []

def Network2Go.unitVal : ComputableGo.Expression

struct {}{}, the sole value of unitTyp.

Equations

• Network2Go.unitVal = Go.Expression.structLit Network2Go.unitTyp []

def Network2Go.doneTyp : Go.Typ

chan struct {}.

Equations

• Network2Go.doneTyp = Network2Go.unitTyp.chan

def Network2Go.goBoolTyp : Go.Typ

Go's own bool, as opposed to the runtime's tlaplus.Bool. A branch's guard and a scheduler's shouldContinue are Go booleans: they drive if and for, which the runtime type cannot.

Equations

• Network2Go.goBoolTyp = Go.Typ.named "bool" []

def Network2Go.locksCall (name : String) (args : List ComputableGo.Expression) : ComputableGo.Expression

locks.f(e₁, …).

Equations

• Network2Go.locksCall name args = (Network2Go.locksVar name).call args

def Network2Go.condlocksCall (name : String) (args : List ComputableGo.Expression) : ComputableGo.Expression

condlocks.f(e₁, …).

Equations

• Network2Go.condlocksCall name args = (Network2Go.condlocksVar name).call args

Per-process environment

structure Network2Go.ProcEnv : Type

Everything the compilation of one process's blocks needs to agree on: the names its generated functions bind, and the lock assignment they all share.

self is not freshly named. A compiled expression mentioning self goes through binderName, so the parameter has to answer to exactly that; the elaborator binds self rather than declaring it, so no process-local variable can collide with it. net and done are fresh, since nothing in a compiled expression refers to them and a process variable named net is perfectly legal.

• proc : String

  The process's source-level name, which every synthesized function name is qualified by.

• locks : ProcessLocks
• varTyps : List (String × ComputableTLAPlus.Typ)

  Declared process-local variables and their types, in declaration order.

• chanTyps : List (String × ComputableTLAPlus.Typ)

  Every channel of the whole specification and the type it carries — the Network struct is algorithm-wide, so a process may send/multicast on one another process declared. Needed where a channel's element type cannot be read off the statement: multicast's payload compiles to a function literal, and Go requires a literal to state its result type.

• net : String
• self : String
• done : String
• condBackend : Bool

  Whether this process compiles under the experimental -Xgo-cond backend rather than the default busy-wait one. The two share every field above — lock inference does not care how a lock is represented at runtime — and differ only in which package a lock's type/calls name and in how an atomic block's branches are scheduled.

def Network2Go.lockStructTyp {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (env : ProcEnv) (l : Lock) : m Go.Typ

The struct {x τ, …} a lock carries: one field per variable it guards, in declaration order.

The field order is fixed by Lock.vars rather than sorted, unlike a compiled record type. Nothing structural depends on it here — this type is written out at every site that mentions the lock, and all of them get it from this function.

Equations

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

def Network2Go.lockTyp {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (env : ProcEnv) (l : Lock) : m Go.Typ

The Go type of one lock: locks.Lock[struct {x τ, …}], or condlocks.Lock[struct {x τ, …}] under -Xgo-cond.

Equations

• Network2Go.lockTyp env l = do let τ ← Network2Go.lockStructTyp env l pure (if env.condBackend = true then Network2Go.condlocksTyp "Lock" [τ] else Network2Go.locksTyp "Lock" [τ])

def Network2Go.acquireCall (env : ProcEnv) (l : Lock) : ComputableGo.Expression

Acquire respelled for whichever lock representation env selects: locks.Acquire(ℓ), a free function, by default; ℓ.Acquire(), a method, under -Xgo-cond, whose Lock carries an extra change signal Acquire itself never touches.

Equations

• Network2Go.acquireCall env l = if env.condBackend = true then ((Go.Expression.var l.name).field "Acquire").call [] else Network2Go.locksCall "Acquire" [Go.Expression.var l.name]

def Network2Go.releaseCall (env : ProcEnv) (l : Lock) (v : ComputableGo.Expression) : ComputableGo.Expression

Release respelled the same way — under -Xgo-cond this is always the broadcasting release, ℓ.Release(v); a guard-false attempt there calls ReleaseNoBroadcast directly instead of this.

Equations

• Network2Go.releaseCall env l v = if env.condBackend = true then ((Go.Expression.var l.name).field "Release").call [v] else Network2Go.locksCall "Release" [Go.Expression.var l.name, v]

def Network2Go.mkLockCall (env : ProcEnv) (v : ComputableGo.Expression) : ComputableGo.Expression

MkLock respelled for whichever package env selects. Always a free function in both backends — nothing to construct it from yet — so only the package qualifier differs.

Equations

• Network2Go.mkLockCall env v = (if env.condBackend = true then Network2Go.condlocksCall else Network2Go.locksCall) "MkLock" [v]

def Network2Go.releaseNoBroadcastCall (l : Lock) (v : ComputableGo.Expression) : ComputableGo.Expression

ℓ.ReleaseNoBroadcast(v) — -Xgo-cond only, the guard-false release that leaves the value unchanged and returns the change signal to wait on next, snapshotted before the release completes.

Equations

• Network2Go.releaseNoBroadcastCall l v = ((Go.Expression.var l.name).field "ReleaseNoBroadcast").call [v]

def Network2Go.lockParams {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (env : ProcEnv) : m (List (String × Go.Typ))

The lock parameters every generated function takes, in locking order.

Equations

• Network2Go.lockParams env = List.mapM (fun (l : Network2Go.Lock) => do let __do_lift ← Network2Go.lockTyp env l pure (l.name, __do_lift)) env.locks.locks

def Network2Go.lockArgs (env : ProcEnv) : List ComputableGo.Expression

The lock arguments, matching lockParams position for position.

Equations

• Network2Go.lockArgs env = List.map (fun (l : Network2Go.Lock) => Go.Expression.var l.name) env.locks.locks

def Network2Go.commonParams {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (env : ProcEnv) : m (List (String × Go.Typ))

The parameter list shared by branch, block-scheduler and thread functions: (ℓ₁, …, ℓₖ, net, self, done).

Equations

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

def Network2Go.commonArgs (env : ProcEnv) : List ComputableGo.Expression

The matching argument list.

Equations

• Network2Go.commonArgs env = Network2Go.lockArgs env ++ [Go.Expression.var env.net, Go.Expression.var env.self, Go.Expression.var env.done]

def Network2Go.dropCall (f : String) (args : List ComputableGo.Expression) : ComputableGo.Statement

_ = f(args…) — a call whose result is deliberately dropped. Every generated function returns struct {} or bool, and Go rejects a bare call only for the sake of the value, so the blank assignment is what makes go { … } around one legal.

Equations

• Network2Go.dropCall f args = Go.Statement.assign [Go.Ref.wildcard] [(Go.Expression.var f).call args]

Statements

def Network2Go.compileGuard {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (guardVar : String) : ComputableNetworkPlusCal.Statement true false → m (List ComputableGo.Statement)

A branch's guards. await conjoins onto guard unconditionally — its condition is always total, an ordinary TLA⁺ boolean, so evaluating it after guard has already gone false costs nothing but a redundant read. A with is not total: with x = e's e can be a CHOOSE/search with no witness, and with x ∈ e's e can be an empty (or infinite) set — either is undefined exactly when some guard textually before it already made the branch not fire. So only the binder's own evaluation is gated, by the current guard at that point — var x τ (no initializer, nothing to evaluate) sits outside the if, the assignment inside it. Nothing else in the branch needs to nest: guard only ever narrows (&&), never recovers, so a later statement reading guard — the next with's own if, another await, or the branch's final if guard { action } — sees the same false once anything upstream has failed, whether or not this with actually ran. (A later with's e may then read x at its zero value rather than a real one, if guard was already false here — harmless, since that later with is itself gated on the same guard and so skips its own assignment too, never forcing the zero value through anything partial.) One if per with, each independent — not one nested inside the last.

with x ∈ e compiles through Pick (runtime/tlaplus/sets.go), the same uniform-random draw a variable x ∈ S initializer already uses (initLocks below): pick now, unconditionally on whatever e denotes at this attempt, and let a guard after this with reject the draw the ordinary way — guard goes false, the branch function returns false, and the block's scheduler (this file's top comment) retries with a fresh iteration, which re-enters this with and draws again. There is deliberately no search for a value satisfying what follows: the specification only requires some run to reach a satisfying draw, and every failed one is exactly as cheap as any other failed guard.

Equations

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

def Network2Go.compileAction {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) {b : Bool} : ComputableNetworkPlusCal.Statement false b → m (List ComputableGo.Statement)

A branch's action statements. These run only once every guard has passed, so they are emitted inside the branch's if guard { … }.

Equations

• One or more equations did not get rendered due to their size.
• Network2Go.compileAction env NetworkPlusCal.Statement.skip = pure []
• Network2Go.compileAction env (NetworkPlusCal.Statement.print e) = do let __do_lift ← Network2Go.compileExprTop e pure [Go.Statement.expr (Network2Go.tlaplusCall "Print" [__do_lift])]
• Network2Go.compileAction env (NetworkPlusCal.Statement.send c e) = do let __do_lift ← Network2Go.compileSend✝ env (posOf (NetworkPlusCal.Statement.send c e)) c e pure [__do_lift]

Locks around a branch

Branches, blocks, threads, processes

def Network2Go.compileBranch {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (label : String) (i : ℕ) (br : ComputableNetworkPlusCal.AtomicBranch) : m ComputableGo.Function

One branch of an atomic block, as its own bool-returning function.

The order is fixed by what depends on what: guard first, then the locks (a guard reads locked variables), then the guards — each compileGuard result appended flat, per its own doc comment — then the body under one if guard, then the releases, then return guard. The releases sit outside the if because the locks were acquired outside it too.

Equations

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

def Network2Go.compileBlock {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (B : ComputableNetworkPlusCal.AtomicBlock) : m (List ComputableGo.Declaration)

An atomic block: its branch functions, plus the scheduler that picks between them.

shouldContinue = !branch(…) is the whole protocol — a branch returns whether it fired, and the loop stops exactly when one did. With a single branch the switch is redundant (Rand(0, 1) is always 0); the thesis emits it anyway and so does this, leaving the peephole to a later pass rather than special-casing the shape here.

The ToInt around the switch head is load-bearing rather than cosmetic. Rand is typed over the runtime's Int, which under the default arbitrary-precision build is a struct — an Int-valued switch head could not match the integer-literal cases, and Go would reject the function.

Equations

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

Branches and blocks, experimental -Xgo-cond backend

def Network2Go.compileBranchCond {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (cancel arbiter label : String) (i : ℕ) (br : ComputableNetworkPlusCal.AtomicBranch) : m ComputableGo.Function

One branch of an atomic block under -Xgo-cond, as its own struct {}-returning function taking two parameters beyond commonParams: cancel, closed once by whichever branch of the block resolves it, and arbiter, the one-shot arbitration every simultaneously-true branch of the block shares — lock exclusivity alone only serializes branches whose footprints overlap, and says nothing about two branches on disjoint locks that are both true at once.

Loops, unlike compileBranch: a guard-false attempt releases without broadcasting, gets back the change signal ReleaseNoBroadcast snapshots before releasing, and sleeps on it — or on cancel, which every sibling branch not sharing this one's locks would otherwise never wake for — before retrying. The nonblocking recheck right after the sleep is not redundant: select has no priority, so a live change can win the pseudo-random pick over an already-closed cancel, and without the recheck this branch could keep retrying a resolved block for as long as something else keeps touching its locks.

A guard-true attempt always returns, win or lose the arbitration — the block is resolved either way, and a loser must release exactly what it acquired, never running its action.

Equations

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

def Network2Go.compileBlockCond {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (B : ComputableNetworkPlusCal.AtomicBlock) : m (List ComputableGo.Declaration)

An atomic block under -Xgo-cond: its branch functions, spawned as goroutines racing on a cancel/arbiter pair fresh to this block instance, plus the function that spawns them and blocks on <-cancel until one resolves the block.

Blocking before returning, rather than returning the moment every branch is spawned, is what keeps this function's calling convention identical to compileBlock's scheduler: compileCodeThread's caller (ultimately compileProcess's thread_k, called synchronously) sees the same run-to-resolution contract from either backend.

Equations

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

def Network2Go.compileCodeThread {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (k : ℕ) (blocks : List ComputableNetworkPlusCal.AtomicBlock) : m (List ComputableGo.Declaration)

A code thread: every block it contains, plus the function that starts the chain by calling the first one. Everything after that first block happens through goto's goroutines, so this really is all a thread needs.

A thread with no blocks compiles to a function that does nothing. That is not a degenerate case to reject: @rx-annotated threads are written {} in the source, and Guarded2Network turns them into Thread.rx — but an ordinary empty thread is legal too, and denotes a process component that terminates immediately.

Equations

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

def Network2Go.compileRxThread {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (k : ℕ) (τ : ComputableTLAPlus.Typ) (inbox : String) : m ComputableGo.Declaration

A receiving thread: loop on mailbox.Recv(), and on each message that arrives, acquire the lock holding inbox just long enough to append.

Locking only around the append is the point. Recv blocks — possibly forever, if no peer ever sends — and a thread that held inbox's lock across that call would freeze every block trying to consume a message, including ones with nothing to consume. ok going false means the medium is gone, which is how the loop terminates instead of blocking against a channel nobody will write to.

This thread takes mailbox in place of done: it never finishes on its own, so it has nothing to signal.

Equations

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

def Network2Go.initLocks {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (env : ProcEnv) (inits : List (String × Bool × Option (Bool × ComputablePlusCal.Expression))) : m (List ComputableGo.Statement)

A process's initialization prologue: the declaration walk, then the initial lock values (INIT_LOCKS).

The walk is in declaration order, and interleaves two different things. A @parameter emits no local — its value comes from the caller, as a parameter of the process function, so binderName x already names it — but its declared bound becomes an assertion. Every other variable emits a Go local: Pick(S) for an ∈ initializer, the compiled expression for =, and nothing for an uninitialized one, which leaves it at Go's zero value (the runtime types are built to accept theirs — tlaplus.Int's reads as 0 rather than dereferencing a nil pointer).

Interleaving rather than asserting everything up front is what lets a bound name an earlier local. Nothing forces the other order: a parameter is live from function entry, a local is computed from parameters and earlier locals, and an assertion computes nothing, so declaration order is both what PlusCal's sequential initializers already mean and the order that fires each assertion as early as it can — before an initializer that could panic on the very value the assertion is there to reject.

Locals come before locks because a lock is where the variable lives. A process-local exists only inside its lock's struct, so an initializer naming an earlier sibling would otherwise compile to a Go identifier that does not exist; with the locals emitted first, each lock's struct is built by naming them.

Equations

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

def Network2Go.compileProcess {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (condBackend : Bool) (chanTyps : List (String × ComputableTLAPlus.Typ)) (p : ComputableNetworkPlusCal.Process) : m (List ComputableGo.Declaration)

A whole process: its threads' functions, and the function that starts them.

The process function returns done immediately rather than blocking, so its caller decides when to wait. Each code thread signals the buffered done' when it reaches goto Done; a final goroutine reads done' once per code thread and only then signals the unbuffered done. Receiving threads never signal: they run until the medium vanishes, which is not the process finishing.

mailbox is a parameter, not something the generated code constructs. The compiler emits no main and takes no position on how processes find each other — whoever assembles the system supplies a Receiver backed by a socket, a queue, or a Go channel.

Equations

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

def Network2Go.channelTyps (algo : ComputableNetworkPlusCal.Algorithm) : List (String × ComputableTLAPlus.Typ × List ComputablePlusCal.Expression)

Every channel and FIFO of the whole specification, algorithm-level and process-local alike, as (name, element type, index-domain expressions). Both the Network struct below and ProcEnv's own channel table are built from this one list — the struct is algorithm-wide, so a process may name a channel another process declared.

Equations

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

def Network2Go.networkTyp {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (algo : ComputableNetworkPlusCal.Algorithm) : m ComputableGo.Declaration

The Network struct type: one field per channel of the whole specification, holding the sending end only — a process reads from its own mailbox, which it is handed directly, and never from the network at large.

A channel declared with an index domain (pong[Pongs]) becomes a map[Address]Sender[τ], which is what makes net.c[e].Send(…) resolve; one declared without becomes a plain Sender[τ].

Equations

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

def ComputableNetworkPlusCal.Algorithm.toGo {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (algo : Algorithm) (condBackend : Bool := false) : m (List ComputableGo.Declaration)

A whole algorithm: the Network type, then every process.

Order is for readability only — Go resolves package-level declarations regardless of the order they appear in.

Sits outside namespace Network2Go so that algo.toGo resolves by dot notation, matching Guarded2Network/PlusCal.lean's guarded.toNetwork — Driver/Pipeline.lean calls each pass that way.

condBackend selects the experimental -Xgo-cond scheme for every process of the algorithm — an algorithm compiles as a whole under one backend or the other, never a mix, since it is one .go file and every process there shares the runtime import list Network2Go.Emit computes from it.

Equations

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