Appendix C. Draft 0.6 and 0.6b concurrency (normative for version 0.6 and 0.7 modules)

The 23 words below are reserved in a version 0.6 module, in addition to the 0.5 keywords of 2.4, except directly after . (so c.offer() and c.choose(L) remain method calls):

par       branch    nondet    budget    deadline  priority
replicated interrupt session  lvar      group     lanes
barrier   scope     atomic    protocol  offer     choose
node      supervisor strategy child     restart

In a 0.5 module they are names (fn f(node: i64) is valid 0.5). The reference checker keeps them in parse::DRAFT06_KEYWORDS, separate from parse::KEYWORDS, and reserves them only when the module is version 0.6 or 0.7.

These productions extend section 3 for version 0.6 modules. They are the productions of the tree-sitter port (spec/tree-sitter/grammar.js) and of the Rust parser. A rule below with the name of a section-3 rule replaces it for a 0.6 module; the others are new. The machine check of 3.12 also builds the LALR(1) tables of section 3 with these rules applied (lalr::book_grammar_06), lexing with the keywords of C.1 reserved, and fails on any conflict; it runs that machine over the 0.6 corpora (spec/conc06, spec/conc06b). So T10 (one parse per program) holds for version 0.6 modules too.

Item         = UseDecl | IntentDecl | ExampleDecl | CheckDecl
             | [ "pub" ] ( ConstDecl | TypeDecl | StructDecl | KindDecl
                         | TraitDecl | FnDecl | ActorDecl | ProtocolDecl )
             | StateDecl | EventDecl | ErrorDecl | StepDecl | ImplDecl
             | ExternDecl | NodeDecl | SupervisorDecl .
StateDecl    = [ "replicated" ] "state" NAME NEWLINE INDENT Field { Field } DEDENT .
EventDecl    = [ "interrupt" ] "event" NAME [ Payload ] [ "priority" Expr ] NEWLINE .
StepDecl     = "step" NAME "on" Pattern [ "if" Expr ] [ "deadline" Expr ] StepBody .
ProtocolDecl = "protocol" NAME NEWLINE INDENT ProtoStep { ProtoStep } DEDENT .
ProtoStep    = "send" Type NEWLINE | "recv" Type NEWLINE
             | "offer" NEWLINE INDENT ProtoArm { ProtoArm } DEDENT
             | "choose" NEWLINE INDENT ProtoArm { ProtoArm } DEDENT
             | "loop" NEWLINE INDENT ProtoStep { ProtoStep } DEDENT
             | "break" NEWLINE .
ProtoArm     = NAME NEWLINE [ INDENT ProtoStep { ProtoStep } DEDENT ] .
NodeDecl     = "node" NAME "{" NAME { "," NAME } "}" NEWLINE .
SupervisorDecl = "supervisor" NAME "strategy" NAME NEWLINE INDENT SupChild { SupChild } DEDENT .
SupChild     = "child" NAME ":" TypePath [ "restart" Bound ] NEWLINE .
BaseType     = TypePath | "(" ")" | "(" Type "," [ Type { "," Type } [ "," ] ] ")"
             | "(" Type ")" | "[" Type "]" | "[" Type ";" Expr "]"
             | "chan" BaseType | "iter" BaseType
             | "fn" "(" [ TypeList ] ")" "->" BaseType
             | "session" TypePath | "lvar" BaseType .
Stmt         = SimpleStmt | LetStmt | VarStmt | IfStmt | WhileStmt | LoopStmt
             | ForStmt | MatchStmt | ReturnStmt | BreakStmt | ContinueStmt
             | EmitStmt | FailStmt | SpawnStmt | SelectStmt | ArenaStmt
             | DeviceStmt | YieldStmt | ComptimeStmt | CheckDecl | PassStmt
             | ParStmt | BudgetStmt | DeadlineStmt | GroupStmt | BarrierStmt
             | ScopeStmt | AtomicStmt .
ForStmt      = "for" Pattern "in" Expr [ "par" ] Block .
SpawnStmt    = "spawn" Expr [ "priority" Expr ] [ "->" NAME ] NEWLINE .
SelectStmt   = "select" [ "nondet" ] NEWLINE INDENT SelectArm { SelectArm } DEDENT .
ParStmt      = "par" NEWLINE INDENT Branch { Branch } DEDENT .
Branch       = "branch" NAME Block .
BudgetStmt   = "with" "budget" Expr Block .
DeadlineStmt = "with" "deadline" Expr Block [ "else" Block ] .
GroupStmt    = "with" "group" NAME "lanes" Expr Block .
BarrierStmt  = "barrier" NEWLINE .
ScopeStmt    = "scope" Block .
AtomicStmt   = "atomic" Block .

The footprint of a statement is the set of place paths (5.6) it reads and the set it writes. Two branches are disjoint when no path written by one is a prefix of, or has as prefix, a path read or written by the other.

par runs its branches; each branch is a block. The result equals running the branches in source order (C.4.2). Rules:

• W-PAR-1: the footprints of two branches overlap (write/write or write/read), including through a &mut self method call.
• W-PAR-2: a branch has an effect other than its own writes (emit, channel operations, spawn, foreign calls), or returns, breaks or continues out of the par.
• W-NAME-2 also refuses two branches with one name.

• with budget n runs the block with a cost budget n: every Form operation charges its cost (C.6.4) and the operation that takes the total past n is trap("budget"), at the same operation on every target. The cost table is the reference evaluator's (interp and conc.rs, charge), listed in C.6.4. W-TY-1 if n is not an integer.
• with deadline n runs the block with an expiry n logical ticks after entry; if the block has not completed by then, the else block runs instead (T22). W-DL-1: outside fn main or a task function.
• select nondet may take any ready arm; the choice is an input and is logged, so replay reproduces it (T21). W-ND-1: outside fn main or a task function. select without nondet keeps the rotation rule of 6.8.
• spawn f(...) priority p and event E priority p: admission prefers the highest pending priority (T25). W-TY-1 if p is not an integer.

C.6.1 A cost is a non-negative integer number of units. Cost is a deterministic accounting of Form operations, the same on every target; it is not a measurement of time or energy (est_j is separate).

C.6.2 Charging point. An operation charges its cost after its operands are evaluated and before it acts. If the charge would take any enclosing budget past its limit, the operation is trap("budget") and does not act; otherwise every enclosing budget is charged. So nested budgets see the same operation trap, and a budget n admits exactly the operations whose running total stays at most n.

C.6.3 par and for ... par charge c_fork per branch (or chunk), then each branch's own costs. The branches' costs are summed in source order, and exhaustion is placed where the sequential run would hit it (C.4.2), so the trap does not depend on scheduling.

C.6.4 The cost table (normative). Operations not listed (literals of scalars, variable reads, assignment, control flow, let) cost 0. The table is checked against the reference evaluator, and the emitted Rust, Python and JavaScript runtimes charge the same costs (spec/checker/tests/stdlib_costs.rs).

Method work (normative for version 0.7). In a version 0.6 module a standard library method costs c_call whatever its sizes, as draft 0.6 defined it; a budget there bounds the number of operations. In a 0.7 module it costs c_call plus work(m, n, k). A budget is a proxy for energy, and energy scales with the operations performed, so a method's cost must track its work. Sizes: text is its UTF-8 byte length, a list its length, a map its number of entries, any other value 0. n is the receiver's size and k the first argument's (0 when there is none). work(m, n, k) is fixed by the method's complexity class in the reference evaluator:

The calls a map, filter or fold makes to its function argument are charged as calls in addition (c_call each, plus their bodies). The arithmetic saturates at the largest i128, so it cannot overflow; no reachable size comes near it, so the Python and JavaScript runtimes, whose integers are unbounded, give the same numbers. work is monotone: it never decreases when n or k grows. The reference evaluator (conc::method_work) and the Rust, Python and JavaScript runtimes compute the same function, and the budget boundary falls on the same operation in all of them (spec/checker/tests/method_costs.rs, which also checks monotonicity).

Inside a device region (5.13), a version 0.6 module may use par and for ... par with the same rules; the device rules of W-DEV-1 still apply.

for x in e par runs the iterations as if in order. It is encoded in the reference checker as the marker region $forpar (the AST has no new variant). Rules:

• W-PAR-3: the body writes a place other than as a reduction (+= *= &= |= ^= on a variable never read in the body) or as slot [i] of a range loop over i.
• W-PAR-4: the body has an effect, or returns, breaks or continues.

A reduction is evaluated on a fixed tree, which equals the left fold for an associative operation with an identity (T18).

• C.11.2 Workgroups. with group g lanes n runs n lanes in phases separated by barrier. W-GRP-1: a group not directly inside a device region. W-GRP-2: barrier other than as a statement at the top level of a group body. W-GRP-3: a lane reads another lane's slot in the same phase, or lanes share a scalar written in the phase.
• C.11.3 Sessions. protocol P declares a session type; a value of type session P is an endpoint. W-SES-1: an operation not allowed by the protocol state, an unknown label, offer() not matched over its labels, a match that does not handle every label, or branches leaving the endpoint in different states. W-SES-2: an endpoint not at the end of its protocol when it goes out of scope or is closed. W-SES-3: a label that appears twice, a protocol loop with no message before it repeats, or break outside a protocol loop. W-TY-1: a payload of the wrong type.
• C.11.5 Merge. impl Merge for T declares a join. The admission gate (conc::crdt_gate) checks the merge laws (commutative, associative, idempotent) by evaluation on generated values; a failure is W-CRDT-1.
• C.11.8 LVars. lvar T requires T: Merge (W-CRDT-1). W-LVAR-1: freeze() before the par or loop that puts to the LVar has joined. W-LVAR-2: wait with other than one threshold.
• C.11.9 Structured spawn. spawn f(...) -> h gives a join handle. In a version 0.6 module a task function may spawn only inside scope; fn main is an implicit scope (W-SCOPE-1). A join handle cannot leave its scope (W-SCOPE-1). A 0.5 module keeps the rule of 5.8: any task function may spawn.
• C.11.10 Transactions. atomic applies all its actor sends or none (T30). W-ATOM-1: spawn, a receive, select or another wait inside atomic. W-ATOM-2: actors of one atomic on different nodes.
• C.11.11 Placement and supervision. node N {A, B} places actors on a node. W-NODE-1: a placed name that is not an actor, or an actor placed twice. supervisor S strategy k with k one of one_for_one, one_for_all, rest_for_one (W-SUP-1); each child must be an actor (W-SUP-2), and W-NAME-2 refuses a duplicate child.
• C.11.12 Real time. interrupt event E priority p with p an integer literal in 0..=255 (W-INTR-1). step ... deadline n with n a positive integer literal in ticks, and const TICK_NS: u64 = n when declared (W-RT-1). TICK_NS only relates logical ticks to a nominal duration for reporting; no construct reads a wall clock (6.3 N11).
• C.11.4 Replicated state. replicated state R is a region whose log is shared by replicas; a replica that applied a prefix of the log holds the fold of that prefix (T31).

The reference checker also raises three rules that belong to the 0.5 language and are now listed in section 7: W-MOD-3 (an imported name that clashes with a declaration or with another import; names are not renamed), W-VIS-1 (use of a name private to its module, the form W-MOD-1 takes in link.rs) and W-TRAIT-3 (a type used with ==, < or a generic bound that does not implement the required trait).

Status is stated exactly. "Proved on a semantics" means a Lean proof over a small-step semantics of a core of RCE. "Model" means a Lean proof about an abstract model that is not connected to the RCE semantics or to the reference evaluator. "Vectors" means the reference evaluator's results on generated programs are checked against the model by the Lean kernel; that is a correspondence on samples, not a proof about the evaluator.

None of T16 to T31 is a proof about the Rust reference evaluator. The checker rules W-PAR-1 to 4 and W-GRP-1 to 3 are not linked to the Lean footprints beyond the core of ParSem.lean (W-PAR-1 on variables).

rce run runs version 0.6 programs on the reference evaluator (conc.rs). The program emitters (emit/conc06.rs) run par branches in source order (C.4.2), which the meaning allows; a par whose branches wait on LVars is run by restart, and budgets charge the same costs as the evaluator, so trap("budget") falls on the same operation on every target. Workgroups run lane after lane per phase. The 0.6b actor, session and node constructs follow the limits of 10.5.

# rce-version: 0.7 declares version 0.7. Its syntax, keywords, static rules and evaluation are those of version 0.6, with one difference: a standard library method costs c_call + work(m, n, k) (C.6.4) instead of c_call. The rule that decides what needs a new version: a module's meaning (its outputs, states and outcomes, including where a budget traps) must be determined by its declared version, so a change that gives a valid program of an existing version a different meaning that the old text defined is a new version; a change that makes the implementations meet text that already defined the meaning, or that only touches artifacts outside a program's meaning, is an erratum and applies to every version.

Which version governs a cost (normative). A program may join modules of different versions (2.7). The cost of a standard library method call is fixed by the declared version of the module that contains the call expression, not by the version of the module that declared the function being run, of its caller, or of the program's first module. A call written in a 0.7 module, including one inside a closure written there, costs c_call + work(m, n, k) wherever it is executed from, and a call written in a 0.5 or 0.6 module costs c_call even when a 0.7 module calls the function around it. The rule is lexical, so linking modules changes no cost. Every other cost of C.6.4 is the same in 0.6 and 0.7. Example: a 0.6 function that holds with budget B and calls an imported 0.7 function whose body sorts an 8-element list is charged 24 more than the same call to an identical function declared in a 0.6 module.

So a 0.6 program keeps its meaning, a 0.5 program is unaffected (it has no budgets), and a 0.7 program differs from the same program declared 0.6 only in where a with budget block traps. Checked by spec/checker/tests/method_costs.rs (0.6 charges c_call alone, 0.7 charges the table, in the reference and every runtime) and spec/checker/tests/draft06_gate.rs, and the per-call-site rule by spec/checker/tests/call_site_cost.rs (0.5, 0.6 and 0.7 modules joined by use, in the reference evaluator and the Rust, Python and JavaScript emitters on the linked program); the tree-sitter port and the LALR(1) check treat 0.7 as 0.6, since the grammar is the same.

# rce-version: 0.8 declares version 0.8: the syntax, keywords, rules, evaluation and costs of 0.7, plus 5.16. It reserves no keyword, so the grammar, the LALR(1) check and the tree-sitter port treat it as 0.7. It is a version, not an extension, by the C.15 rule: the eight names of 5.16 are ordinary names in 0.7, and a 0.7 program that declares one (struct Text, struct Html) would change meaning if 5.16 applied to it. In a 0.8 module C.lit(s) costs c_call, C.encode(t) costs c_call plus the size of t (the linear class of C.6.4) and .raw() costs c_call (the text is not copied), in the reference evaluator and every runtime; the indices are erased, so nothing else in C.6 changes. A 0.5, 0.6 or 0.7 module never sees 5.16 (spec/checker/tests/indexed.rs, gate test), and modules of different versions may use each other (2.7).