Oberon RTK

ECS for Control: Round 3 Retrospective

The round-3 outlook tracked against what round 4 delivered: item by item – the schedules proven on two cores, the review written down as rules and the checker following from it, recovery and the asynchronous seam carried into the architecture round – with the round's lessons folded in.

Overview

The round-3 outlook took over two residuals – the snapshot demonstration and the checker tool – and opened or restated eight directions, the most consequential among them the step to several schedules on several cores. Round 4 – the EcsControlSchedule programs, the fourth edition of the concepts and the third of the implementation document, the schedules document, the ECS file reference, the review guide and the manual pages of two tools – took that step and proved the claim behind it, wrote the review down as the rules the checker was to support, and deliberately left the application-side directions – the temporal domain, recovery, the asynchronous seam – to the rounds that follow, by a decision taken at the round's start: architecture before application. This document goes through the outlook in its own order; what it hands forward is collected at the end, for the round-4 outlook to take over.

The outlook's items, at a glance:

Opened or carried by round 3 Verdict
the snapshot demonstration carried forward – a fourth time; recovery's inputs gathered
the checker tool delivered differently, and beyond – the review written down as rules; the tools holding what it marks
several schedules, several cores delivered beyond – two cores, a partition moved, a prescription
the temporal domain carried forward – by decision; the rates settled at the boundary
run-time errors: detection and decision carried forward, advanced – the line between contract and operation drawn at the transports
recovery on the store carried forward – the trust line's first run-time mechanism
observations, continued delivered differently – the recording moved into the adapter layer; the loop across two cores
completing the declared world delivered differently – declared kinds and recorded imports, not a manifest class
the asynchronous seam carried forward – its declaration identified as the boundary declaration
toward lib/v4.0 carried forward – the kernel consideration retired; the tools and the guide bound to the release

And, as in the round before, one axis arrived that the outlook never asked for: the program's definition as an artefact of its own, with the module kinds that make it extractable – accounted for below, beside the outlook.

The Snapshot Demonstration

Carried forward, for the fourth time – and this time by decision rather than by displacement. A decision at the round's start settled the order of the coming rounds: the architectural questions first, recovery and the asynchronous boundaries, the application rounds after them; capture, compare and restore belong to the first of those, and nothing of them was built here. What the round added is on the recovery side's input list rather than in its mechanism: the kernel's lock at Run, the first run-time form of the trust line and the line a recovery re-entry would return to (Recovery on the Store, below); and a finding from the bench that a restart without a power cycle must reckon with – hardware state survives a soft reset. The specification the previous retrospective handed over stands unchanged.

The Checker Tool

Delivered differently, and beyond. The outlook asked for a tool – smaller than it was going to be, walking the review-held legs of the invariants – and attached one question: which reviews a tool can take over. The round delivered the review, written down, and the tool followed from it.

The question could not be answered about a review that existed as a closing table in the implementation document and as the walks in its chapters. The review had to be stated first, and stating it is the step the architecture had not taken: the concepts document says what must hold, the implementation document shows what holds it in the evaluation programs, and neither states a rule over any program. The review guide does. For every invariant and every construct it says where the property is read, what must hold, what a program without it is – a violation, an observation the programmer assesses, a fact recorded for the reviewer, or a reading no tool can make – and whether a tool holds it. That is the architecture's rule set, and the two documents together describe the implemented architecture: the implementation document the constructs, the guide the rules a program built from them is read against.

Writing the rules down admitted no hand-waving and no pointing at the code. The code is one instance, and a construct's listing is not a rule; a rule says what holds for a program nobody has seen. Each check-point had to survive two questions – can a tool decide it, or only a reviewer; is a program without it non-compliant outright, or is the fact a judgement call to point out – and many did not survive as first written: rules the compiler already holds were dropped, rules were folded into one another, one was re-founded on a different operand when the program showed its stated operand was wrong. The principle that carried the work is one the round kept returning to: what cannot be written down for someone else is not known. A rule that could not be stated for any program was either not a rule or not yet understood, and the guide is the first place the architecture was put through that test for every rule it has.

Two things followed from the review's stance before any tool was touched. A check has a direction only when the program states what each module is – so every module declares its kind, SYSTEM, STATE, ADAPTER, SCHEDULE, …, in a comment before its MODULE line, naming the identifiers that play the kind's roles, its placement its directory, nothing inferred; a review by hand needs that as much as a tool does. And the imports are read against an allow-lists file, the architecture's import matrix as data, open beside the guide.

The tools follow. extract-ecs reads a built program – the linker map file is the module list, the build is verified by its own products – and writes the program's definition, the ECS file with the ECS map file beside it; check-ecs runs the extract as its first station and the check-points the guide marks as tool-held over it, every finding under the guide's identifier. The outlook's three kinds of review each have their place in the guide: the program against the architecture's rules is what the tools check; the facts the reviewer wants to look at – a module's library imports, the constants a System takes from its values module, the deployment calls – are recorded in the file and never judged; the authored agreements between parties – the bilateral contracts, the periods' arithmetic, the facts against the datasheet – are the guide's last part, read by a person only. The tools hold no rule the guide does not state; they are in beta until lib/v4.0, and the guide is a draft until it is published with the library, since its identifiers must be used before they are frozen. The discipline relies on neither.

One thing the outlook foresaw held: the tool's territory is readable off the implementation document's closing table. The two readings were compared once the guide stood: every structural invariant of the concepts document has a check-point that guards it, or rests on the reviewer with the reason stated.

Several Schedules, Several Cores

Delivered beyond. The proof the outlook called due – "the same program, cut along a declared boundary, its parts paced independently and meeting only at their transports" – is EcsControlSchedule-v29 and -v30: the one-schedule program -v26 with a second schedule created on the second core and the adaptation partition placed on it, two surfaces crossing; then the coordination partition moved as well, a third surface crossing, and schedule 1 ticking five times faster than schedule 0. The partitions are the same files in all three programs; the three differ in their program-level modules only. The claim on record since the third round – where a partition runs is a deployment decision, not an architectural one – held to the letter: creating the schedule touched one new schedule module, one new boundary module and two edited files; moving the further partition touched four program-level files and no partition file.

What it took is the schedule layer, program-level throughout: a schedule module per schedule running the station sequence for its partitions, schedule 0's module being the main program module and starting the other cores; a boundary module declaring once what crosses between which schedules, as surfaces, never as the Components behind them; the memory map declaring the number of cores; the kernel keeping a context per schedule, deriving from the boundary each schedule's view of the others – what arrives counts as produced, what leaves as consumed – so that every existing construction check falls out in both directions, and adding two cross checks after a rendezvous: no instance written on two schedules, every declared counterpart present. The schedules wait for each other twice, after planning and after committing, and never again; one timer is shared so that time stays one axis; each core ticks at its own period; one error console serves both cores, with the program's one lock behind it: a hardware spinlock that guards the error console alone, never a Component and never the program's own terminal, so that the error path stays as straightforward as it can be and gets through in whatever state the program is.

Three rules make up the whole discipline of the boundary, and they stand in the concepts document now: data crosses only through transports, named by surfaces; all depositors of a facility run on one schedule; no lock, anywhere. Beyond the proof, the round delivered what the outlook did not ask for: the schedules document, a prescription in two parts – create a schedule, move a partition – each step naming the file and the line, executed as written on the evaluation programs, with a rate test at its end.

Why it came out this way is worth stating, because it is the round's headline. The invariants carried over the core boundary unchanged, and they are what made lock-free transports sufficient: one writer per Component instance, program-wide, means every word of a crossing has one writer, so the four-slot sampling port and the single-producer ring are correct by their own proofs – plain writes and a barrier, no atomic instruction; Systems meet only in the store, and partition boundaries were transport boundaries before the second core existed; no module body touches hardware, so every module initialises on one core and each schedule creates its world on its own. The MCU-specific surface of the design is three items: the core identity read, the core-start protocol, and the spinlock behind the error console. The kernel's own cost did not move with the second core: measured with the kernel's run-time instrumentation at the 50 ms tick, a pass of schedule 0 with its nine Systems peaks at 221 µs, a pass of schedule 1 with its one System at 14 µs, and everything the step added to the kernel runs at creation or costs a context selection per pass. The counterpoint stands on record too: multi-core did not become easy; the architecture rules out the hard shapes. It holds because the model stays quasi-synchronous – communication by sampling, the latest complete value, no shared mutable state across schedules, no request-response across the cut – and the discipline is not to want them, which is the discipline the partitioned avionics architectures impose, arrived at here from the invariants.

The outlook's second box – two CPUs with no shared memory – remains the concept's claim: the schedules document places multi-MCU programs out of scope, and names the first conceptual question, one token space across several binaries.

The Temporal Domain

Carried forward, by decision: the round's order was settled at its start – the architectural rounds before the application rounds – and the temporal domain follows the architecture round on recovery and the asynchronous boundaries. What the round settled of it is the part the schedules forced, the outlook's "rate relation at every transport": once two schedules tick at different periods, a tick is no longer common currency, so every quantity counted in ticks belongs to the schedule whose tick counts it, a value crossing the boundary is denominated in the consumer's tick, a schedule's periods live in the periods module as that schedule's own, and the schedules document's rate test makes the rule checkable – change one schedule's tick and nothing else; every period re-derives to the same milliseconds and the plant behaviour does not change. The kernel's timing instrumentation supplied the round's closing measurement, the baseline the temporal round starts from. Producer rates as declared facts, deadlines and budgets, the whole-program view: untouched, as planned.

Run-Time Errors: Detection and Decision

Carried forward, advanced. The program-wide run-time error concept was not written; the round drew one of its lines, at the transports, and gathered the cases the concept will have to cover.

The line: a transport with a capacity has preconditions – a put needs room, a get needs content – and the round made meeting them the caller's obligation: the transport exports what the caller needs to meet them, asserts them once, and never clips, drops or corrects silently. The caller is the adapter, which is where the decision about a failing precondition is made – clip to what fits, drop, or record. A failed precondition is therefore a programming error and goes down the assertion path; a full buffer met by the adapter is an operational condition and becomes an observation. That is the outlook's "where an assertion is even useful" answered for one class of site – contract violations assert, operational conditions are observed – and the concepts document now says so in general form while leaving the program's run-time error handling undefined, which keeps the orthogonality the outlook demanded: the transport and the adapter fix where a condition is detected and where the decision about it is made; what it means for the impacted System falls to the error concept, which is still to come.

The cases gathered for it, from the two-core work: an error inside the error path – the deferred-report handler at the same priority as the faults it reports – is a nesting policy and a priority setting in one decision; hardware state survives a soft reset, so a restart without a power cycle needs an inventory of what to reset; a schedule whose partner never commits, or dies holding the error console, waits forever under the current stance, and whether it should is a decision; and one case from the adapters themselves – the adapter deciding and the transport asserting the same precondition is a double check on the hot path, the trust line drawn one layer too high. The question whether a System may assert stays open as the outlook left it.

Recovery on the Store

Carried forward. Nothing of capture, compare and restore was exercised, and the specification stands as the previous retrospective handed it over. The round's contribution lies on two edges the specification did not have: the re-entry line and the inventory.

The kernel now has two states, open and locked, and Run is the transition: from load until Run the station procedures accept calls and the world is created, registered, planned and committed; from Run on every one of them refuses, per schedule, and nothing after Run is entitled to configure. That is the trust line in its first run-time form – the implementation document names it one instance of a general shape, a resource open during creation and locked for steady state, with hardware lock bits, software refusal and a locked heap as the other levels – and it is the line a recovery re-entry would return to, should recovery re-run creation's later phases rather than re-value the store in steady state: world creation again, infrastructure bring-up not. Which of the two it is, the architecture round decides. The inventory is the finding from the bench: devices keep their state across a soft reset, spinlocks included, so recovery's build and acquire stations must reset explicitly what a power cycle would have reset for them. Both go forward with the specification.

Observations, Continued

Delivered differently. The outlook listed three extensions – severity, more instruments, more facilities – and the round pursued none of them as such. It moved the apparatus one layer instead.

The clip tally had lived in the library's string ring, one layer below where it belonged. The round placed every observation about a transport – a clip, a dropped put, a queue found full – in the adapter: the one place that knows both the transport's interface and the partition's store, and that detects the capacity events anyway, as a by-product of the precondition check it makes. The transport became pure mechanism, the ring buffer in its framework form; the tally became a Component of the hosting store, written on the depositor's access and attributed to the depositing System like the access itself; the distiller collects it, the supervisor reads the level. The layering is orthogonal: the transport detects, the adapter records, the System is impacted, and each varies without the other two moving.

Two things followed that the outlook could not have listed. The supervisor left the print partition for a partition of its own, so the observed facility and the System adapting to it are two partitions meeting through two transports – and in the two-schedule programs those two transports cross cores, the observation out and the command back; the loop runs identically on one core and on two, and the ports that had stood in for a boundary case now cross one. And severity turned out to need no machinery: the site that marks an event may tally its magnitude as the count's increment, so a grave event outweighs many trivial ones in the same linear account, the calibration unchanged. More instruments and more facilities remain where the outlook left them: the tick monitor deposits a report line on a slipped tick, the heartbeat is still the load player, and the print buffer is still the one facility watched.

Completing the Declared World

Delivered differently. The outlook proposed a declaration class for consultations of the locked store part, so that those reads become attributable and surveyable like the reads of the variable part, and judged the case to rest on review value alone. No manifest class was built; the round completed the declared world on another axis, and the locked consultations came along with it.

Every module declares its kind, and the ECS file records, per module, what the sources establish: the kinds and roles, the tokens and surfaces, the manifests, the adapters' store paths and directions, the crossings – and every import that is neither a program module nor a named framework module, as a fact for the reviewer. A System's consultation of a peer's locked interface is thereby visible at module granularity, as an import the allow-lists admit from any partition under one usage rule – a foreign locked part is read through its interface record only – and the cross-partition cases the outlook wanted to see in a manifest rather than a search are read off the file. The construction checks gained nothing, as the outlook predicted. Whether the per-value form pays its way beyond that is a question the round did not need to answer; it goes forward only if a program asks it.

The Asynchronous Seam

Carried forward – to the architecture round, and with its machinery identified. The outlook named the external-producer declaration as the thing to evaluate; the round built the boundary declaration for schedules, and the two are one seam: the boundary's crossings are seeded into a schedule's plan as a derived manifest, so that what arrives from elsewhere counts as produced – exactly what a hardware-paced producer would need, its productions declared as crossings into a schedule without a loop of its own. In-store hosting of the port, interrupt affinity as device ownership per schedule, and the exception priority scheme as an authored fact of the resources module are the three items beside it. The invariant stands with its footnote; the round added the device seam's kind, the binding, and the reviewer's test for what a binding may hold below the store – transfer state under a single-producer single-consumer protocol, each item consumed once, never a cache.

Toward lib/v4.0

Carried forward, with its gate re-read. The outlook made the framework step a plan: the next round delineates, and the release is staggered, the kernel's surface to survive the temporal round before any freeze. The delineation did not run this round; the schedules and the definition did. Two things about the gate changed on the way, and the outlook's sentence on the kernel is the one that stands as a dated direction rather than as the plan:

  • the kernel is no longer the reason to wait. The kernel is complete and stable for the functionality it has – the two-core round extended it without changing its shape – and what the temporal round adds to it are ordinary version bumps after a release, not a reason to hold one. The gate stays discretionary, pulled when seen fit; the kernel's surface is no longer among the considerations;

  • the release has more in it than modules. The review guide is a draft until it is published with the library; the tools are in beta until then; the allow-lists file and the kinds' reference implementations move to the library with them. The delineation names those beside the module roster.

The example's own library directory, meanwhile, grew by what two cores need – the per-schedule kernel, the error console, the locks – and was read in full once, against the design rules the round made framework-wide.

Beside the Outlook: The Definition and Its Kinds

The round's largest unplanned delivery answered a question the outlook did not ask: what a program's definition is, and where it lives. The schedules work needed one notation for programs, schedules, partitions and crossings that the tools and the documents could share; writing it down for the first program with two schedules turned it from a sketch into an artefact, and the review's stance – every module declares its kind, nothing inferred – is what made the artefact extractable from the sources rather than authored beside them.

The ECS file states the program's definition in the architecture's terms – which modules exist, of which kind, under which names they play their kind's roles, where they belong, and what the sources establish for each – and it is extracted from the sources, never authored, except where it is written to generate a skeleton from. The Oberon precedent is the module definition derived from the symbol file; the engineering precedent is the schematic read back from the layout. The file is not required to implement the architecture; it is what makes the program's structure statable in one place and comparable between versions.

The kinds are the architecture's module taxonomy, and they come from the review: a module is read against the rules of its kind, so the kind is declared where the module is. They became the documents' vocabulary: "a SYSTEM module of a PARTITION" says what no module name can. Each kind has a purpose, a placement, roles, an export rule and an import list; the schedule and boundary modules joined the taxonomy this round, as did the transports – sampling port, queueing port, ring buffer, and the plain buffer for any other library form – the adapter naming its transport, the binding at the device seam, and the plain helper. The canonical transports have reference implementations, which a generator writes from and the review compares against.

Two moves in the constructs made the kinds hold. Access procedures through adapters, in both directions: a System reaches a transport by binding the adapter's procedure into its run signature, the procedure type carrying the direction, so that the compiler holds what had been a VAR parameter's awkward claim – and so that nothing in a System, its signature or its manifest says where the producer runs, which is what made a partition schedule-agnostic by construction. And grouped store variables named by their path, the tokens mirroring the store leaf by leaf, so that the review of a manifest against a run procedure stays a line-by-line comparison.

Around them, the round made two design rules framework-wide: definition modules carry no code – a boundary module is a few assignments, and the derivation it once held is kernel code – and a module body initialises the module's own memory only, never hardware, the start-up excepted; the latter is the precondition for several schedules, every module initialising on one core and each schedule creating on its own.

Lessons

The method that produced the round, kept for the rounds after it:

  • The definition follows the code. A schedules section sketched before the two-schedule program existed was held back, and dissolved when the program did; the ECS file is extracted rather than written; and the round's documents were written concrete first – the programs and the constructs, then the concepts abstracting from what exists. The code was the thinking.

  • Squeeze to what the language gives, and refuse the compromise. The round's chain: no exported string constants, so the names tables are filled in module bodies; no multi-dimensional open arrays, so the store is grouped; a previous-value consumption is not derivable from code, so it is declaration only; a sampling port's read wants a VAR parameter, so every transport access is a procedure whose type carries its direction – and that last step is what made moving a partition to another core a four-file edit. One language feature remains unexploited, record extension, and the store is built so that it may stay unexploited.

  • The same mechanism, twice, before building it once. The boundary declaration is the external-producer declaration the asynchronous seam will need; the kernel lock is one instance of open-then-locked at every level. A mechanism that serves two foreseen cases is built for the first and recognised for the second.

  • Soundness by construction or not at all. A rendezvous claim written at installation races; written at load it precedes every gate on every core. A lock per string protects nothing; a lock per sequence, claimed and released around what must not interleave, protects the report too. The measurement rule applies to the claims: "one load per tick" was loose until the listing showed the instructions.

  • What cannot be written down is not known. A rule that could only be shown in code was not yet a rule: writing it for a program nobody has seen is the test, and the rules that failed it were dropped, folded or re-founded. The implementation document and the review guide together are the written form of the implemented architecture, and the tools are what the written form made possible, not the other way round. One consequence runs through the guide: a check has a direction only when the program states what it is, so every module declares its kind, the tools mandate the kernel and its procedure names and nothing else, naming is free, and an observation is a hint the programmer assesses, never a rejection.

  • Retire names that overpromise, and words that mislead. A specification precedes code and is never derived from it, so the file holds a definition; a form with placeholders is not a canonical form, so what a program is compared against is a reference implementation; a "world" was a container, so the thing that runs is a schedule, and a core is where it runs. The vocabulary that survives is the part of the architecture that costs nothing to enforce.

Carried into the Round-4 Outlook

  • recovery and the run-time error concept – the specification as handed over, now with the round's inputs: the line between contract violation and operational condition drawn at the transports, the nested-error policy, the device-reset inventory, the schedule with a dead or absent partner, the double check on the hot path; the snapshot demonstration, carried a fourth time;

  • the trust line at run time – the kernel lock as its first mechanism, the other levels open: which resources lock, by which means, and the inventory of what a re-entry resets;

  • the asynchronous boundaries – the interrupt-driven unit as a System of a hardware-paced schedule, the boundary declaration as its external-producer declaration, the port hosted in the store, interrupt affinity as ownership;

  • transports that can fail with perfect data – a sampling port over a noisy bus, a timeout, a failed checksum: nothing a precondition can observe, so the transport must report, and the adapter take the observation;

  • the checks still to build – the review guide's reviewer-held readings that a program may yet motivate into a tool, the generator's publication with the tools, and the multi-MCU reading of a program's singletons;

  • the application rounds behind the architecture – the temporal domain, from the closing measurement as its baseline; the observations' further instruments and facilities; and the framework step, its delineation now carrying the guide, the tools and the allow-lists beside the module roster.

See Also

Last updated: 3 November 2026