feat(runtime): select the scheduling policy a run resolves its choice points under - #125
Merged
Conversation
Contributor
Author
🤖 Devin AI EngineerI'll be helping with this pull request! Here's what you should know: ✅ I will automatically:
Note: I can only respond to comments from users who have write access to this repository. ⚙️ Control Options:
|
devin-ai-integration
Bot
force-pushed
the
feature/scheduling-policy
branch
from
September 8, 2026 14:26
64c24cc to
06a46f2
Compare
devin-ai-integration
Bot
force-pushed
the
feature/scheduling-policy
branch
from
September 8, 2026 18:40
743f14b to
3a2f5c8
Compare
… points under A run follows a named scheduling policy wherever the library orders nothing: `reverse` (the default, unchanged: reverse token order, first holding guard, first enabled transition), `declared` (spawn and declaration order) or `seed:<n>` (a PCG sequence the seed fixes, reproducible on every platform). Every choice point is still reported and each `took ...` is what the policy took. `explore` is reserved and refused by name until it exists. The same spelling is taken by `sysml -schedule`, `%schedule` in the REPL (a debugging session under way keeps its own), a `schedule` field on ExecuteActionRequest, ExecuteStateRequest and RunAnalysisRequest advertised as the `schedule` capability (a spelling naming no policy is INVALID_ARGUMENT), the Go and Python clients, and a `schedule` pin on a conformance case. The conformance suite runs whole under `declared` and `seed:1` as well, requiring every case that pins no policy and lists no outcomes to produce its default outputs; policy trace goldens pin every outcomes case. The two cases whose default result is one linearization of several pin `reverse`. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
… non-cryptographic Co-Authored-By: jason.han <hanhuijun@gmail.com>
…olicies may reach different ones Co-Authored-By: jason.han <hanhuijun@gmail.com>
Restate action_choice_shared_message_accept as an outcomes case derived in the semantic oracle, with a .trace.order and declared/seed-1 trace goldens, in place of its reverse pin. send_identity_same_named_ports stays pinned: the via-less accept over-matches a port-addressed transfer, fixed separately. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…scheduler A decision branch the policy picks past the first was read only in a probe the context undoes, so its evaluation left nothing behind. The run now reads the picked guard once more before taking the branch, as fireTransition reads a transition's guard again before it fires; the seed:1 trace golden of action_choice_decision_overlapping_guards gains that reading. An executor driven call by call (the REPL debuggers) keeps the scheduler its run started with: another run driven to completion while it is paused no longer replaces the sequence its remaining choices draw from. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
… dispatch selectCandidates remembers per source state which transition it offers, so a composite state reached from every leaf of its orthogonal regions is asked once per event dispatch or change poll: the choice among its enabled transitions draws once, yields one candidate and one choice note, and the run's next choice takes the seed's next draw. Nested transitions keep their priority. The state_choice_shared_ancestor_regions trace goldens lose the second leaf's redundant re-reading of the first guard. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…t resolution An enclosing state's enabled transitions were chosen, and the seeded draw spent, before losesToNestedTransition dropped the candidate to a nested transition, so a choice that never fired and was never reported shifted every later seeded choice. Candidate discovery now returns the enabled positions and chooseTransition picks among them after conflict resolution, on both the dispatch and the change-poll path; a shared ancestor still draws once. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…n example Co-Authored-By: jason.han <hanhuijun@gmail.com>
Decide read the scheduler the context happened to hold, so after another run had used the context it could name a transition other than the one ProcessNextEvent then fired. It now previews under the executor's own scheduler, drawing nothing from it. Co-Authored-By: jason.han <hanhuijun@gmail.com>
… act A token parked at a join its other branches have not reached, or at an accept no message in flight answers, keeps its place in the step's order, so steps taken while tokens wait do not shift the choices the run makes later. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A malformed spelling is INVALID_ARGUMENT whether or not the service offers verification, as it is on ExecuteAction and ExecuteState. Co-Authored-By: jason.han <hanhuijun@gmail.com>
With a via-less state accept routed by the receiver a transfer reaches, the case has one enabled transition under every policy and needs no schedule pin. Co-Authored-By: jason.han <hanhuijun@gmail.com>
devin-ai-integration
Bot
force-pushed
the
feature/scheduling-policy
branch
from
September 8, 2026 19:56
7195386 to
098d5b8
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
The action and state executors already report a choice point wherever the Kernel Semantic Library orders nothing — several steppable tokens in one
Step(), several holding guards at a decision node, several enabled transitions out of one state for one event, two tokens writing one feature in one step — but they always resolved it the same way, so the tool could not tell a scheduling artefact from a bug. This PR makes the policy the run resolves those choices under selectable, with the same spelling on every surface, without changing the default result of a single existing model.internal/core/runtime/scheduler.go:SchedulePolicy+ParseSchedulePolicywith the policiesreverse(the default: reverse token-index order, first holding guard, first enabled transition),declared(spawn/declaration order) andseed:<n>(scheduler-localmath/rand/v2PCG; token order by shuffle, alternatives byIntN; guard probes save and restore the generator so previews consume no choice).Context.SetSchedule/Schedule(); an executor already running keeps the policy it started under.scheduleTokens(Step and nested flows inaction_subflow.go),stepDecisionNode, transition selection instate_executor.goandstate_change_trigger.go, same-step write order — and the recordedtook …and theTakenindex are what the policy took. Ancestor-priority transitions are still ordered by UML/SysML and are not a choice.stepDecisionNodereads it once more for real before the token travels, so the chosen branch's effects are the run's and its reading is in the trace; a picked transition's guard was already read again byfireTransition/ the change-event poll as it fires.selectCandidatesremembers the answer per source state), so the choice among its enabled transitions draws once, yields one candidate and onetook …, and the run's next choice takes the seed's next draw. A leaf whose own state offers a transition still never reaches the ancestor, so nested transitions keep their priority. Discovery and pick are separate steps:enabledTransitions/risenChangeTransitionsreturn the enabled positions, andchooseTransitionconsults the scheduler only for a candidatelosesToNestedTransitionhas kept, so a composite state a nested transition outranks — never fired, never reported — draws nothing and does not shift the seeded choices after it.Step,ProcessNextEvent,RunDoRound,PollChangeEvents— the REPL debuggers) keep their own scheduler for their whole run:beginExecutorRuninstalls the run's scheduler for each top-level call and restores the previous one afterwards, so a pausedseed:<n>run resumes its own sequence after another run under any policy has used the sameContext. Nested executions (subflows, object behaviours) still share the outer run's scheduler.Decidepreviews under that same scheduler (previewExecutorRun), so the transition it names is the oneProcessNextEventthen fires, and the preview puts the draw back.ActionExecutor.parked, from the readinessbeginStepOrderalready records), so steps taken while tokens wait — a debugger stepping a parked action, an idle poll — draw nothing and do not shift the choices the run makes once the messages arrive.reverseanddeclaredare unaffected.RunAnalysisreadsschedulebefore requiring the verification capability, asExecuteAction/ExecuteStatehave no earlier gate: a malformed spelling isINVALID_ARGUMENTon a service withholding verification too, a valid one there is stillUNIMPLEMENTEDfor verification, and a non-empty spelling on a service withholdingschedulestaysUNIMPLEMENTEDfor that (TestAnUnknownScheduleIsInvalidArgumentWithoutVerification).exploreis not implemented here:ParseSchedulePolicy("explore")is a typed error saying bounded exploration is not available yet, and the docs/changelog say so. Nothing else in this PR presumes its shape.sysml -schedule <policy>for-action,-stateand-analysis(-calcaccepts the flag but a calc's body performs nothing, so it has no choice to make); REPL%schedule [<policy>](show / set for later runs; a%action/%statesession under way keeps its own); wire fieldschedule(string) onExecuteActionRequest(4),ExecuteStateRequest(4) andRunAnalysisRequest(6), empty = default, refused asINVALID_ARGUMENTbefore anything runs, advertised as theschedulecapability.Diagnostic.code(4) and thediagnostic_codescapability come frommainand sit beside it; a scheduled run's choice-point diagnostics carry"code":"choice-point"like every other.make proto). Handwritten surfaces: Goopensysml.WithSchedule(...)onExecuteAction/ExecuteStateandopensysml.Schedule(...)AnalysisOption,CapabilitySchedule; Pythonschedule=onexecute_action/execute_state/run_analysiswith capability preflight,CAPABILITY_SCHEDULE; JavaCapabilities.SCHEDULE; NodeCAPABILITY_SCHEDULE. Node and Rust have no handwritten execution wrappers, so only the capability surface and its tests changed there..expected.jsonmay carry"schedule": "<policy>"and the harness runs it under that policy (README documents it).Cases the default suite had been pinning to one linearization
TestExecutionConformanceUnderPoliciesruns the whole suite underdeclaredandseed:1; every case without a pin must produce its default outputs. Two did not (nothing is skipped; an unpinned case that differs makes the sweep fail loudly):reverse)declaredseed:1action_choice_shared_message_accept(twoaccepts racing for two sends)a = 2, b = 1(1 choice point)a = 1, b = 2(2 choice points)a = 1, b = 2(2 choice points);seed:2,seed:3givea = 2, b = 1send_identity_same_named_ports(SendIdentity::alpha), before the accept-routing fix onmainfinalState = received, visitsstart, waiting, receivedfinalState = strayed, visitsstart, waiting, strayedaction_choice_shared_message_acceptis a genuine multi-outcome model: it now lists both pairings asoutcomes, citing the new section “Two accepts of one type racing for two sends: each takes one message, which one is open” indocs/project/behavior-semantic-oracle.md(the transfers'HappensBeforelinks order each send before the accept that takes its transfer and nothing orders one accept before the other), carries a.trace.orderfor the order the library does fix (splitbefore the sender and both accepts,sendOne < sendTwo,sync < recorder < done; the join's predecessors are not stated because a token parks at a join before it performs), and hasdeclared/seed-1trace goldens like the otheroutcomescases. Its default.trace.goldenis unchanged.send_identity_same_named_portswas pinned toreversebecause the via-lessaccept Pingover-matched a transfer addressed toalpha.inPort.mainnow routes a via-less state accept by the receiver the transfer reaches, sowaitinghas one enabled transition under every policy; the pin is gone and the case runs unpinned in the sweep. The newaccept_port_addressed_via_onlyandaccept_part_addressed_receiver_onlycases, and everyperformerscase the trace harness now runs per performer, produce the same outputs and the same trace underdeclaredandseed:1as under the default (none has a choice point).Policy-specific trace goldens (
<case>.declared.trace.golden,<case>.seed-1.trace.golden) exist only for the cases that carryoutcomes, andTestExecutionTracechecks them.Specification basis
The Kernel Semantic Library orders performances only where a⚠️ approximate, because
HappensBeforelink joins them (Occurrences.kerml;Actions::DecisionActionpicks exactly one outgoingHappensBeforeLink, SysML v2 §7.17.3 rule 2; aStateTransitionPerformance'stransitionLinkisHappensBefore[0..1],StatePerformances.kerml), so which linearization a run takes where nothing orders it is tool-defined. The policy names that choice instead of hard-coding one; ancestor-priority transitions are ordered by UML/SysML and stay out of the choice set. No existing row moves;docs/project/spec-compliance.mdgains a row for the scheduler under the choice-point rows (exploredoes not exist yet), anddocs/guide/06-behavior.mdgains the paragraph next to the choice-point paragraph.How it was verified
Default behaviour: the whole suite under the default produces its recorded outputs — no
.expected.jsonchanges but theoutcomesrestatement and thereversepin above, plus the new policy goldens — and one default trace golden moved:state_choice_shared_ancestor_regions.trace.golden(and itsdeclaredandseed-1goldens) lose one reading of the guardlevel > 5: the second leaf of the parallel state used to askworkfor its transition again, re-reading the first guard and — underseed:<n>— drawing again for the same choice. The case's own oracle comment says the choice out ofworkis made once and reported once; the trace now shows the readings that selection actually needs (the first guard once, the picked transition's guard once more as it fires). Final state, visits and outputs are unchanged.One policy golden moved:
action_choice_decision_overlapping_guards.seed-1.trace.goldennow shows thealarmguard (level > 70) read a second time in step 1, between the preview of both guards andchoice step 2: … took 2->alarm. That is the real reading of the picked branch described above; before it the run travelled a branch whose guard had only ever been evaluated in a rolled-back probe.New tests:
internal/core/runtime/scheduler_test.go— parsing (reverse,declared,seed:<n>, empty), typed errors forseed,seed:,seed:-1,seed:abc, unknown names, whitespace/case variants,explore; reverse/declared ordering; same seed ⇒ same trace, different seeds may differ; guard probes leave the generator untouched; atook …under each policy names the alternative actually taken;TestPickedGuardIsReadByTheRun(over sixteen seeds, the run's trace contains the later guard's reading exactly when that guard was taken);TestDrivenRunKeepsItsSchedulerAcrossOtherRuns(a seeded run stepped once, interrupted by a wholedeclaredrun on the sameContext, then stepped to completion produces the same trace as the same run driven alone);TestSharedAncestorChoiceDrawsOnce(a parallel state with two enabled transitions out of it, reached from both regions, by event dispatch and by change poll: over sixteen seeds the run reports two transition choices whoseTakenare the seed's first and second draws — on the previous revision seven seeds per path took a shifted second choice);TestOutrankedChoiceDrawsNothing(an enclosing state with two enabled transitions loses to a nested one, by event dispatch and by change poll, ahead of two observable choices: over sixteen seeds those two take the seed's first two draws — on the previous revision the outranked state's hidden draw shifted the first of them);TestDecidePredictsTheDrivenRunsTransition(a seeded machine with two transitions enabled by one signal, after a whole run of the same machine on the sameContext: over sixteen seedsDecidetwice names the same transition andProcessNextEventfires it — on the previous revision eleven seeds named the other one);TestParkedTokensDrawNothing(two accepts parked in parallel branches, then two messages and a run to completion: over sixteen seeds the two token-order choices take the same alternatives whether or not five idle steps were taken while parked — on the previous revision fifteen seeds took another one).TestExecutionConformanceUnderPolicies(suite underdeclaredandseed:1), policy trace goldens intrace_test.go.cmd/sysml/run_test.go(-scheduleon every execution flag, invalid spellings),internal/repl/schedule_test.go(show/set, later-runs-only, running debugger keeps its policy),internal/grpc/schedule_test.go+capability_test.go(field applied, reproducible,INVALID_ARGUMENT, capability advertised),client/opensysml/schedule*_test.go,clients/python/tests/test_schedule.py, Node and Rust capability tests, JavaApiIntegrationTestcapability assertion, conformance scenarios01-server-info.json(capability) and06-behavior.json(scheduleon the wire, in-process and over every transport).Gates (after rebasing onto current
main):Generated code is
make protoon the rebased tree; a secondmake protochanges nothing. Clients: Gogo test ./client/...against the locally builtsysml-grpc; Pythonpytest831 passed / 3 skipped against it; Nodetypecheck,lint,test(112 pass); Rustcargo test -p opensysml(all ok, 16 in the client integration suite,OPENSYSML_GRPC_BINARYpointing at the local build). The Java suite could not be run here — Maven could not fetchjacoco-maven-pluginoffline and stalled online — soApiIntegrationTestrelies on CI.By hand, on the CLI, the REPL, the Python client against a local service, and raw gRPC / Connect JSON, byte-compared with
origin/mainfor the default andreverse:reverseoutput identical to main across seven ordering-sensitive action fixtures, a performed-part instantiation, an analysis, a timed state machine and a scalar calc; no panic or hang under any policy.declared/seed:<n>change the linearization where the model admits one (action_choice_shared_message_accept:a=1,b=2underdeclaredandseed:1;state_choice_transition_conflict:seed:3settles inhigh), eachtook …matching the send/accept that actually ran; three repeated runs per seed are byte-identical.seed,seed:,seed:-1,seed:abc,seed:1.5, casing/whitespace variants, unknown names) is refused before the model loads on the CLI, leaves the REPL policy unchanged, and isINVALID_ARGUMENT/ HTTP 400invalid_argumenton gRPC and Connect for all three requests; concurrent mixed-policy requests stay isolated.%actiondebugging session keeps the policy it started under after%schedulechanges it; the next run takes the new one.Checklist
make testandmake lintpass locallychanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build)F4,K5) in the body, docs, or changelog