scheduling.md

Scheduling policies, choice points and exploration

How the runtime resolves what the Kernel Semantic Library leaves unordered, how it reports each such resolution without changing the run, how a driver asks for another one, and how every one within a bound is enumerated. The behavior a user sees is in the guide; which openings are the library's and which are the tool's is derived case by case in the semantic oracle.

The problem this answers

A succession is a HappensBefore link between whole occurrences (Occurrences.kerml); the library orders nothing two such chains do not connect. Fork branches, the reactions of sibling regions to one event, two enabled transitions out of one state, several holding guards of one decision, and two performances due at one instant of the clock are all unordered, so one model admits several complete outcomes and every one of them conforms. The executor runs exactly one linearization. Until that linearization is named and reported, a conformance case can only pin it, and a test that pins it cannot tell an admissible alternative from an executor bug.

The design separates four things that were one: the set of outcomes a case admits, the linearization a run took, the points at which it had a choice, and the rule it chose by.

Choice points (choice.go, action_choice.go)

A ChoicePoint is one point where an executor had several enabled alternatives the library leaves unordered and took one by its scheduling rule. ChoiceKind names the twelve:

Kind	Where it is noted	Alternatives, canonically
ChoiceTokenOrder	ActionExecutor.noteTokenOrder	the tokens that could act in the step, by ID; the one stepped first is taken
ChoiceDecisionBranch	ActionExecutor.noteDecisionBranches	the successions whose guards hold, by declaration position
ChoiceWriteOrder	stepWriteLedger.noteChoices	the tokens that wrote one feature in one step; the write that stood is taken
ChoiceTransition	StateExecutor.chooseTransition; pickBranch (state_route.go)	the transitions one event enables out of one state, by declaration position; or the branches of a choice or junction pseudostate enabled when its guards are read, labelled choice <name> or junction <name>
ChoiceRegionOrder	dispatchInOrder, drawn on the front of state_unit_front.go (on <event>); chooseDoAction (do round at t=…); fireJoinIncoming (join <name>)	the next unit — a source's exit, a segment's effect, a target's entry — of each firing one occurrence selected across regions, by source in declaration order; the one performed first is taken, and the entries and exits a firing nests are drawn on its front — likewise the states whose do behaviors are due in one round, and the sources of the transitions into a join that fires
ChoiceEntryOrder	enterRegionsInto (entering <state>), enterForkBranches (fork <name>), a history's restore	the next entry unit of each region, branch or restored region of a composite state, in declaration order; the one performed first is taken. A unit performing no behavior rides with the performing unit beside it
ChoiceEntryStep	StateExecutor.entryStep (entry at t=…)	a free dispatch due at the instant, followed by the held entry cascades that can resume; the free dispatch is listed first and the selected alternative is taken
ChoiceExitOrder	exitState (exiting <state>)	the next exit unit of each region a state leaves, innermost first within a region, in declaration order; the one performed first is taken
ChoiceStepOrder	StateExecutor.chooseStepOrder	the move of a due do behavior and a dispatch due beside it; the one that goes first is taken
ChoiceStatementOrder	stmtEngine.pickStatement (statements in <body>)	the statements of one body that no succession or control structure orders and that may run next (lower.StatementOrder), by declaration position; the one run first is taken
ChoiceDueOrder	Context.runDue (advance.go); the checker's run, one executor holding the turn until it has no move at the instant	the executors due at one instant, in creation order; the one run first is taken
ChoiceDispatchOrder	StateExecutor.nextEvent, when the queue leaves several events unordered at its head	the events due at one instant the library does not order — time triggers with each other, a time trigger with a pool event of the same timestamp — labelled as the queue labels them; the one dispatched first is taken. A completion event goes before any of them and pool events keep their arrival order (earlierFirstIncomingTransferSort), so neither is a choice

Two rules hold at every site:

• Recording a choice never alters the run. The executor resolves the point exactly as the policy says and then describes what it resolved. To know a decision had a second holding guard, every guard is evaluated, not just up to the first that holds; a later guard that cannot be evaluated is recorded as an UnevaluableGuard, not a failure — a guard with no result is not true, so its succession is simply not selected, which is the library's reading. A first guard that errors still fails the run as it always did.
• A choice is a fact about the run, not a fault in the model. ChoicePoint.Diagnostic() is informational with code choice-point; UnevaluableGuard.Diagnostic() is informational with code guard-unevaluable. Both are RunNotes.

Context.note appends a note to the run's runState.notes and, when tracing, writes its String() to the trace at the point it was made (choice …, unevaluable guard …). A probe — a preview of what a run would do, bracketed by beginProbe — notes nothing, since it is not a run. Context.Notes, Choices and UnevaluableGuards read them back; the executors' Notes and NoteCount let a caller driving a run call by call see what one call noted, which is how the REPL ends %step, %continue and %advance with a count; NotesSince reads the notes past such a mark without copying the ones before it.

Region order is drawn per dispatch, not per event: dispatchInOrder draws among the candidates still active before each firing, since a reaction may leave a sibling's leaf, and both the broadcast of a queued event and the polling of change triggers (state_change_trigger.go) go through it. The choice is labelled by the occurrence dispatched, not by the trigger of whichever region was drawn first, so the label is the same under every policy.

An entry-step choice is recorded as entry at t=<instant> when a state entry cascade has been held by a non-default run-to-completion scope and a dispatch is due at the same clock instant. The alternatives list the free dispatch first, when one exists, followed by the held entries that can resume. A dispatch whose transition owner lies within a held scope is not offered as free; tied events are filtered to the free alternatives, and a dispatch with no free alternative does not appear. Fixed policies select the first alternative, so they dispatch before a held entry when that dispatch is free. Exploration snapshots the entry boundary and enumerates each alternative; replay parses the entry at t= location and applies the recorded pick. Once the selected dispatch or held entry settles, ordinary transition, region-entry and exit choice points continue as usual.

A choice pseudostate's branch is drawn on arrival: resolveChoice reads its guards once the incoming segments' effects have run, so which branches are enabled can depend on those effects, and with two or more enabled the draw is a ChoiceTransition at choice <name> that explore enumerates and a seed replays (TestExploreDynamicChoiceBranches). A junction's guards are read statically, when the transition is selected — against the data as it stands before the incoming effect — and with two or more enabled the draw is likewise a ChoiceTransition at junction <name>, made and recorded only as the transition fires (settleDraws), after the region order among several candidates and after the transition's own guard is read again: a candidate another region's reaction disarms draws nothing, and no branch guard is read again: the route beyond each enabled branch — through any further junction — is settled with the transition, so the branch drawn is taken along it though another region's effect since changed what those guards read (TestExploreStaticJunctionBranches, TestExploreJunctionDrawnAsTransitionFires, state_junction_guards_read_once, state_junction_beyond_a_draw_read_once). A history's default transition through such a junction draws and records the same way (TestExploreHistoryDefaultThroughJunction).

One thing that looks like an opening is determined and is never recorded. A composite state's completion: once its do behavior and every one of its regions have ended, its nil-trigger transitions are queued as completion events at the current instant, ordered as a leaf's are, and the machine ends only when its own top-level regions are all at done (completeIfDone → scheduleCompletedComposites).

Repeated action-step performances

When a node declares an exact count greater than one, the arriving action token is split into sibling tokens, one per performance. They use the existing ChoiceTokenOrder choice point: no new scheduling policy is introduced, and declared, reverse, seeded, replayed and explored runs continue to select among the same steppable tokens. Each token begins a fresh frame for the node, so its local features are independent, while writes to features of the owning action remain shared. Data flows, bindings and connections involving a repeated node's pins are refused.

The owner frame holds a per-node completion barrier. A repeated performance that finishes retires its token without taking the node's outgoing successions or delivering its data flows. The last one to finish releases the barrier and advances the node once, so every target follows every source performance and the owner continues once. A nested flow runs separately inside each performance's frame. Repetition identity and the live barrier are part of snapshots, held images and the execution state key; otherwise replay and exploration could merge states with different remaining performances.

A count of zero passes through without beginning a performance, trace events or data flows. It is only order-safe at a flow boundary: a zero-count step between two real steps leaves their order open and is refused. Any step count that is not fixed, or succession, guard, control-node or pin interaction the multiplicity checker cannot support, is refused before the node runs. The two-reading treatment of unwritten succession ends is documented in the semantic oracle.

Leaf action-body interleavings

A leaf action body — a node's initial feature values and its direct statements, with no flow of its own — runs through the statement engine (usageWork.perform, stmtEngine). Its performance encloses separate times the semantic oracle derives: the start shot, where attribute t : Integer := c snapshots c, and one subperformance per statement, an assign writing when it ends. Another performance may run between any two.

• Atomic units. One initialization (every initial value of the body, read at its start shot) and one statement are each one move: an assignment reads its value and writes it with no boundary between, since the library places nothing between them. A loop iteration is one move; a step of a flow the body drives is one move unless its own body divides, as a token of the outer flow's does, so the repeated performances of a counted step in a loop or branch body and the branches of a fork there interleave as they do at the top level.
• Scheduler boundaries. Where a body divides, the run yields after its start shot and after each statement (Context.bodyPerformed, Context.yieldBody, bodyPause.yielded): the token goes back to the step's steppable tokens with its body frame held, and the next pick among them is an ordinary ChoiceTokenOrder. No new choice kind is added, so a witness, a replay file, a snapshot and a held image name a body boundary as they name any token move, and the body frame is resumed where it paused.
• Where a body divides. lower.BodyDivides lists a body's moves (its start shot, then each statement, a conditional's guard by itself and a loop counted twice) with their footprints (Footprint, the reduction's), and the footprints of every node of the outermost flow and its nested flows; the node's own, with its per-performance pins removed, when it may run beside itself. When the flow can hold two tokens at once and two or more of the body's moves are dependent on one of those footprints, the body divides. With at most one, every interleaving inside the body only reorders independent moves, so the body stays one move and the state space does not grow.
• Guards. An if's guard is evaluated before its branch (IfThenPerformance), so a dividing body yields between them (Context.guardPerformed); the branch taken is kept in its branchFrame across the pause. A state's do body yields there only under one-move schedules, so reverse, declared and seeded runs keep their state traces.
• Do bodies stating a flow. A for, while or if node of a do body's stated flow yields after each iteration and branch statement, as the same statement in a statement-list body does (bodyRun.nodesYield); the flow counts the node's yield as a move (ActionExecutor.yieldedIn), so adding then takes no interleaving away. A token of a flow such a node drives moves only through that node's work, never as a move of the outer flow (Token.drivenUnder), so a replayed witness meets the same choices it recorded.
• Callees in executors of their own. An action a step is typed by, or a body performs, runs in its own ActionExecutor, outside the graph BodyDivides reads. When the body or flow driving it goes one move at a time, the callee's start shot is a boundary (Context.startShotMove), its own bodies divide where two of their moves may touch what they do not hold (lower.BodySharesMoves), and its flow pauses after each move when two of its moves may (lower.FlowSharesMoves, Context.tokenStepBody); the attributes and in parameters the callee's definition declares are its performance's own, not shared, while each write to an output reaches the caller's pin and its streaming flows as it is made, so outputs are shared. A pause inside a body-driven token propagates to the body driving it. A seeded run whose step holds another token pauses there when drawYield says so (Context.drawsTokenSteps), so seeds reach those outcomes too.
• Executors on one clock. Separate executors — object behaviors, state machines, actions started together — still interleave by whole turns: the executor the due order draws runs until it has no move at the instant (Context.runDue, invocationRun.turn). Their moves within one instant are not interleaved, which spec compliance records as approximate.
• Ordered and unordered statements. A succession inside a nested flow orders its steps, so no boundary reorders them; a boundary lets only another performance in. The direct statements of one body that no succession or control structure orders are unordered (derivation). lower.StatementOrder lists, before each statement runs, those that may run next: a statement then links waits for the one before it, a local declaration, return or perform keeps its place, and two orders that only swap adjacent independent statements (by the reduction's footprints) are one. Two or more candidates are a ChoiceStatementOrder (stmtEngine.pickStatement); a compound statement already started yields at its inner boundaries so a dependent sibling may run between them. declared and reverse run a nested body's statements first to last as before, and an action definition's own statements in the token order each policy already gave them (reverse last to first), so their results do not move; explore, the checker, replay and seeds choose. A terminate action usage's implicit terminate is one of its body's statements in this sense. explore enumerates without partial-order reduction, so a body of many dependent unordered statements may exhaust its run budget, which it reports as incomplete.
• Policies. explore, replay and the checker step one move at a time and yield at every boundary of a dividing body. reverse and declared never yield, so a body runs whole as before and their results do not change. A seeded run whose step holds another token yields at a boundary when scheduler.drawYield — a hash of the seed, the token's ID and the boundary's ordinal — says so. That draw does not consume the generator the run's picks come from, so one seed still reproduces one run.
• Checker and SMT. The checker's moves are the executor's, so it reaches every interleaving exploration does, under its reduction and state merging; a paused body frame is part of the state it keys. The SMT encoding performs a body as one move and refuses a flow whose body divides (Flow.checkBodyInterleaving, UnsupportedError construct body interleaving), so it reports such a flow as not covered rather than encoding one order.

Policies (scheduler.go)

A SchedulePolicy is parsed from one spelling and printed back to it:

Spelling	Token order in a step	pick (branch, transition, region)	pickDue
reverse (default, zero value)	reverse spawn order	first in declaration order	last created
declared	spawn order	first in declaration order	first created
seed:<n>	shuffle of the tokens not parked; a dividing body yields where the seed's hash says	uniform draw	uniform draw
replay:<file>	the witness's step n: … line, then reverse's pick alone	the witness's line, then reverse	the witness's line, then reverse
explore[:runs=N,depth=D]	the exploration's plan	the exploration's plan	the exploration's plan

reverse is exactly what every run did before policies existed, so every .expected.json and .trace.golden recorded before them still holds unchanged; that is the invariant the whole design is built to keep. Under reverse and declared a region-order pick is declaration order and is still reported — a fixed policy resolves the choice, it does not remove it — and so are the entry-order and exit-order draws, one choice line per draw in the trace golden of a fixture entering or leaving a state of two or more regions, its event order unchanged (region-order scheduling). One order the fixed policies take is not yet a recorded choice: a due do step against the dispatch at the head of the pool, drawn per token move of the do flow in that note's design.

SchedulePolicy.start begins the resolutions of one run as a scheduler. A seeded one carries a math/rand/v2 PCG the run consumes draw by draw, so the same seed replays the same run on every platform; scheduler.mark saves and restores that state around a probe, so previewing does not move the generator. Context.SetSchedule sets the policy runs started from then on draw under; a run already under way keeps the one it started with, and explore is refused with ErrExploreUndriven because it is not a policy one context runs under (below). Context.Reschedule is the same change reaching the runs driven call by call too — the clock's and those of the behaviors the objects run — each given a scheduler started under the new policy where it stands, so a persistent session's turns from then on choose as a fresh run would; a snapshot restores the schedulers the runs had along with their marks.

The scheduler lives in the run's runState beside the budget and the notes. A run driven call by call — a REPL %action or %state session — owns its executorRun.state, installed for each call by beginExecutorRun whatever ran in between, so a seeded debugging session draws from its own generator and an interleaved run neither consumes its draws nor inherits its notes.

replay:<file> (replay.go) is the policy a witness is run again under: the file's choice lines — ChoiceTaken.String spellings, one per line up to the first blank line, so a checker's witness file with a trace body after its header serves as it stands — are followed one move at a time, each having to name the step the run is at and pick among the alternatives it offers, and once they are spent the run picks as reverse does, still one token a step — the witness was written by a run stepping so, and a sweep letting every token act would leave another trace. A line the run cannot follow, or one left over at the end, is recorded as the run goes and reported by Context.Unfollowed as a ReplayError naming the move, its choice and what the run faced; the run is never quietly turned into another linearization. A refused move changes nothing: a transition draw is refused before the dispatch fires (broadcastEvent), and a choice pseudostate's, drawn only once the compound transition's exits and incoming effects are made, or a join's, drawn one incoming segment at a time, undoes that move whole — exits, effects, the do behaviors the exits abandoned, what was traced and noted (moveWhole marks the move with a moveMark, kept or undone by the refusal; marks nest, a choice on the way out of a join handing the do behaviors it ended to the join's). The model checkers replay every sat witness under it before claiming a violation.

Exploration (explore.go)

explore enumerates every linearization within a budget by replaying whole runs, each from a fresh Context:

1. The first run records each choice point it reaches as an exploreSlot (a pick among n alternatives, or which of the tokens able to act a step tries next) and takes the first alternative at each.
2. unexplored leaves one prefix per slot the run owns with an untried alternative — the record up to that slot with the alternative advanced — and a later run replays the prefix and takes first alternatives past it. The queue (explore_queue.go) runs the prefixes in plan order: those departing from the first run at one choice before any departing at two, and among them the earliest choice varied first. So the first run's choice points are each varied once, from the first, before any is varied twice: a choice met early with a long tail of choices behind it is varied by the second run, not after every order of the tail, and a runs budget of one more than the first run's choice points varies each of them at least once.
3. A replay that does not meet the choice points its prefix planned — a different number of alternatives, or tokens able to act the plan did not find so — is ErrExplorationDiverged, and no outcome set is reported, since one could not be trusted.
4. Runs stop when every alternative within depth is tried, or when the runs budget is reached; a slot resolved past the depth budget takes its first alternative and is not the exploration's to vary, so a choice point deeper than depth is never varied however many runs remain. Either bound reached makes the Exploration incomplete, and Exploration.Status says which; nothing is silently truncated. The default budget is DefaultExploreBudget, 1024 runs and 64 choice points per run; a witness lists every choice point its run met, so its length sizes depth.

A fresh context per run is what makes replay sound: instances, identities, the message bus, the clock, object behaviors, calc memoization and the notes of one run cannot leak into the next. Context.beginExploration installs the exploration's run as the scheduler every choice draws from; scheduler.describe attaches the ChoicePoint the run reports to the slot it just resolved, so a witness names alternatives exactly as the trace does.

Outcomes are keyed by Outcome.identity — outputs, finalState, state visits, or the error — and grouped: each distinct outcome reports how many linearizations reached it and the choices of the first run that did, its witness. A step's pick among tokens that then did not act is no alternative (the slot is narrowed, and a run that repeats one already made is not counted twice). Explore is the one driver of this policy; the CLI's -schedule explore, the wire schedule field and the Python client all reach it, and a REPL debugging session refuses it because it steps one run and cannot replay from the start.

A root executor creation failure, or a pure structural start check that fails before any root model behavior runs, is a SetupError: it fails the exploration and produces no outcome. Errors from entry behaviors, entry guards, state entry actions, do-behaviors, completion, or later model behavior are runtime error outcomes, even when they occur during initialization; FailedLinearizations counts the runs represented by error outcomes. A complete exploration containing any such failure is observed, not proved. Action-step-multiplicity refusals occur when the step is reached, so they are runtime error outcomes, never a SetupError.

Outcome probabilities describe only the model's weighted draws. A run records a trie of choice prefixes; weighted nodes sum their children with normalized model weights, while scheduling nodes take the minimum and maximum over their explored alternatives. An unexplored scheduling alternative contributes zero to the minimum; an unexplored weighted alternative contributes zero to its sum. The root vectors give each outcome's ProbabilityRange, computed in O(depth × outcomes) vector space before outcomes are sorted. A probability is absent if no committed run made a weighted pick, and an incomplete exploration has lower bounds only when it did. Random-function draws still come from the model seed and are not enumerated, so these probabilities are conditional on those draws. Checker Violation.Mass is a separate measure, the path mass a check reports per violation.

The conformance contract

Every element above has a test surface, documented for authors in internal/exec/runtime/testdata/conformance/README.md and summarised in testing:

• A case whose model admits several results lists them under outcomes with an admissible citation into the semantic oracle; a case with one result states it as before. The observed run must match exactly one listed outcome.
• TestExecutionConformance runs every case under the default policy. TestExecutionConformanceUnderPolicies runs the whole suite under declared and seed:1: a case with no schedule pin was recorded under the default and must hold under any policy, so one that differs has been pinning a scheduling artefact and fails rather than being skipped. OPENSYSML_SCHEDULE_SEEDS=<n>,<m>,… widens that sweep to further seeds for a local or scheduled run; seed:1 stays in every run so a sweep is never opted out of.
• A case with outcomes is also explored (exploreConformanceCase): exploration must reach every listed outcome, reach nothing unlisted, and complete within the case's exploreBudget. A case without outcomes is not explored, on the expectation that it has one reachable outcome; when exploring it shows more, the fix is to derive its admissible set in the oracle and list it, not to pin the policy. A schedule pin of reverse says the case's result is one linearization, kept only until its admissible set is derived or the bug it pins is fixed.
• TestExecutionTrace checks a case's .trace.golden under the default policy and, for a case with outcomes, a <case>.<policy>.trace.golden under each sweep policy; a .trace.order states the partial order — a < b per line — a trace must respect, checked beside the golden or instead of one, and TestTraceOrderViolationFails proves a violated constraint fails.
• explore_test.go covers the enumeration itself: every outcome reached once, determinism, the one-run case with no choice points, each budget's incompleteness, an error as an outcome, a decision in a loop, transition conflict, sibling region order under every policy, and due order.

What this is not

This is bounded enumeration of linearizations, not model checking: bounded model checking proposes snapshots at choice points and partial-order reduction so that only one representative of each equivalence class of interleavings is run. Exploration runs every linearization within budget and reports the distinct outcomes it reached; it answers "which outcomes can this model produce, and by what choices" and reports honestly when the budget stopped it, which is the question the conformance harness asks. The reduction, the deadlock and requirement analyses across schedules, and the exploration of value domains remain that proposal's.