ECS for Control — Implementation Concepts
How the ECS-for-control architecture is realised in Oberon on a microcontroller: the store modules, the System modules, world creation, and the kernel.
Overview
The concepts document defines the architecture in platform-neutral terms: all state in one store, stateless Systems on a tick, declared access roles, a derived schedule, structure fixed at creation. This document shows the program elements that implement it, each with its code, drawn from EcsControlStore.
An ECS control program consists of five kinds of modules:
-
the main program – performs world creation, then hands over to the kernel;
-
the store modules –
CSandCL, holding the store, withW,I, andVsupplying their values; -
one module per System;
-
service and binding modules – device drivers, buffers, and text writers from the framework, plus the program-specific connectors to the hardware;
-
the framework modules – the kernel, kept in the example's
libdirectory, and its two supporting development-build modules.
Module names are free choices – CS, CL, W, I, V are deliberately short so the architectural modules stand out from the rest of the program; only the framework modules have fixed names.
The same holds for the idioms this document shows – the two lines by which a Run reaches the store, the form of a manifest body, the shape of a wiring line: none is prescribed, and each could be written differently. Their consistent use is what carries weight: one way of expressing each construct, within a program and across programs, gives review – by eye or by tool – a stable shape to recognise, and makes a deviation visible as information.
Throughout, each architectural rule is held at one of three levels:
-
by structure, which the compiler enforces: a module boundary, a type, an array layout, a compile-time constant;
-
by a world-creation check, where structure alone cannot reach;
-
or by review, manual or tool-assisted, over surfaces the structure is shaped to keep small – an import list, an argument list, a wiring line.
The Store Modules
The store spans two modules – both hold Components:
| Module | Role | Content |
|---|---|---|
CS |
Components State | the store's variable half: the Components the ticks advance, as one record |
CL |
Components Locked | the store's locked half: per-instance configuration as read-only records |
W |
wiring values | the deployment facts someone chose: pins, device units, handle assignments |
I |
identities | the named instance identities Systems refer to |
V |
tuning values | operational parameters: periods, rates, thresholds |
What each module may import is part of the design (utility imports such as error codes aside):
| Module | Imports | Never imports |
|---|---|---|
CS |
W (array bounds) |
CL, I, V |
CL |
W, I (the wiring pairs) |
CS, V |
W |
device modules, for named constants | CS, CL, I, V |
I, V |
nothing | – |
| a System | CS, CL, Kernel, service modules; I where it self-identifies |
W, V |
| the main program | everything | – |
The matrix is an enforcement mechanism: what a module does not import, its code cannot name. A System cannot mention a pin, a device unit, or a baud rate – the modules holding them are not in its import list. And the never column is a review surface: a System module importing W is a finding, regardless of what it does with it.
CS – Components State
CS declares the Component types as value records, a token id for each writable unit, and the variable half of the store as one record:
CONST
LedMeasuredId* = 0;
LedSetpointLeaderId* = 1;
LedSetpointFollowerId* = 2;
...
NumComponents* = 8;
TYPE
LedSetpoint* = RECORD
value*: INTEGER
END;
...
Store* = POINTER TO StoreDesc;
StoreDesc* = RECORD
(* producer: SenseSystem -> token 0 *)
(* consumers: CoupleSystem, ActuateSystem *)
ledMeasuredLeader*: ARRAY W.Leader_Num OF LedMeasured;
ledMeasuredFollower*: ARRAY W.Follower_Num OF LedMeasured;
(* producer: BlinkSystem -> token 1 *)
(* consumer: ActuateSystem *)
ledSetpointLeader*: ARRAY W.Leader_Num OF LedSetpoint;
(* producer: CoupleSystem -> token 2 *)
(* consumer: ActuateSystem *)
ledSetpointFollower*: ARRAY W.Follower_Num OF LedSetpoint;
...
END;
VAR
S*: Store;
PROCEDURE Build*;
BEGIN
NEW(S); ASSERT(S # NIL, Errors.HeapOverflow)
END Build;
Four decisions are visible in these lines.
-
Value records only. No pointer enters the store; every Component is plain data. The variable half is thereby one block of values – copyable, comparable, snapshottable whole, which is what the recovery motivation of the concepts document asks of it.
-
One record for the whole variable half. What must be captured together is declared together; a snapshot is one assignment.
-
Storeis a pointer – necessarily. An exported record variable would be read-only to every importer, Systems included, and Systems must write; read-only-to-all is the only grant the export rule has. The exported pointerScannot be re-pointed by an importer, but a local copy of it reaches the record behind it for writing – exactly the access a System'sRunneeds (next chapter). The compiler thus cannot police who writes what inCS– it would be welcome if it could – so the manifests and the kernel's checks do. -
Arrays split where the writers differ. There is no single set-point array with two Systems writing different halves; there are two arrays, one per writer – the single-writer invariant holds by construction. The attribution comments on each field group are the storage-side echo of the manifests.
Because every population is a W constant, every array is exactly its population: no partially-filled arrays, no sentinels, no capacity-versus-count distinction anywhere in the store.
CL – Components Locked
CL holds the Components that are fixed at creation: bindings to the hardware, structural references, the wiring of shared facilities.
TYPE
(* locked: SenseSystem, ActuateSystem *)
LedBinding* = RECORD
ledPin*: INTEGER
END;
(* locked: BlinkSystem, CoupleSystem *)
LedFollower* = RECORD
follows*: INTEGER
END;
...
VAR
ledBindingLeader*: ARRAY W.Leader_Num OF LedBinding;
ledBindingFollower*: ARRAY W.Follower_Num OF LedBinding;
ledFollower*: ARRAY W.Follower_Num OF LedFollower;
printWriter*: ARRAY W.Printer_Num OF PrintWriter;
...
BEGIN
ledBindingLeader[0].ledPin := W.Pin_Leader_0;
ledBindingLeader[1].ledPin := W.Pin_Leader_1;
...
ledFollower[0].follows := I.Leader_1;
ledFollower[1].follows := I.Leader_0;
printWriter[I.Printer_Heartbeat].writerHandle := W.WriterHandle_A;
printWriter[I.Printer_TickMonitor].writerHandle := W.WriterHandle_B;
...
END CL.
Here the implementation is the exact opposite of CS, for the opposite requirement:
-
Plain exported record variables. Importers can read them and never assign to them – and since no pointer type exists for these records, no alias can regain write access. The compiler's read-only is final: the lock the concepts document asks for is the export rule.
-
Populated in the module body. Oberon runs a module's body before any importing module's code – the locked half is complete before any System, and before the main program, can look.
-
One wiring line per pairing, identity on the left, resource on the right:
printWriter[I.Printer_Heartbeat].writerHandle := W.WriterHandle_A. This is where the binding modules' devices meet the store (see Bindings and Handles), and it is a review surface: each line answers who and what at a glance.
CL needs no single enclosing record: the locked half is never snapshotted – it cannot change – so its records stay separate, one per purpose.
I, W, V
Three modules of constants, deliberately not one. The separation carries meaning through the import matrix:
-
I– identities. The named instances Systems refer to:Leader_0,Printer_Heartbeat. Imports nothing. A System that participates in a shared facility importsIto know which participant it is – a compile-time constant cannot be reassigned, cannot drift, needs no initialisation order: the strongest form of "fixed at creation". -
W– wiring values. The deployment facts someone chose against a constraint: pins, device units, handle assignments – and the populations:CONST Leader_Num* = 2; Follower_Num* = 2; Printer_Num* = 2; ... UartUnit_Drain* = UART.UART1; Pin_Leader_0* = LEDbinding.LED0;
The controlled system is bounded and static – and that alone decides nothing: a program can run resource discovery over a fixed plant, taking the next available timer. The architecture prescribes the opposite: what is bounded in the world is bounded in the program text. The populations are named constants here, every collection is sized by them, and the length of an array is its population.
-
V– tuning values. Parameters changeable without structural impact:CONST TickPeriod* = 10; (* milliseconds *) (* kernel-based periods are in kernel ticks *) BlinkPeriod_0* = 400 DIV TickPeriod; HeartbeatPeriod* = 1000 DIV TickPeriod;
The kernel schedules in ticks, not milliseconds (see The Kernel); the one conversion from time to ticks happens here, visibly, where the periods are defined.
Why not all constants in one module? Because the import matrix would lose its meaning. Systems never import W or V – but a System may import I. With one constants module, the reviewer must read every use; with three, module provenance answers the question line by line: an I name is an identity, a W name is a resource – and a W name inside a System module is a finding. The split is not for the compiler, which sees only integer constants either way; it is for review.
The System Modules
One module per System. A complete one:
MODULE BlinkSystem;
IMPORT CS, Kernel;
CONST
SystemName = "Blink";
VAR
Manifest*: Kernel.Manifest;
Name*: Kernel.SystemName;
PROCEDURE runLed(VAR bc: CS.BlinkConfig; VAR sp: CS.LedSetpoint);
BEGIN
DEC(bc.ticker, Kernel.ElapsedTicks);
IF bc.ticker <= 0 THEN
sp.value := ORD((BITS(sp.value) / {0}) * {0}); (* XOR toggle 1 bit *)
INC(bc.ticker, bc.period)
END
END runLed;
PROCEDURE runSystem(VAR cfg: ARRAY OF CS.BlinkConfig; VAR setp: ARRAY OF CS.LedSetpoint);
VAR i: INTEGER;
BEGIN
i := 0;
WHILE i < LEN(setp) DO
runLed(cfg[i], setp[i]);
INC(i)
END
END runSystem;
PROCEDURE Run*;
VAR S: CS.Store;
BEGIN
S := CS.S;
runSystem(S.blinkConfig, S.ledSetpointLeader)
END Run;
BEGIN
Name := SystemName;
Manifest.C := {};
Manifest.O := {CS.BlinkConfigId};
Manifest.P := {CS.LedSetpointLeaderId};
Manifest.Cx := {};
Manifest.Px := {}
END BlinkSystem.
The Manifest
Each System declares its store access as a value record of five token sets, defined by the kernel:
Manifest* = RECORD
C*: SET; (* consumes: reads another System's product *)
O*, P*: SET; (* owns / produces: writes, single-writer *)
Cx*: SET; (* collects: reads a deposit, after all depositors *)
Px*: SET (* deposits: writes into a shared facility *)
END;
-
OandPare the single-writer classes –Ofor private state no other System reads,Pfor produced values with consumers;Cis the matching read class. -
PxandCxare the deposit classes for shared facilities – Depositors and Collectors, below.
Tokens are the constants declared in CS, one per writable unit, and a token follows the writer, not the type: LedSetpointLeaderId and LedSetpointFollowerId are two tokens over one record type, because two Systems produce set-points. How many arrays back a token is a separate, storage-level decision. A token need not even have a record type: DrainBufId marks the dataflow edge from PrintSystem to DrainSystem, whose payload lives in a service module's buffer – a pure id. The SET type bounds this implementation at 32 tokens per store – EcsControlStore uses 8 – a limit of the representation, not of the architecture: a store that outgrows it extends the manifest sets to ARRAY OF SET, and the checks remain the same set expressions, applied per word.
The manifest is populated in the System's own module body and exported read-only: the declaration travels with the code it describes, and nobody else can alter it. The main program registers it but never defines it.
Why declarations, and not introspection – metadata through which a program examines itself at run-time? Not because the environment could not provide it: Astrobe can resolve a code address to its procedure for run-time error reporting, and the same technique could carry richer metadata if a design wanted it. This design does not, on grounds the concepts document already set: introspection is run-time behaviour, machinery whose own correctness would have to be reviewed and tested – an added verification surface that runs counter to reviewable, let alone certifiable, control-system design – and it would only surface, at run-time, facts about the closed world that are defined and fixed at design time.
A manifest is values, not behaviour. For the same reason, nothing is generated: the declarations are ordinary source, written and reviewed like all the rest.
Run and runSystem
The pair at the bottom of BlinkSystem is the idiom that connects a System to the store:
-
runSystemcarries the law, and its signature repeats the manifest in compiler-enforceable form: written Components asVARparameters, read Components as value parameters – which for records and arrays Oberon passes by reference but treats as read-only.PrintSystemreads the deposits it collects, so its signature saysprintb: ARRAY OF CS.PrintBuf– noVAR; an assignment to it would not compile. -
Run*adapts between the kernel's parameterless call and the typed signature. It takes the one local copy ofCS.Sand passes store fields as arguments – the only place the System touches the store variable itself.
The division is what makes the access reviewable. runSystem's parameter list is checked against the manifest: one VAR parameter per O/P/Px token, one value parameter per C/Cx token. Run's argument list is checked against the field attributions in CS. Both surfaces are a handful of lines, and both are exactly the kind of correspondence a checker tool can verify mechanically.
One access deliberately does not go through the signature: the locked half. HeartbeatSystem's law reads its wiring directly – and, through the handles found there, drives its service modules:
PROCEDURE runSystem(VAR hbs: CS.HeartbeatStatus; VAR pbs: ARRAY OF CS.PrintBuf);
VAR now, delta, writerHandle: INTEGER;
BEGIN
writerHandle := CL.printWriter[I.Printer_Heartbeat].writerHandle;
PrintBuffers.Reset(CL.printBuf[I.Printer_Heartbeat].devHandle);
TIMER.GetTimeL(CL.timerBinding.devHandle, now);
...
Uniformity would suggest passing the CL records as parameters too, read-only like any consumed Component. Two things decide against it. The signature's job is to enforce what the compiler otherwise would not – and for CL the compiler already enforces everything: the export rule makes every access read-only, parameter or not, so a CL parameter would duplicate an existing guarantee. And parameters are a bounded resource – an open array costs two words (address and length), a record two as well (address and type tag) – best spent where the modes carry meaning: on the store's variable half.
A practical decision, then, at no cost to the rules. What remains for review is the import list – CL and I there announce exactly this kind of access – and the I-indexed lines themselves, each one reading as a self-identification. (The slot write this System's pbs parameter leads to is the subject of Depositors and Collectors, below.)
Inside runSystem, iteration bounds come from the parameters themselves – LEN(setp) – never from imported size constants: in the bounded domain, length is population, and the law needs no other size.
The Main Program
The main program module assembles the world and hands over to the kernel. Its body is the whole program start sequence:
BEGIN
build;
attest;
acquire;
value;
propagate;
Kernel.Install(V.TickPeriod);
addSystems;
Kernel.Plan;
PlanView.Report(Console.Werr[Console.SYSTERM0]);
Kernel.Commit;
Kernel.Run
END EcsControlStoreV11.
Before any of it runs, the framework's start-up has already brought the infrastructure up – importing the framework module Main first places the program start-up ahead of everything – the first sub-phase of the concepts document. (Main is the framework's start-up module, its name mandatory – not to be confused with the main program module, whose name is free.)
The procedure names and their scopes are programmer-selected – what the concepts document fixes is each sub-phase's contract; what stands here is a proven idiom, one local procedure per sub-phase, called in order:
-
build– constructs everything:CS.Buildallocates the store; devices are allocated and initialised (NEWvisibly in the main program – the caller allocates); the binding modules configure the hardware. Contract: acquire can run. -
attest– not a concepts-document sub-phase but an added consistency check: every device reference wired inCLmust resolve to a constructed, bound device.ASSERT(UART.Bound(CL.uartBinding.devHandle), Errors.ConsCheck); ASSERT(TIMER.Bound(CL.timerBinding.devHandle), Errors.ConsCheck); ...
A wiring line that promises a device the build did not deliver fails here, at creation, where failure is allowed.
-
acquire– gives every measured Component its starting point; here, by sampling:WHILE i < LEN(CL.ledBindingLeader) DO LEDbinding.Get(CL.ledBindingLeader[i].ledPin, S.ledMeasuredLeader[i].value); INC(i) END;
-
value– sets every remaining Component, explicitly, field by field. Nothing zeroes memory at load in Oberon, and nothing needs to: the zeroth consistency point demands designed values, and automatic zeroing would not deliver one – it would only make a missed initialisation read like data. Where zero is the designed value, the assignment says so. -
propagate– writes the store's commanded values out, so the hardware's initial state is derived from the store, never stated independently:WHILE i < LEN(CL.ledBindingLeader) DO LEDbinding.Put(CL.ledBindingLeader[i].ledPin, S.ledSetpointLeader[i].value); INC(i) END;
The kernel calls that follow – install, register, plan, commit, run – are the kernel's chapter.
Depositors and Collectors
The Systems seen so far form chains: a producer, its consumers, an order between them. Shared facilities have a different shape – several Systems each contribute a piece, and the whole is read across. In EcsControlStore the facility is terminal output: several Systems print, one System moves the text toward the UART.
The deposit classes carry this shape. The facility has one token – PrintBufId – and one slot per participant; the slot arrays in CS and the wiring in CL are indexed by the participants' identities from I.
A depositor – HeartbeatSystem – declares the token in Px and writes its own slot:
PROCEDURE runSystem(VAR hbs: CS.HeartbeatStatus; VAR pbs: ARRAY OF CS.PrintBuf);
VAR now, delta, writerHandle: INTEGER;
BEGIN
writerHandle := CL.printWriter[I.Printer_Heartbeat].writerHandle;
PrintBuffers.Reset(CL.printBuf[I.Printer_Heartbeat].devHandle);
...
Texts.WriteString(writerHandle, SystemName);
...
INC(pbs[I.Printer_Heartbeat].seq)
END runSystem;
Manifest.C := {};
Manifest.O := {CS.HeartbeatStatusId};
Manifest.P := {};
Manifest.Cx := {};
Manifest.Px := {CS.PrintBufId}
Everything the depositor needs, it reaches by its own identity: which slot to write, which writer and buffer to print through – one I constant, resolved against CL's wiring. Single-writer per instance holds untouched: each participant writes only its own slot.
A collector – PrintSystem – declares the token in Cx and iterates all slots:
PROCEDURE runSystem(printb: ARRAY OF CS.PrintBuf; VAR printc: ARRAY OF CS.PrintCursor);
VAR
drainHandle: INTEGER;
buf: ARRAY PrintBuffers.BufSize OF CHAR; numChar, i, id: INTEGER;
BEGIN
drainHandle := CL.drainBuf.devHandle;
id := 0;
WHILE id < LEN(printb) DO
IF printb[id].seq # printc[id].seqDone THEN
PrintBuffers.GetString(CL.printBuf[id].devHandle, buf, numChar);
i := 0;
WHILE ~DrainBuffers.Full(drainHandle) & (i < numChar) DO
DrainBuffers.Put(drainHandle, buf[i]); INC(i)
END;
printc[id].seqDone := printb[id].seq
END;
INC(id)
END
END runSystem;
The derived order places every collector after every depositor of the token. At least one collector must exist; any number may – collectors multiply as consumers do; this program has one.
A token is dataflow (O/P, read via C) or deposit (Px, read via Cx), never both – the kernel rejects reading a deposit through C, or a product through Cx, as a class conflict. What the deposit classes buy is linearity: one token per facility, however many participants – not one per participant-collector pair.
Adding a participant is one I constant, one W handle set, its CL wiring lines, and the participant's own module. The collector does not change: it iterates an array whose length is the population.
Bindings and Handles
Binding modules are the program-specific connectors to the hardware. They use the framework's device records and drivers in general, and may reach hardware registers directly where that is all that is needed – whatever the program requires: UARTbinding configures pins and the UART device; LEDbinding writes GPIO pins.
PROCEDURE Config*(uartHandle, txPinNo, rxPinNo, baudrate: INTEGER);
VAR uartCfg: UART.DeviceCfg;
BEGIN
cfgPins(txPinNo, rxPinNo);
UART.GetBaseCfg(uartCfg);
uartCfg.fifoEn := UART.Enabled;
UART.Configure(uartHandle, uartCfg, baudrate);
UART.Enable(uartHandle)
END Config;
Handles are how the store refers to devices without holding pointers – and "device" covers more than hardware: the UART and the timer are devices, but so are the print buffers, the drain buffer, and the text writers – virtual, software-only devices, handled identically. The store – CS and CL both – contains values and handles only; the device records, the pointers, the working state behind them form the technical state, and each service module owns the table for its own devices, hardware or virtual, indexed by handle. There is no central device table: the main program constructs the devices at world creation, and each module resolves its own handles thereafter.
The UART that drains the terminal output shows the whole chain:
(* W: the choices -- a handle, a unit, the pins *)
UartHandle_Drain* = 0;
UartUnit_Drain* = UART.UART1;
Pin_DrainUartTx* = 4;
Pin_DrainUartRx* = 5;
(* CL body: the handle assigned to the binding Component *)
uartBinding.devHandle := W.UartHandle_Drain;
(* main program, build: device constructed, bound to the handle, configured *)
NEW(uartDev); ASSERT(uartDev # NIL, Errors.HeapOverflow);
UART.Init(uartDev, W.UartHandle_Drain, W.UartUnit_Drain);
UARTbinding.Config(CL.uartBinding.devHandle, W.Pin_DrainUartTx, W.Pin_DrainUartRx, V.DrainBaudrate);
(* main program, attest: the wiring verified *)
ASSERT(UART.Bound(CL.uartBinding.devHandle), Errors.ConsCheck);
From then on, a System reads the handle from CL and passes it to the driver's procedures; the pointer behind it never leaves the driver module. The pay-off is the two-state split of the concepts document, in code: the store stays plain copyable data across its whole extent, and what a handle resolves to is the technical side's business – re-establishable behind an unchanged handle.
The Kernel
The kernel is a framework module – fixed name, kept in the example's lib directory, about 250 lines. It does four things: registers Systems, checks the manifests, derives the schedule, runs the tick loop. All its state is exported read-only; it prints nothing and does not know a terminal exists.
Registration
The main program registers each System – procedure, manifest, period in ticks (0 = every tick), name:
Kernel.AddSystem(BlinkSystem.Run, BlinkSystem.Manifest, 0, BlinkSystem.Name);
Kernel.AddSystem(PrintSystem.Run, PrintSystem.Manifest, 0, PrintSystem.Name);
...
Kernel.AddSystem(HeartbeatSystem.Run, HeartbeatSystem.Manifest, V.HeartbeatPeriod, HeartbeatSystem.Name);
The order of these calls is explicitly meaningless – the schedule comes from the manifests. The manifest is passed by value and copied: the kernel never reaches back into a System module.
Plan and Commit
Plan gathers all manifests and does the whole structural verification – and it never faults. Every check is evaluated, every violation recorded with its offending tokens; then the dependency edges are derived – a producer's P against a consumer's C, a depositor's Px against a collector's Cx – and the Systems are topologically sorted into the run order. A cycle is recorded like any other violation, not trapped.
The checks are set expressions:
| Check | Rule |
|---|---|
| single writer | no token in two Systems' O/P |
| class agreement | a token is dataflow (O/P, read via C) or deposit (Px, read via Cx), never mixed |
| owned is private | no O token in any C |
| no self-loop | no System consumes a token it writes – reading one's own written Component is implicit in write access |
| produced is consumed | every P token has a consumer |
| consumed is produced | every C (Cx) token has its producer (depositors) |
| deposits are collected | every Px token has at least one collector |
| acyclic | the dependency graph has no cycle |
Each looks like this in the code:
(* collectors per deposit token: min one *)
IF allPx - allCx # {} THEN
INCL(Failed, ChkNoCollector);
Offend[ChkNoCollector] := allPx - allCx
END;
Commit is the gate – the entire procedure:
PROCEDURE Commit*;
BEGIN
ASSERT(planned, Errors.ProgError);
ASSERT(Failed - Relaxed = {}, Errors.PlanCheck)
END Commit;
In a deployed program a rejected plan is a hard fault with its own error code – a static construction fault, never retryable – handled by the run-time error machinery like any other.
Development Builds
Development builds insert, they never restructure. Between Plan and Commit, a development-build main program adds one call: PlanView.Report reads the kernel's exported results and prints them – every manifest, the dependency matrix, the derived order, every violation by name – to the same console the run-time error output uses. Because Plan collects everything before Commit gates, a broken program reports all its violations in one run, before the fault.
The full report for EcsControlStore:
Kernel.Plan
manifests (registration order):
0 Blink
O:
BlinkConfig
P:
LedSetpoint Leader
1 Couple
C:
LedMeasured
P:
LedSetpoint Follower
2 Actuate
C:
LedMeasured
LedSetpoint Leader
LedSetpoint Follower
3 Drain
C:
DrainBuf
4 TickMonitor
Px:
PrintBuf
5 Print
O:
PrintCursor
P:
DrainBuf
Cx:
PrintBuf
6 Sense
P:
LedMeasured
7 Heartbeat
O:
HeartbeatStatus
Px:
PrintBuf
dependencies (registration order):
0 Blink
1 Couple
Sense
2 Actuate
Blink
Couple
Sense
3 Drain
Print
4 TickMonitor
5 Print
TickMonitor
Heartbeat
6 Sense
7 Heartbeat
derived scheduling order:
0 Blink
1 TickMonitor
2 Sense
3 Couple
4 Actuate
5 Heartbeat
6 Print
7 Drain
plan checks: all pass
Two supporting modules serve this, both development-only imports: PlanView, the reporter, and TokenNames, a name table indexed by the token constants – unnamed tokens degrade to their numbers, so the table may lag the program without ever invalidating it.
One more development aid: the three coverage checks – unproduced, unconsumed, uncollected, exactly those whose relaxation only widens what is accepted – can be waived, so a producer can be tested before its consumer exists:
Kernel.Relax({Kernel.ChkUnconsumed});
The structural checks cannot be waived, by construction: Relax masks its argument against the relaxable set. The deployed main program omits the report call, the Relax call, and the development imports; Plan and Commit appear identically in both builds.
The Tick
Steady state is one loop: sleep until the tick, then run every System once, in the derived order, to completion – the cooperative run-to-completion of the concepts document, realised here. That this program runs one schedule on one core is a deployment fact, not a concept; within one schedule, nothing needs a lock, and nothing has one.
The tick is counted, not flagged. The SysTick handler does exactly one thing:
PROCEDURE* sysTickHandler[0];
BEGIN
INC(TickCount)
END sysTickHandler;
The loop compares the counter against its own cursor; the difference is the number of ticks the pass represents – one, normally; more, when a pass overran its period. The hardware's own tick flag saturates and cannot distinguish one elapsed tick from several; the counter can, so overruns are detected and counted. The policy is slip and count: the pass runs once, periodic tickers advance by the full elapsed count so their long-run cadence holds, and the missed ticks are recorded.
Periods are counts of ticks – a period in milliseconds would promise a resolution the tick machinery cannot deliver; a period in ticks is exact, constant, and honoured. The one time-to-ticks conversion sits in V, where the periods are defined.
The counters – total ticks, missed ticks, the current pass's elapsed count – are exported read-only: the kernel is a sensed device. Whether missed ticks stay merely visible or become control data is a System's decision, not the kernel's – in EcsControlStore, a monitor System samples them and deposits a report like any other participant of the print facility. Every cooperatively scheduled program owes its reader an answer to "what happens when a tick is missed"; this is the answer here: nothing blocks, nothing replays, the slip is counted, and the record is available to any System that cares to look.
Holding the Invariants
The following table lists what holds the concepts document's rules – collected, invariant by invariant. The left column is the concepts document's list of structural invariants; the other two say at which of the three levels the implementation holds each, and by what. Most rules are held at more than one level – the compiler and the reviewer meet at the Run seam – and two are not exercised by this program at all, which the table says rather than hides.
| Invariant | Held by | Mechanism |
|---|---|---|
| All state is in Components; a System holds none | review | a System module's only variables are Manifest and Name, written once at start; all working state arrives as runSystem parameters |
| Every Component instance has exactly one writer, and the run order is derived | structure + check + review | arrays split per writer; Plan: single writer, class agreement, acyclic; Commit gates; runSystem modes (VAR = written) bind code to manifest at the Run seam |
| A shared facility has one slot per participant and at least one collector | structure + check | slot indexed by the participant's own I constant; Plan: deposits are collected; derived order: collectors after depositors |
| Systems meet only in the store | structure + review | no System imports another System – what is not imported cannot be named; the import list is one glance |
| A System runs to completion | structure + review | the kernel offers no yield to call; no waiting loop in a law – a review item, a spin has no fixed count |
| The store holds values and handles, never machinery | structure + review | CS/CL records are value types and INTEGER handles; no pointer type appears in any Component; the pointers sit in service-module tables |
| On the synchronous control path, the HAL is stateless and passive | review | UARTdrain shows the form: status read fresh, guarded write, no module variables, called and never calling – the conditions are visible in a screenful |
| Asynchronous units are not Systems | not exercised | this program drives all hardware synchronously; for the seam and its rules in working code, the round-1 programs drive the terminal output synchronously, asynchronously, and as a hybrid in turn |
| Partitions stay private and meet only in interface stores | not exercised | one store, one schedule – partitioning begins with a second |
| Structure is fixed at creation; steady state changes values | structure + review | every NEW sits in the main program's build; registration ends at Commit; no construction call is reachable from a law |
The two operational invariants are verified rather than held: the infrastructure by the framework start-up, before the main program's body runs; the interface hardware by attest – every wired reference resolves to a bound device – and by the sampling acquire, which doubles as the live check. Their supervision in steady state arrives as Components, the monitoring subject of the next round.
See Also
- ECS for Control — Concepts
- EcsControlStore
- ECS for Control — Round 2 Lessons Learned
- ECS for Control — Round 1 Retrospective
- ECS for Control — Round 2 Outlook
Last updated: 29 July 2026