ECS for Control: Implementation

How the ECS-for-control architecture is realised in Oberon on a microcontroller: definition and store modules, tokens, Systems, ports and adapters, world creation, and the kernel.

Overview

The concepts document defines the architecture in platform-neutral terms. The invariants, listed at the bottom of the concepts document, are rules that an implementation of the architecture must follow.

This document shows the program constructs developed so far to implement the architecture with Oberon and the Astrobe compiler and linker for the RP2350. The constructs presented below are drawn from the latest evaluation and test program EcsControlWatch.

Discipline

Oberon is a general-purpose programming language, with no specific support for any architecture. It is an excellent substrate, providing many of the features required and useful, but only the combination of defined constructs and a discipline for building a program using them can get us to the point where we can profit from the language properties. This holds for any architecture.

The constructs and the discipline for our architecture have been developed starting from humble code experiments to what is described in this document, from exploring basic feasibility to maximally exploiting language features. This often meant to ruthlessly simplify, by relentlessly probing and asking what the actual essence of the architecture's invariants is, and how to express this in constructs supported by the language as directly as possible. However, no invariant has been sacrificed or weakened due to limitations of language support.

Naturally, this still results in constructs that cannot be fully checked and enforced by the compiler. The architectural invariants demand much more than that. Some constructs, and what they express, can be gated at start-up of the program during world creation, but there will always be the need for review to bridge the gap between what the invariants demand, and what can be expressed by the language. Furthermore, review will always be required for how the facts of the controlled system, as well as of the run-time substrate of the control system – its infrastructure – are represented in the program.

The discipline is the practice: employing the constructs, consistently, program after program. The constructs enforce nothing by their mere existence – the discipline comes first, and everything else is built on it.

This document consistently uses module names and idioms – the form of a token module, the two lines by which a Run reaches the store, the shape of a wiring line: however, 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.

Enforcement

The constructs have evolved to support the different tiers of enforcement as directly as possible. The tiers are not alternatives of equal rank: each matter is held at the strongest tier that can reach it. They also order in time: the language binds at every compile, the gate at every program start, review at every change.

Language

The language enforces it, in two ways: the compiler rejects at compile time – a type, a parameter mode, an export mark, a module boundary – and the language's defined semantics guarantee behaviour, such as module bodies running before any importer's code.

The compiler enforces Oberon, not the architecture: its grip on an invariant exists exactly where a construct placed the matter within the language's reach – a named type in a signature, a value-mode parameter, an unexported field. Language-tier enforcement is manufactured – the concepts document's "claim everything the compiler can enforce", enacted: each such construct converts a review obligation into a language guarantee.

The two ways combine with one authored absence: an exported variable, populated in its module's body, in a module that exports no procedures, is written once at load and closed thereafter – read-only to every importer by the export rule, immutable with no means to alter it anymore.

Gate

The program does not pass into steady state unless creation succeeded – all of it. The gate has three stations, in creation's own order:

• the start-up sequence: loading and initialising every module, in dependency order. The framework's start-up brings up the infrastructure, asserting as it goes; bodies of modules that export immutable (locked) values as variables assign the values, and fire the architecture-level assertions written into them: a token back-check, a calibration that does not validate. A failed body never reaches the main program's;

• world creation: the partitions' creation code, every assertion at its fact's authority – an allocation that fails, a device that cannot answer where acquire samples one – failing in the phase where failure is allowed and handled;

• Plan and Commit: the store access declarations verified against each other, the derived order established, Commit refusing a violated world – the gate's final station.

Passage through all three licenses the switch to steady state, and any closing that comes with it – a run of configuration lock calls, a locked heap. The tier binds once, at creation, and never runs on the hot path.

For contradictions among declarations, the verification is complete: a second writer, a dependency cycle, an uncollected deposit cannot hide. What no check can see is fidelity – whether the declarations state what the code does: a System that writes a store variable while declaring nothing contradicts nobody, and the kernel sees a consistent world that happens not to be this program.

Review

Reading the sources, manual or tool-assisted. Fidelity is review's territory by necessity, not as a fallback; the constructs are shaped to make the reading a mechanical, line-by-line comparison rather than a reconstruction of intent – verbatim token names, every store access named once in Run, parameter modes mirroring the manifest, one idiom per construct – and the same shaping is what makes it tool-supportable.

One class of review is stronger than the walk: absences. What a module must not do – import a System, hold a working variable, allocate outside creation – is verified exhaustively, by a search that finds nothing: a zero-hit result concludes, where presence-conformance can only compare line by line.

The Relations

Read as verification, the tiers check different relations: the language checks the code against its rules; the gate tests the declarations against each other; review reads the code against the declarations, and the authored facts against reality – the plant, the chip resources, the board – the one side no program artifact can stand in for. Each relation is checkable only because the constructs shaped the program for it: fact authority, for one, is what makes a unit readable against its datasheet.

Constructs Contribute to Invariants

The constructs presented in this document are software architecture elements and Oberon idioms – module kinds, store shapes, tokens, manifests, access idioms. A construct is not a rule; it contributes to implementing invariants. The discipline describes how to use the constructs.

No construct alone implements an invariant: each invariant is carried by several constructs together, and one construct can contribute to several invariants. Also, some constructs lay groundwork for others.

Each chapter closes by naming the invariants its constructs contribute to, and how; the chapter Holding the Invariants collects the whole map.

Program Modules

Kinds

A program based on the architecture consists of different kinds of modules:

• the main program module – brings up the infrastructure, sequences the partitions' world creation and hands over to the kernel;

• partition modules – create the partitions' worlds, and register their Systems (via the main program);

• System modules – implement one System: the Run procedure, the manifest to declare the store access attributions;

• store modules – both the locked (CL) and the variable state (CS) parts;

• port and adapter modules – interactions and communication between partitions as needed;

• hardware binding modules – the program-specific access modules to the underlying hardware as needed;

• definition modules – the values defining structures, tuning, resources, periods, and store tokens;

• framework and library modules – program-agnostic modules, ie. re-usable across different programs; this includes the RTK framework modules, as well as the programmer's own. Some RTK modules are specific to the architecture, such as the kernel, some are generic.

Names

The module names used in this document have proven to be useful. This includes the suffix naming (CSprint, Wblink, Tcoord), which encodes a module's family and partition in the name; within a partition, its own modules are imported under the bare family letters (CS := CSprint), foreign ones with a partition initial (Tp := Tprint) – every use site then carries its provenance.

But: all module names – apart from the RTK framework modules – are free choices, as is the aliasing used in import lists.

The Definition Modules

Overview

Every partition authors its own definitions; two modules are program-level because their facts are:

R and P are program-level by the consult-scope criterion: a chip resource is arbitrated program-wide, and the periods pace the one schedule, which spans the partitions. Two boundaries keep the split clean: W holds no chip facts, and R holds no cardinalities. A pin lives in R, expressed in the owning module's vocabulary (fact authority); a population lives in the partition that creates that world.

The constructs of this chapter contribute to the following invariants:

• every fact has one authority;
• structure is fixed at creation; steady state changes values.

How each contribution works closes the chapter; the chapter also lays groundwork – the wiring facts feed the store shapes. The import discipline binding all module kinds, definition modules included, is collected in a chapter of its own (The Import Matrix, below).

Constructs

MODULE R;

  CONST
    (* library module handles *)
    (* Texts *)
    WriterHandle_Term* = 0;
    (* UART; note: handle 1 is used by console *)
    UartHandle_Drain* = 0;

    (* chip peripherals *)
    UartUnit_Drain* = UART.UART1;

    (* chip pins *)
    Pin_DrainUartTx* = 4;
    Pin_DrainUartRx* = 5;

    Pin_LedLeader0* = LEDbinding.LED0;
    Pin_LedLeader1* = LEDbinding.LED2;

END R.

UartUnit_Drain* = UART.UART1 and Pin_LedLeader0* = LEDbinding.LED0 are fact authority in code: the value is written in the vocabulary of the module that owns it. Every constant here names an authored choice – which unit on the chip drives the drain link (UartUnit_Drain), which pin carries its TX (Pin_DrainUartTx* = 4) – and every choice is made, never found: there is no "next free" UART device slot; the RP2350 has unit 0 and unit 1, and R selects. A name that would assert a choice nobody has – an index that is pure position, with no role behind it – does not appear; such a value stays a literal at its use site.

Two of R's kinds are allocations in shared spaces – a handle, a unit: their referent is the space's other claimants, and false means a collision or an out-of-range claim – a writer handle already held by the console faults the program. Allocations are held accordingly: derived where derivable (the token bases, Tokens), asserted where the space is owned (the creation checks), reviewed where a co-claimant must be known – the sheet's "handle 1 is used by console", one comment long.

A partition's W is correspondingly small – pure structure:

MODULE Wprint;

  CONST
    PrintBuf_Num* = 1;
    PrintBuf_Size* = 128;

    DrainPeriod_Num* = 3; (* number of drain system periods available *)

    Ix_PrintBuf_Term* = 0; (* index of the buffer used for the terminal *)

END Wprint.

Ix_PrintBuf_Term is a role-binding index – which instance plays a role, remappable, so the name survives its value. And where a peer's structure must follow a fact, the peer authors its own copy: Wcoord.Periods_Num* = 2 tracks the number of leaders authored in Wblink, each side commented with its counterpart – the follower doctrine of the concepts document, in two lines that must be edited together, deliberately.

Contributions to Invariants

• Every fact has one authority. This chapter is the invariant's home. Each definition module is an authority, placed where its facts are consulted: W for the partition's structure, V for its tuning, R for the program's resource choices, P for its periods. Within each, fact authority sets the vocabulary – a value is written in the owning module's terms, readable against its source – every fact is authored, never discovered, and every name asserts an authored choice. Across partitions, agreement is the follower twins': authored copies, commented with their counterparts, verified at composition and never propagated.

• Structure is fixed at creation; steady state changes values. The earliest fixity lives here: cardinalities and role-binding indices are compile-time constants, settled before creation runs at all; the store shapes they size cannot drift afterwards.

• Groundwork. W's cardinalities size the named array types and anchor the follower twins (CS – Components State); V authors what the V-to-CL derivation consumes (CL – Components Locked); the token definitions Tx and Tbase have a chapter of their own (Tokens).

CS – Components State

Overview

Each partition's Component store spans two modules: CSx holds the variable part, and CLx the locked part (see next chapter).

The constructs of this chapter contribute to the following invariants:

• all state is in Components;
• every Component instance has exactly one writer;
• the store holds values and handles, never references to data via pointers or addresses;
• structure is fixed at creation; steady state changes values.

How each contribution works closes the chapter; it also lays groundwork – the store vocabulary, the named array types, and the hosting of transports.

Constructs

MODULE CSblink;

  IMPORT W := Wblink, Errors;

  TYPE
    LedMeasuredArray* = ARRAY W.LedRole_Num OF INTEGER;
    LedSetpointArray* = ARRAY W.LedRole_Num OF INTEGER;
    BlinkTickerArray* = ARRAY W.LedRole_Num OF INTEGER;

    Store* = POINTER TO StoreDesc;
    StoreDesc* = RECORD
      ledMeasuredLeader*: LedMeasuredArray;
      ledMeasuredFollower*: LedMeasuredArray;
      ledSetpointLeader*: LedSetpointArray;
      ledSetpointFollower*: LedSetpointArray;
      blinkTicker*: BlinkTickerArray
    END;

  VAR
    S*: Store;

  PROCEDURE Build*;
  BEGIN
    NEW(S); ASSERT(S # NIL, Errors.HeapOverflow)
  END Build;

END CSblink.

The record StoreDesc gives the vocabulary its sharp form, compatible with the concepts document:

• the Components are that document's instances – for a population, the array elements: ledSetpointLeader holds one set-point Component per LED role, and these are what a System iterates;

• the store variable is the field of the store record – the unit above the Components: a single Component (drainRun in CSprint, below) or a whole population of them;

• the store variable is the discipline's unit: tokens, manifests, and the kernel's checks speak in store variables – never in types, never in single array elements.

Five properties are visible in these lines:

• Value records only. No pointer enters the store; every Component is plain data. The variable part is thereby one block of values – copyable, comparable, snapshottable whole.

• One record for the whole variable part. What must be captured together is declared together; a snapshot is one assignment.

• Store is a pointer – necessarily. An exported value record variable is read-only to every importer, Systems included, and Systems must write. Exporting the pointer S opens the write path: access directly via S is still read-only, but a local copy of S reaches the record behind it for writing.

• Arrays split where the writers differ. The leader and follower set-points are two arrays, one per writing System: the storage layout follows the writers.

• Every population array has a named type. LedSetpointArray is declared once and used both in the store and in System signatures (The System Modules, below).

The blink store above is all run state. Where a partition hosts transports, they are ordinary store fields – hosted means in the store, exactly as the concepts document says. CSprint carries the partition's run state and the three transports it hosts, the print buffers, the observation ports, and the drain command port:

MODULE CSprint;

  IMPORT W := Wprint, Errors, Observations, PrintBuffers, ObservationPorts, DrainCmdPorts;

  TYPE
    DrainRun* = RECORD
      ticker*: INTEGER
    END;

    AdaptRun* = RECORD
      drainPeriodCmd*: INTEGER;
      opsAtCmd*: INTEGER
    END;

    PrintBuf* = RECORD
      buf*: ARRAY W.PrintBuf_Size OF CHAR;
      state*: PrintBuffers.State
    END;

    PbBufArray* = ARRAY W.PrintBuf_Num OF PrintBuf;
    PbClipsTallyArray* = ARRAY W.PrintBuf_Num OF Observations.Tally;
    PbClipsObsPortArray* = ARRAY W.PrintBuf_Num OF ObservationPorts.Port;
    PbClipsAcctArray* = ARRAY W.PrintBuf_Num OF Observations.Account;

    Store* = POINTER TO StoreDesc;
    StoreDesc* = RECORD
      drainRun*: DrainRun;
      adaptRun*: AdaptRun;
      pbBuf*: PbBufArray;
      pbClipsTally*: PbClipsTallyArray;
      pbClipsObsPort*: PbClipsObsPortArray;
      pbClipsAcct*: PbClipsAcctArray;
      drainCmdPort*: DrainCmdPorts.Port
    END;

  VAR
    S*: Store;

  PROCEDURE Build*;
  BEGIN
    NEW(S); ASSERT(S # NIL, Errors.HeapOverflow)
  END Build;

END CSprint.

Which System reads or writes which Component or array of Components is not defined and visible in the store: each System's access to the store's variables is defined in its manifest, spoken in the token vocabulary of the next chapter, and held by review against the System's Run procedure (The System Modules, below).

Contributions to Invariants

• All state is in Components. The store records are the invariant's substrate, not a guard on it: "in Components" means in these records – CS holds the variable share, CL (next chapter) the locked one. What stays outside is exactly what the concepts document exempts: technical state behind handles, below the store. One capability rides along: one record for the whole variable part, so a snapshot is one assignment.

• Every Component instance has exactly one writer. The declaration of StoreDesc aligns storage with authorship: single writing becomes declarable per store variable; where two populations of one type have two writers, they are two store variables. Stated per Component in the concepts document, the invariant is thereby checked per store variable: coarser, and therefore stronger. Systems declare their access roles in their manifests using tokens that represent the store variables (Tokens), and their code is bound to the named types at their Run seam (The System Modules). All store variables must be declared with a named type, which cannot be an alias for a base type.

• The store holds values and handles, never references to data via pointers or addresses. A review ensures that the record types defined in CS only contain value fields, and that this also holds for imported types such as Observations.Tally. Hosted transport protocol state is values like any other, eg. DrainCmdPorts.Port.

• Structure is fixed at creation; steady state changes values. The store record is allocated in heap memory in Build, called from the partition's creation code, which also initialises the store variables; after the kernel starts scheduling the Systems in steady state, they change store variable values.

• Groundwork. The vocabulary fixed above – Component, store variable – is what tokens, manifests, and checks speak (Tokens); the named array types serve the System signatures (The System Modules); the hosted transports make CS one side of the partition crossing (Ports and Adapters).

CL – Components Locked

Overview

The locked part is its own construct kind: it holds no run state, it creates itself – populated by its module body, not by the partition's creation code – and it is the only component module that exports values for foreign partitions.

The constructs of this chapter contribute to the following invariants:

• structure is fixed at creation; steady state changes values;
• stores are partition-private;
• the store holds values and handles, never references to data via pointers or addresses.

Constructs

MODULE CLprint;

  IMPORT R, V := Vprint, W := Wprint, Observations;

  TYPE
    DrainCfg* = RECORD
      maxCmdNo*: INTEGER;
      periods*: ARRAY W.DrainPeriod_Num OF INTEGER
    END;

  VAR
    L*: RECORD
      (* all print buffers use the same calibrations *)
      (* if different calibs needed -> arrays over W.PrintBuf_Num *)
      pbDistCalib*: Observations.DistCalib;
      pbAdaptCalib*: Observations.AdaptCalib;

      drainCfg*: DrainCfg;
      drainUartHandle*: INTEGER; (* handle in UART.mod *)
      drainPrintBufIx*: INTEGER; (* index of the print buffer DrainSystem drains *)
    END;

    I*: RECORD
      termPrintWriter*: INTEGER;
    END;

BEGIN
  L.drainUartHandle := R.UartHandle_Drain;

  L.drainCfg.periods[0] := V.DrainPeriod_Slow;
  L.drainCfg.periods[1] := V.DrainPeriod_Mid;
  L.drainCfg.periods[2] := V.DrainPeriod_Fast;

  L.drainCfg.maxCmdNo := LEN(L.drainCfg.periods) - 1;

  (* define a specific role/use *)
  I.termPrintWriter := R.WriterHandle_Term;
  L.drainPrintBufIx := W.Ix_PrintBuf_Term;

  (* print clipping observations *)
  Observations.Calibrate(V.pbClipsCalibDef, L.pbDistCalib, L.pbAdaptCalib)
END CLprint.

Five properties define the locked part:

• Locked by the language. Exported variables are read-only to every importer; populated in the module body, which runs before any importing module's code – the locked part is complete before any System can look. And CL exports no procedures, so after load no code exists that could write it: written once, closed thereafter.

• Two exported records, L and I. L holds the partition's own locked components; I is its declared interface – the values published for foreign partitions: here, the writer handle a foreign System prints through. The qualifier at every use site carries the visibility: CL.L.x is local, CLp.I.x in a foreign System is a declared interface access – one greppable pattern separates sanctioned from unsanctioned reads.

• Locked values may be derived, not only assigned. The last line computes the partition's calibration: an authored value record in V (V.pbClipsCalibDef), passed to a library algorithm whose validity checks run as creation-time assertions, its results locked in L. That is, derivation is a legitimate way to populate CL, and the lock is unchanged by it.

• The assignment configuration terms draw from definition modules. All wiring, value, and resource definition and allocation values are defined in R, V, and W under fact authority.

• Store values use the type native to their configuration target. Handles and indices can be directly declared as basic types such as INTEGER, if this is what the configuration target, such as a UART device, uses for device record lookups: no need to wrap handles and indices in a record.

Contributions to Invariants

• Structure is fixed at creation; steady state changes values. CL is allocated by the compiler in module memory space, and its values are assigned by the module body during the program start-up sequence, guaranteed to be executed before any importing System can access them. Thereafter, the values in CL are locked and immutable, via the read-only access language rule enforced by the compiler.

• Stores are partition-private. CL.I contains the only Components ever exported for direct access by foreign partitions; the qualifier at every foreign use site carries the visibility: CLp.I.x is sanctioned, CLp.L.x is a finding, one greppable pattern.

• The store holds values and handles, never references to data via pointers or addresses. A review ensures that the record types defined in CL only contain value fields, that this also holds for imported types such as Observations.DistCalib, and that all store values declared without a record type are not pointers or addresses.

Tokens

Overview

Every store variable – every field of a StoreDesc – has a token: a small integer naming it in the manifests, the checks, and the reports.

The constructs of this chapter are foundation rather than direct carriers: the tokens underlie the manifests (The System Modules), and through them the checks (The Kernel).

The invariants verified over the manifests all stand on them:

• every Component instance has exactly one writer;
• the run order is derived from the declared roles;
• a shared facility has its declared depositors and at least one collector.

Constructs

The tokens live in the partition's T module:

MODULE Tprint;

  IMPORT Tbase, PlanView, Errors;

  CONST
    drainRun = 0;
    adaptRun = 1;
    pbBuf = 2;
    pbClipsTally = 3;
    pbClipsObsPort = 4;
    pbClipsAcct = 5;
    drainCmdPort = 6;

    NumTokens = 7;
    Base = Tbase.TprintBase;

  VAR
    L*: RECORD
      drainRun*: INTEGER;
      adaptRun*: INTEGER;
      pbBuf*: INTEGER;
      pbClipsTally*: INTEGER;
      pbClipsObsPort*: INTEGER;
      pbClipsAcct*: INTEGER;
      drainCmdPort*: INTEGER
    END;

    I*: RECORD
      print*: SET
    END;

    Names*: ARRAY NumTokens OF PlanView.TokenName;

BEGIN
  (* back-check Tbase *)
  ASSERT(Tbase.TprintNum = NumTokens, Errors.ConsCheck);

  (* local tokens *)
  L.drainRun := Base + drainRun;
  L.adaptRun := Base + adaptRun;
  L.pbBuf := Base + pbBuf;
  L.pbClipsTally := Base + pbClipsTally;
  L.pbClipsObsPort := Base + pbClipsObsPort;
  L.pbClipsAcct := Base + pbClipsAcct;
  L.drainCmdPort := Base + drainCmdPort;

  (* interface token sets *)
  I.print := {L.pbBuf, L.pbClipsTally};

  (* token names *)
  Names[drainRun] := "drainRun";
  Names[adaptRun] := "adaptRun";
  Names[pbBuf] := "pbBuf";
  Names[pbClipsTally] := "pbClipsTally";
  Names[pbClipsObsPort] := "pbClipsObsPort";
  Names[pbClipsAcct] := "pbClipsAcct";
  Names[drainCmdPort] := "drainCmdPort"
END Tprint.

The token construct is defined by four properties, each buying a mechanical review:

• One token per store variable.

• The token's name is the variable's name, verbatim, in the L record and in the Names table alike.

• T.I contains only role-named sets. The interface record holds no individual tokens; it holds surfaces – I.print is the deposit surface of the print facility, the set a participant declares wholesale (Depositors and Collectors, below). In a foreign System, Tp.I.x is a correctly declared participation, Tp.L.x is a finding, comparable to CL.I and CL.L.

• L/I mirror the store family's split: local tokens, interface surfaces – the same qualifier grammar as CL, one audit pattern across the families.

Token values are allocated program-wide by Tbase – counts authored, bases derived, overlap impossible by construction:

MODULE Tbase;

  IMPORT
    Kernel, Errors;

  CONST
    TblinkNum* = 5;
    TprintNum* = 7;
    TcoordNum* = 2;
    TmonNum* = 1;

    TblinkBase* = 0;
    TprintBase* = TblinkBase + TblinkNum;
    TcoordBase* = TprintBase + TprintNum;
    TmonBase* = TcoordBase + TcoordNum;

    T = TblinkNum + TprintNum + TcoordNum + TmonNum;

BEGIN
  ASSERT(T <= Kernel.MaxTokens, Errors.ConsCheck)
END Tbase.

Each partition's T asserts its count against Tbase (the back-check above); Tbase asserts the total against the kernel's capacity. A miscounted partition fails at creation with its own error, not with a phantom dataflow edge. Tnames aggregates the partitions' name tables for the development-build report – dev tooling, not functionally essential.

Contributions to Invariants

• The manifest-checked invariants stand on the tokens. Every Component instance has exactly one writer; the run order is derived from the declared roles; a shared facility has its declared depositors and at least one collector: all three are verified over the manifests (The System Modules), and a manifest is sets of tokens. The tokens give every store variable one program-wide identity, so two Systems' declarations about the same store variable meet in the same token value – a second writer shows as the same token in two writer sets, an edge as a token shared between a producer set and a consumer set. Without that shared identity there is nothing to compare; with it, the checks are set expressions.

• Groundwork. The Names tables feed the report via Tnames; the T-beside-CS walk – name against name – is review capacity for the whole store family. And the token space is the allocations doctrine in miniature: values derived where derivable (the bases), asserted where the space is owned (the back-check, the kernel-capacity check) – authored throughout, never searched.

The System Modules

Overview

One module per System. The constructs of this chapter contribute to the following invariants:

• all state is in Components; a System holds none;
• every Component instance has exactly one writer;
• the run order is derived from the declared roles;
• a shared facility has its declared depositors and at least one collector;
• Systems meet only in the store;
• a System runs to completion;
• every store access is a System's.

The Module

A typical System module, from the blink partition:

MODULE ActuateSystem;

  IMPORT T := Tblink, CS := CSblink, CL := CLblink, LEDbinding, Kernel;

  CONST
    SystemName = "Actuate";

  VAR
    Manifest*: Kernel.Manifest;
    Name*: Kernel.SystemName;

  PROCEDURE runLed(pin: INTEGER; set: INTEGER; measured: INTEGER);
  BEGIN
    IF measured # set THEN
      LEDbinding.Put(pin, set)
    END
  END runLed;

  PROCEDURE runSystem(setp: CS.LedSetpointArray; meas: CS.LedMeasuredArray; pins: CL.LedPinArray);
    VAR i: INTEGER;
  BEGIN
    i := 0;
    WHILE i < LEN(setp) DO
      runLed(pins[i], setp[i], meas[i]);
      INC(i)
    END
  END runSystem;

  PROCEDURE Run*;
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    runSystem(S.ledSetpointLeader, S.ledMeasuredLeader, CL.L.ledPinLeader);
    runSystem(S.ledSetpointFollower, S.ledMeasuredFollower, CL.L.ledPinFollower)
  END Run;

BEGIN
  Name := SystemName;
  CLEAR(Manifest);
  Manifest.C := {T.L.ledSetpointLeader, T.L.ledSetpointFollower, T.L.ledMeasuredLeader, T.L.ledMeasuredFollower}
END ActuateSystem.

Four properties:

• No import of other System modules. Systems only meet at the store, and never call each other, hence other System modules must not be imported.

• No import of foreign store or definition modules. Stores are partition-private, hence no foreign store modules must be imported in general. If this System used a cross-partition facility implemented or hosted by another partition, for example a print buffer or a port, we would see one or two admissible foreign imports: the other partition's CL or T (their interface records), or one of its adapter modules.

• Systems run to completion. There are no yield-points or polling (busy-waiting) loops.

• The store is accessed via a local copy of the store record pointer: Run opens the write-path to the Component store CS using S := CS.S.

Read on for the store access manifest, and how a layered set of procedures connects the System's logic to the Component store.

The Manifest

Each System declares its store access as a value record of six token sets, defined by the kernel:

Manifest* = RECORD
  C*: SET;      (* consumes: reads another System's product *)
  Cp*: SET;     (* consumes the previous pass's value: the consumer runs BEFORE the producer *)
  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 -- multi-producer by design *)
END;

Five of the classes are what their comments say; Cp, the previous-value consumption, needs more words: the consumer declares that it reads what the last pass left, and the derived order runs it before the producer – the reversed edge. It breaks legitimate same-tick cycles (the couple System reading the leader set-points it mirrors) and it authors a deterministic unit delay where the design wants one: the drain consumes its command port Cp, so a command issued this pass takes effect at the drain's next firing, predictably.

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. CLEAR(Manifest) then set only what applies – absent classes stay empty without naming them. The tokens come from T modules – the System's own (T.L.x) and, for a declared foreign participation, a peer's interface surface (Tp.I.print).

Why declarations, and not introspection – metadata through which a program examines itself at run-time? Not because the environment could not provide it. A manifest is values, not behaviour: introspection is run-time machinery whose own correctness would need review and test, and it would only surface, at run-time, facts about the closed world that are defined and fixed at design time. Nothing is generated, either: the declarations are ordinary source, written and reviewed like all the rest.

Run, runSystem, and the Rim

The three procedures of ActuateSystem are the idiom that connects a System to the store – an authority gradient in three layers:

• Run* resolves the store pointer once and hands out named slices: every token-relevant S.x name appears here, exactly once, next to the CL slices that ride along. The argument lines are the manifest re-stated in code – the review walk reads them against the declaration, name by name.

• runSystem carries the law over named fixed array types – CS.LedSetpointArray, CL.LedPinArray – not open arrays. The named types are the compiler's strongest grip: name equivalence rejects a cross-role actual (a measured array where a set-point array belongs) and a cross-size one; LEN of a fixed formal folds to a constant; and a fixed-typed parameter passes as one word where an open array costs two. Open arrays remain the library's form – sizes are unknowable there; in a System they are authored facts, and the check gradient follows the knowledge gradient. Parameter modes still mirror the manifest: VAR for written slices, value for read – structured value parameters pass by reference and are compiler-enforced read-only, so the value mode is the read declaration, at no copy cost.

• the rim leaf – runLed(pin, set, measured) – is the hand-over to the substrate: bare integers, already the library's vocabulary, so the driver call crosses with no conversion. At the rim the names carry the whole contract; a rim call whose names do not state its meaning is a naming defect, since names are the only contract carrier below the checked layers.

runSystem is population-blind – no size constant, no role knowledge; population identity concentrates in Run's call lines. Adding a population is a new call line, not a new procedure.

One access deliberately does not go through the signature where nothing is gained: a System may read its own CL.L directly inside the law (the supervisor reads its thresholds so). The export rule already makes every such access read-only – a parameter would duplicate an existing guarantee – and the import list plus the CL.L. pattern keep it reviewable. Passing CL slices as value parameters, as ActuateSystem does, is the choice where the slices participate in the population walk.

Contributions to Invariants

• All state is in Components; a System holds none. The second half of the invariant is this chapter's: a System module's only variables are Manifest and Name, written once at start; all working state arrives through Run's slices. A further module variable is a finding.

• Every Component instance has exactly one writer. Three of the chapter's pieces carry it: the manifest is the check's operand – the declared writer sets Plan compares (The Kernel); the value modes make read slices compiler-held read-only, so a write through a read parameter cannot compile; and the Run seam is the fidelity walk – argument lines against the declaration, name by name, VAR against the write classes.

• The run order is derived from the declared roles. The manifest is the derivation's input, Cp included: declaring the previous-value read is what authors the reversed edge and the unit delay. The order is derived from declarations authored here, computed elsewhere (The Kernel).

• A shared facility has its declared depositors and at least one collector. The declarations live here: a participant's Px off a peer's interface surface, a collector's Cx per token – the check's operand again; the facility itself is Depositors and Collectors' subject.

• Systems meet only in the store. The no-import-of-System-modules property carries it from this side: a System module never imports another System, so no call between them can be written; the import list is the review surface, and The Import Matrix collects the rule with its kin.

• A System runs to completion. The run-to-completion property is this chapter's share – no yield-point, no polling loop in a law, a review item per module; the kernel's side of the same invariant is that no yield exists to call (The Kernel).

• Every store access is a System's. The manifest is the declaration itself: access has a declared owner because the owner declares it, in its own module body, exported read-only.

Ports and Adapters

Overview

The concepts document's transports and adapters take module form.

The constructs of this chapter contribute to the following invariants:

• library code contributes mechanics, never ownership;
• stores are partition-private;
• every store access is a System's;
• structure is fixed at creation; steady state changes values.

The Protocols

Two library modules carry the transport protocols, both payload-blind, both operating on indices and a small state record the client owns:

• RingBuffer – the stream transport: single producer, single consumer, indices only (PutIndex/Publish, GetIndex/Release), the client owning the element storage. Publish-last gives whole-transaction visibility – and crash consistency: a fault mid-write leaves the pre-transaction state.

• SamplingPort – the latest-value transport: Simpson's four-slot algorithm, wait-free on both sides, plain word reads and writes, strictly one reader. PutIndex/Publish bracket the write; GetIndex announces and selects; the client always copies out.

This split enacts the concepts document's Values in Stores; Libraries as Mechanics, in its realisation for a programming language without generics: the library contributes the mechanics – the index protocol, the publish order – and owns neither instance nor cardinality. Both sit with the program: the state records and element arrays are store fields in the hosting CS, and an element capacity is authored in W (PrintBuf_Size bounds the ring's storage). Where a capacity is the algorithm's own fact, it is library-fixed and still appears on the client's side, as the array bound: SamplingPort.NumSlots – Simpson's algorithm needs exactly its four slots.

Both modules document their memory-barrier spots for the day a crossing spans bus masters – the protocols are schedule-cut-ready by design. Under one schedule, the schedule itself is the mutual exclusion, and the protocols cost nothing extra.

One essential protocol is absent from the list: the queueing port – delivery semantics, every value crossing in order, the counterpart of the sampling port's latest-value semantics. It is absent only because EcsControlWatch has no seam that needs it; it will be part of the framework.

Per-Seam Port Modules

A seam's port is its own small module, binding a payload type to a protocol – placed by payload authority: in the library when the payload is library vocabulary (ObservationPorts over the observation library's reading type), in the program when the payload's shape is the program's own fact.

The drain's command port:

MODULE DrainCmdPorts;
(**
  Commands are index-based: the commander only knows a ref/index into a command
  repertoire of the commanded, the command semantics and mechanics are the
  commanded's purview and responsibility.
**)

  IMPORT SamplingPort;

  TYPE
    Command* = RECORD
      cmdRef*: INTEGER;
      timestamp*: INTEGER
    END;

    Port* = RECORD
      state: SamplingPort.State;
      data: ARRAY SamplingPort.NumSlots OF Command
    END;

  PROCEDURE Put*(VAR port: Port; c: Command);
    VAR ix: INTEGER;
  BEGIN
    ix := SamplingPort.PutIndex(port.state);
    port.data[ix] := c;
    SamplingPort.Publish(port.state, ix)
  END Put;

  PROCEDURE Get*(VAR port: Port; VAR c: Command);
    VAR ix: INTEGER;
  BEGIN
    ix := SamplingPort.GetIndex(port.state);
    c := port.data[ix]
  END Get;

  PROCEDURE Init*(VAR port: Port; c0: Command);
  BEGIN
    SamplingPort.Init(port.state);   (* latest = 0, slots 0 -> GetIndex yields 0 *)
    port.data[0] := c0               (* established value: Read defined before first Write *)
  END Init;

END DrainCmdPorts.

Four facts to read off. The port's storage is a Port record – instantiated in the hosting partition's CS, like every transport. The record is strictly values: SamplingPort.State and the Command slots are value types throughout, no pointer, no address – hosted in CS, the port keeps the store reference-free, exactly what the store chapters' review demands of imported types. The state and data fields are unexported: no client can navigate a port, only Put/Get/Init it – here the language does enforce the protocol's boundary. And Init takes an established value: a read is defined before the first write, so the first pass is an ordinary pass – Systems contain no start-up logic.

The header carries the seam's command species (the concepts document's reference form: the commander ships an index into the commanded side's repertoire). A generic command port exists in the library as an authoring template – copied and adapted per seam, deliberately never imported: the payload type is the seam's own fact.

Adapters

Where a foreign partition reads or feeds a hosted transport, the hosting side exports an adapter – the whole module:

MODULE PeriodPortAdapt;
(**
  Adapter for BlinkPartition to read command data from CoordPartition.
**)

  IMPORT CS := CScoord, PeriodPort;

  PROCEDURE GetVal*(VAR value: PeriodPort.Value);
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    PeriodPort.Get(S.periodPort, value)
  END GetVal;

END PeriodPortAdapt.

One procedure: the seam is a read seam, so the adapter exports a read and nothing else. It resolves the hosting store internally – the consumer imports the adapter and the port module (for the Value type), never CScoord. Stateless, so everything it forwards is attributed to the calling System: a route, not a party – it appears in no manifest. The deposit-seam twin, the print facility's writer adapter, is shown in the observations implementation document.

Contributions to Invariants

• Library code contributes mechanics, never ownership. The protocol modules are the specimen: they hold no module state – every signature takes the state record and the storage from the client, and the absence of a VAR section is a zero-hit check. Instances and capacities sit with the program (CS fields, W bounds); even a library-fixed capacity appears on the client's side, as the array bound.

• Stores are partition-private. Two carriers. The port's unexported internals: no client can navigate a port, only Put/Get/Init it. And the adapter's routing: the consumer imports the adapter and the port module's payload type, never the hosting store – the hosting CS is absent from every foreign import list.

• Every store access is a System's. The adapter is a route, not a party: stateless – again an absence of a module VAR section – and appearing in no manifest, so everything it forwards is attributed to the calling System; the single exported verb bounds the seam to its one direction.

• Structure is fixed at creation; steady state changes values. The established value at Init closes the last gap: a read is defined before the first write, so the first pass is an ordinary pass and Systems contain no start-up logic – steady state begins structurally and behaviourally complete.

The Main Program and the Partitions

Overview

Each partition owns its creation, behind exactly two exported procedures; the main program composes the partitions and hands over to the kernel.

The constructs of this chapter contribute to the following invariants:

• structure is fixed at creation; steady state changes values;
• stores are partition-private;
• the operational invariants.

Constructs

A partition module, with the two exported procedures:

MODULE BlinkPartition;

  IMPORT
    P, CS := CSblink, CL := CLblink, Kernel, LEDbinding,
    ActuateSystem, BlinkSystem, CoupleSystem, SenseSystem;

  PROCEDURE build;
  BEGIN
    CS.Build;
    LEDbinding.Config
  END build;

  PROCEDURE acquire;
    VAR S: CS.Store; i: INTEGER;
  BEGIN
    S := CS.S;
    i := 0;
    WHILE i < LEN(CL.L.ledPinLeader) DO
      LEDbinding.Get(CL.L.ledPinLeader[i], S.ledMeasuredLeader[i]);
      LEDbinding.Get(CL.L.ledPinFollower[i], S.ledMeasuredFollower[i]);
      INC(i)
    END
  END acquire;

  PROCEDURE value;
    VAR S: CS.Store; i: INTEGER;
  BEGIN
    S := CS.S;
    i := 0;
    WHILE i < LEN(S.ledSetpointLeader) DO
      S.ledSetpointLeader[i] := 0;
      S.ledSetpointFollower[i] := 0;
      INC(i)
    END;
    i := 0;
    WHILE i < LEN(S.blinkTicker) DO
      S.blinkTicker[i] := 0;
      INC(i)
    END
  END value;

  PROCEDURE propagate;
    VAR S: CS.Store; i: INTEGER;
  BEGIN
    S := CS.S;
    i := 0;
    WHILE i < LEN(CL.L.ledPinLeader) DO
      LEDbinding.Put(CL.L.ledPinLeader[i], S.ledSetpointLeader[i]);
      LEDbinding.Put(CL.L.ledPinFollower[i], S.ledSetpointFollower[i]);
      INC(i)
    END
  END propagate;

  PROCEDURE CreateWorld*;
  BEGIN
    build;
    acquire;
    value;
    propagate
  END CreateWorld;

  PROCEDURE AddSystems*;
  BEGIN
    Kernel.AddSystem(BlinkSystem.Run, BlinkSystem.Manifest, P.EachTickPeriod, BlinkSystem.Name);
    Kernel.AddSystem(CoupleSystem.Run, CoupleSystem.Manifest, P.EachTickPeriod, CoupleSystem.Name);
    Kernel.AddSystem(ActuateSystem.Run, ActuateSystem.Manifest, P.EachTickPeriod, ActuateSystem.Name);
    Kernel.AddSystem(SenseSystem.Run, SenseSystem.Manifest, P.EachTickPeriod, SenseSystem.Name);
  END AddSystems;

END BlinkPartition.

The four sub-phases – build, acquire, value, propagate – are the concepts document's creation contracts, one local procedure each, kept even where a phase is empty: the uniform protocol is the review surface. Phases with real content read as their contracts: acquire samples the pins into the measured Components; propagate writes the set-points out, so the hardware's initial state is derived from the store. value sets every remaining Component explicitly – nothing zeroes memory at load in Oberon, and nothing should: the zeroth consistency point demands designed values, and automatic zeroing would only make a missed initialisation read like data.

Partition creations are mutually independent – no CreateWorld reads a peer's state – so the main program is pure composition:

MODULE EcsControlWatchV21;

  IMPORT
    P, Main, BlinkPartition, PrintPartition, CoordPartition, MonPartition,
    Kernel, PlanView, Console, Tnames;

BEGIN
  Kernel.Install(P.TickPeriod);
  PrintPartition.CreateWorld;
  BlinkPartition.CreateWorld;
  CoordPartition.CreateWorld;
  MonPartition.CreateWorld;
  Kernel.Begin;
  PrintPartition.AddSystems;
  BlinkPartition.AddSystems;
  CoordPartition.AddSystems;
  MonPartition.AddSystems;
  Kernel.Plan;
  PlanView.Report(Console.Werr[Console.SYSTERM0], Tnames.Names);
  Kernel.Commit;
  Kernel.Run
END EcsControlWatchV21.

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. Kernel.Install sets the tick and claims the kernel's own timer – an infrastructure claim, asserted at once; Kernel.Begin opens System registration.

One observation for readers of the previous implementation: its creation had an attest phase – a pass asserting that every wired device reference resolved to a constructed device – dropped here without successor. Its check class, agreement between second authorities, is systematically eliminated by the single-authority-per-fact discipline: what remains to guard is guarded at the true authority (PrintBuffers.Init asserts its size against the caller's buffer; Kernel.Install asserts its own timer claim), not re-checked from outside.

Contributions to Invariants

• Structure is fixed at creation; steady state changes values. The creation protocol is where the fixing happens: every NEW sits in creation code, reached from CreateWorld – nowhere else in the program does a NEW appear – and the uniform four-phase shape, kept even where a phase is empty, is what makes "creation only" walkable partition by partition. The gate's side of the same invariant, the end of registration, is The Kernel's.

• Stores are partition-private. The main program's import list names partition top modules and nothing of their insides – no store module appears in it, so composition cannot reach into any partition's world. The partitions match it: no CreateWorld reads a peer's state, so the creations compose in any order.

• The operational invariants. Verified at creation rather than held – both verifications are stations of the gate (Enforcement): the framework start-up establishes the infrastructure before the main body's first line – importing Main is what places it there – and the sampling acquire is where the interface hardware's live check lives: a device that cannot answer fails creation, in the phase where failure is allowed and handled. This program does not exercise that check: its acquire reads GPIO pin states, and a register read cannot refuse – the check has force only where a device can fail to answer, a sensor on a bus, a link with a handshake.

Depositors and Collectors

Overview

The deposit classes carry the shared facilities. Of the concepts document's two facility kinds, EcsControlWatch uses the stream kind: the print facility is one shared ring plus its event tally – no per-participant slots. Several Systems print; the characters interleave in one transport; nobody's identity is attached to a byte.

The constructs of this chapter contribute to the following invariants:

• a shared facility has its declared depositors and at least one collector;
• every store access is a System's.

Constructs

The facility's tokens are published as a deposit surface – a role-named set in the hosting partition's T.I:

I.print := {L.pbBuf, L.pbClipsTally};

A participant declares the surface wholesale – the monitoring partition's load generator:

BEGIN
  Name := SystemName;
  CLEAR(Manifest);
  Manifest.O := {T.L.heartbeatStatus};
  Manifest.Px := Tp.I.print
END HeartbeatSystem.

Px is the one deliberately multi-writer class – multi-producer by design. What makes it sound is the pair the concepts document names: under one schedule, the schedule is the mutual exclusion, and each deposit is whole (run-to-completion); the transport's protocol covers the rest. The collectors declare Cx per token and run after every depositor: the drain collects the ring (Cx := {T.L.pbBuf}), the observation distiller collects the tally (Cx := {T.L.pbClipsTally}).

The indexed kind – one slot per participant, each depositor writing its own under its own identity – remains available where attribution matters; the stream kind is the fit where it does not: an aggregate facility whose overload is an aggregate fact. Adding a participant to the stream facility is one manifest line (Px := Tp.I.print) and the writer handle from the host's CL.I; no store change, no collector change.

Contributions to Invariants

• A shared facility has its declared depositors and at least one collector. The deposit surface makes the depositor side declarable wholesale, and each collector declares its Cx per token – together the gate's operand: an uncollected deposit is a recorded violation, and the derived order places every collector after every depositor. What keeps the deliberate multi-producer sound is stated in the constructs above: the schedule as mutual exclusion, whole deposits, the transport's protocol.

• Every store access is a System's. Participation appears in the participant's own manifest – Px := Tp.I.print rides the depositing System's declaration, whatever machinery sits on the path: the writer handle, the adapter, the ring all forward an access that remains the System's.

Bindings and Handles

Overview

Two constructs connect the store's world to the hardware's: the binding modules, the program-specific connectors, and the handle, the store's one sanctioned indirection.

The constructs of this chapter contribute to the following invariants:

• the store holds values and handles, never references to data via pointers or addresses;
• on the synchronous control path, the HAL is stateless and passive.

Constructs

Binding modules are the program-specific connectors to the hardware: UARTbinding configures the drain UART and its pins, LEDbinding configures and touches the LED GPIOs – drawing their facts from R, under fact authority.

Handles exist only where a boundary is crossed that raw references must not cross – genuine pointer resolution (a device record, a text writer) or seam denial. Everywhere else the store holds the value directly: a handle that merely looks up a value the store could hold is a layer to be removed. The service modules behind the handles own their device tables – technical state, re-establishable beneath an unchanged handle.

The drain UART shows the whole remaining chain:

(* R: the choices -- a handle, a unit, the pins *)
UartHandle_Drain* = 0;
UartUnit_Drain* = UART.UART1;
Pin_DrainUartTx* = 4;
Pin_DrainUartRx* = 5;

(* CLprint body: the handle bound into the locked part *)
L.drainUartHandle := R.UartHandle_Drain;

(* PrintPartition.build: device constructed, bound, configured *)
NEW(uartDev); ASSERT(uartDev # NIL, Errors.HeapOverflow);
UART.Init(uartDev, R.UartHandle_Drain, R.UartUnit_Drain);
UARTbinding.Config(CL.L.drainUartHandle, R.Pin_DrainUartTx, R.Pin_DrainUartRx, V.DrainBaudrate)

From then on, a System reads the handle from CL.L and passes it to the driver's procedures; the pointer behind it never leaves the driver module.

Contributions to Invariants

• The store holds values and handles, never references to data via pointers or addresses. The handle doctrine keeps the invariant's second half livable: where a reference is genuinely needed, the store carries an INTEGER handle in its place, and the pointer behind it never leaves the driver module – absent from the store, absent from every System. The lifecycle property rides along: technical state is re-established beneath an unchanged handle, so the handle survives a recovery that the pointer could not.

• On the synchronous control path, the HAL is stateless and passive. The bindings concentrate configuration at creation – Config is called from build, nowhere else – and steady state meets the devices fresh: the drain's UART access reads status anew and writes guarded, with no module variable caching device state on the path.

The Kernel

Overview

The kernel is a framework module, in the example's lib directory. 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. The partitions changed nothing in it: one scheduler, one global token space, and Plan works across the partitions without knowing they exist.

The constructs of this chapter contribute to the following invariants:

• every Component instance has exactly one writer;
• the run order is derived from the declared roles;
• a shared facility has its declared depositors and at least one collector;
• a System runs to completion;
• structure is fixed at creation; steady state changes values.

Registration

Each partition's AddSystems registers its Systems – procedure, manifest, period in ticks (0 = every tick, which P names EachTickPeriod), name. The order of these calls, and of the partitions, 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 verification of the declared structure – and it does not fault on detected violations: every check is evaluated, every violation recorded with its offending tokens; then the dependency edges are derived and the Systems topologically sorted into the run order.

The checks are set expressions over the manifests:

The edges: a consumer's C against a producer's P, a collector's Cx against the depositors' Px – and a Cp consumer's edge reversed: the producer depends on the consumer, so the consumer runs first and reads the previous pass's value. The unit delay is thereby scheduled, not simulated.

Commit is the gate's final station – two assertions: a plan exists, and no unrelaxed check failed. In a deployed program a rejected plan is a hard fault with its own error code – a static construction fault, never retryable.

Development Builds

Development builds insert, they never restructure. Between Plan and Commit, the development main program adds one call: PlanView.Report prints every manifest, the dependency list, the derived order, and every violation by name – in store-variable vocabulary: the token definitions of the Tx modules, aggregated by Tnames.

The report EcsControlWatch prints at every start:

Kernel.Plan
manifests (registration order):
 0 Drain
   Cp:
     drainCmdPort
   O:
     drainRun
   Cx:
     pbBuf
 1 PrintClip
   O:
     pbClipsAcct
   P:
     pbClipsObsPort
   Cx:
     pbClipsTally
 2 AdaptDwell
   C:
     pbClipsObsPort
   O:
     adaptRun
   P:
     drainCmdPort
 3 Blink
   C:
     periodPort
   O:
     blinkTicker
   P:
     ledSetpointLeader
 4 Couple
   Cp:
     ledSetpointLeader
   P:
     ledSetpointFollower
 5 Actuate
   C:
     ledMeasuredLeader
     ledMeasuredFollower
     ledSetpointLeader
     ledSetpointFollower
 6 Sense
   P:
     ledMeasuredLeader
     ledMeasuredFollower
 7 Period
   O:
     periodSeq
   P:
     periodPort
 8 TickMonitor
   Px:
     pbBuf
     pbClipsTally
 9 Heartbeat
   O:
     heartbeatStatus
   Px:
     pbBuf
     pbClipsTally
dependencies (registration order):
 0 Drain
     TickMonitor
     Heartbeat
 1 PrintClip
     TickMonitor
     Heartbeat
 2 AdaptDwell
     Drain
     PrintClip
 3 Blink
     Couple
     Period
 4 Couple
 5 Actuate
     Blink
     Couple
     Sense
 6 Sense
 7 Period
 8 TickMonitor
 9 Heartbeat
derived scheduling order:
 0 Couple
 1 Sense
 2 Period
 3 Blink
 4 Actuate
 5 TickMonitor
 6 Heartbeat
 7 Drain
 8 PrintClip
 9 AdaptDwell
plan checks: all pass

The Cp edges are readable in it: Couple depends on nobody yet runs first – Blink depends on Couple (the reversed edge) and on Period; Drain runs before AdaptDwell publishes its next command. Because Plan collects everything before Commit gates, a broken program reports all its violations in one run, before the fault.

The three coverage checks – unproduced, unconsumed, uncollected – can be waived (Kernel.Relax), so a producer can be tested before its consumer exists; the structural checks cannot: Relax masks its argument against the relaxable set. The kernel also carries run-time instrumentation: per-System and scheduler pass times, exported read-only like everything else. A deployed main program can omit the report call, and always omits the Relax call; 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. 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 increments a counter, and the loop's cursor difference is the number of ticks the pass represents – one, normally; more, when a pass overran. 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 in read-only counters – the kernel is a sensed device, and whether missed ticks become control data is a System's decision (the monitoring partition samples them).

Periods are counts of ticks, converted from milliseconds once, in P, where they are defined. A System may also self-time inside an every-tick registration – its ticker in its own store state, advanced by the elapsed count – which is how the drain follows a commanded period; the grid-locked reload that makes its runs phase-reproducible is shown in the observations implementation document.

Contributions to Invariants

• The manifest-checked invariants – the kernel holds the gate's final station. Plan tests the declarations against each other and records every violation; Commit refuses a violated world. The single-writer and class-agreement checks carry every Component instance has exactly one writer; the edge derivation and the topological sort carry the run order is derived from the declared roles – with orderless registration as its ground: no order is authorable, so the derived one is the only one there is; the coverage checks and the collectors-after-depositors ordering carry a shared facility has its declared depositors and at least one collector – and the tick loop adds that invariant's other half: running the Systems one at a time, to completion, is the mutual exclusion that makes the deliberate multi-producer sound.

• A System runs to completion. The kernel's side of it is an absence: no yield exists to call – the loop calls a Run and regains control only by its return; the law's side, no polling or waiting loop, is the System chapters' review.

• Structure is fixed at creation; steady state changes values. The kernel's share is the registration bracket: Begin opens it, Commit closes it, and after the gate the System set is closed – the kernel implements steady state with no way to add, remove, or reorder Systems.

• Groundwork. All kernel state is exported read-only – the kernel is a sensed device, which is what lets monitoring arrive as ordinary Systems – and the printed plan is per-run evidence: manifests, edges, and derived order at the head of every trace, so whether a build is the reviewed program is readable off its own output.

The Import Matrix

Overview

The import matrix spans the whole program: every module kind, one row, its imports and its never-imports. It stands here, after all the module kinds have been introduced – part design summary, part review instrument.

The constructs of this chapter contribute to the following invariants:

• stores are partition-private;
• Systems meet only in the store;
• no System configures the infrastructure.

Constructs

The import matrix is part of the design (utility imports such as error codes aside):

What a module does not import, its code cannot name – and the never column is a review surface: a System importing a W module is a finding, a peer's CS in any foreign import list is the privacy violation, visible in one line.

One consequence of the matrix is worth naming: infrastructure modules appear in exactly one import list – the main program's. The start-up anchor must be imported there (importing the framework's Main first is what places the program start-up ahead of everything), and nothing else has business with the infrastructure: no other import list names it. The concepts document's "no System configures the infrastructure" is thereby verified like the rest of the matrix, over the import lists: an infrastructure module in any other import list is a finding.

The rule is role-relative, as this architecture's dividing lines are – and the role is decided by authority, not by touch:

• Reading a value promotes nothing: the timers in use are interface hardware, and a System importing the timer driver to read a timestamp is ordinary device use, no different from reading a sensor.

• Promotion is a control event: a program that actively controls a clock has moved that clock out of the infrastructure – it is then controlled substrate, a plant on the control path, its module imported by its bindings and Systems like any device, the control-path conditions taken on with it.

What remains infrastructure remains main-only; one chip block may sit on both sides at once, its two roles read off the import lists and the access they carry.

Two further qualifications: a substrate monitor may import an infrastructure module read-only, to observe it – none exists in this program; the tick monitor observes the kernel, a framework module read as a sensed device --, and development builds let Systems print to the console service: instrumentation, flagged as such in the code, absent from a deployed build.

Contributions to Invariants

• Stores are partition-private. The never column is the review surface: a peer's CS in any foreign import list is the violation, visible in one line.

• Systems meet only in the store. The same surface, another row: no System imports another System – the import lists are the entire evidence.

• No System configures the infrastructure. The consequence spelled out above: infrastructure modules appear in exactly one import list, the main program's; an infrastructure module in any other list is a finding.

Holding the Invariants

The chapters' contribution lines, collected: the concepts document's structural invariants against the constructs that carry them – the n:m of Constructs Contribute to Invariants as one map. Most invariants are held at more than one tier; what this program does not exercise, the table says rather than hides.

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 the sampling acquire – the live check where a device can fail to answer, present in form but not exercised here, since this program's pin reads cannot refuse – and by each guard at its true authority. Their supervision in steady state arrives as Components – and is no longer the next round's subject but a built and verified capability: the observations set.

Appendix: Language Features by Enforcement Tier

The architecture's grip on the language, collected: the features actively exploited for invariant support, grouped by the tier each serves. Several serve two tiers – one leg enforcing, one leg a review surface – and appear under both.

Language

• Read-only export of variables – the locked parts; manifests unalterable by importers; the kernel's state as a sensed device.

• Selective export – what is not exported cannot be named or called: port internals unnavigable; a module without exported procedures is unreachable after load – the closure of CL, V, and T alike.

• Module bodies run before any importer's code, exactly once – locked parts complete before any System looks; initialisation unrepeatable (and see Gate).

• Import lists – what a module does not import, its code cannot name (and see Review).

• Name equivalence of structured types – cross-role actuals rejected in signatures despite identical structure.

• Fixed array types with constant bounds – sizes as authored facts; cross-size actuals rejected; LEN of a fixed formal folds to a constant, keeping the law population-blind.

• Value-mode structured parameters: read-only, passed by address – the read declaration, compiler-held, at no copy cost; write access only through VAR, so the modes mirror the manifest.

• Records as value types, whole-record assignment – a snapshot in one assignment; the manifest copied at registration (and see Gate).

• References only via declared pointer types, no casts – the never-references invariant decidable from the TYPE sections; the SYSTEM pseudo-module's escapes are visible in any import list.

• Compile-time constant expressions – definition facts fixed before creation runs; the token bases derived, cross-partition overlap excluded by arithmetic.

Gate

The gate is ordinary program code; these features give it its teeth:

• Module bodies, dependency-ordered – the gate's first station is the language's initialisation itself: every body runs with its imports already initialised, so the architecture-level assertions fire in prerequisite order, before anything downstream of them exists (and see Language).

• SET and set operations – the manifests as token sets; the checks as set expressions over them.

• ASSERT with error codes – the refusals of all three stations, each at its fact's authority.

• Records passed by value – the registered manifest is a copy; the gate's operand cannot be altered after registration (and see Language).

• Procedure variables – registration without the kernel importing a single System: the gate verifies a world it has no compile-time knowledge of.

Review

• Import lists as the review surface – the never column of the import matrix; the absence checks, zero-hit searchable.

• Export marks as visibility documentation – the L/I qualifier grammar readable at every use site, greppable program-wide.

• Import aliasing – provenance at every use site (CS := CSprint, Tp := Tprint).

• Declarations as complete evidence – the TYPE section decides no-pointer, the VAR section decides statelessness: reading concludes.

• No reflection, no introspection, no dynamic loading – the source is the complete truth of the program: what makes review a total method rather than a sampling of run-time behaviour.

See Also

• ECS for Control: Concepts
• ECS for Control: Observations – Concepts
• ECS for Control: Observations – Calibration
• ECS for Control: Observations – Implementation
• ECS for Control: Observations – Verification

Last updated: 28 August 2026