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, schedules and their boundary, 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 evaluation and test programs EcsControlSchedule: three programs of one family – one with a single schedule, one with two schedules on the two cores of the RP2350, and one with a partition moved from one schedule to the other. The partitions are the same modules in all three.

A schedule is one run of the kernel's loop over its own set of partitions, on its own core; a program has one or more of them. The constructs are presented for the program with several schedules. The program with one schedule is the case where the schedule layer has nothing to do, and it is shown where it differs.

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. With several schedules, no schedule proceeds past Plan before every schedule has planned, and none enters Run before every schedule has committed.

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 program's definition – an ECS file beside the sources, defined in the ECS file reference – states in one place the facts the walk reads: the modules and their kinds, the tokens and surfaces, the manifests, the schedules and their crossings. Two things build on it:

• the review guide lays out the review of a program as a walk in parts – every module before its kind, each module against its kind, the pairs of kinds, the program as a whole, and what a person alone reads – one check-point per property, stating where it is read, what must hold, and what a program without it is;

• a set of tools supports the walk: check-ecs checks the program against the check-points of the review guide and prints its findings under their identifiers; extract-ecs collects the facts from the implementation and regenerates the file's derived part, so that a change in the sources, or a drift between the two, is detected and documented; a generator writes a program skeleton from an authored definition, the kinds' reference implementations filled in. Each link is the tool's manual page; the generator is not published with this round.

The tools support the work; the discipline does not rely on them. What they check is what review checks, and a program without an ECS file is reviewed by the same walk.

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 schedule modules – one per schedule (kind SCHEDULE): each brings up its core's infrastructure, sequences its partitions' world creation and hands over to the kernel; the schedule module of schedule 0 is the main program module;

• partition modules – create the partitions' worlds, and register their Systems (via their schedule module) (kind PARTITION);

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

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

• port and adapter modules – interactions and communication between partitions as needed (the transport kinds SPORT, QPORT, RBUFFER, BUFFER; kind ADAPTER);

• the boundary module – the crossings between schedules, declared once for the program (kind BOUNDARY);

• the consistency module – the assertions that must hold across partitions' definitions (kind CONS);

• binding modules – the program-specific modules that operate the hardware for a partition's Systems, as needed (kind BINDING);

• other modules – a program module of no other kind, a helper or a program's own memory map, which the definition places and says nothing further about (kind OTHER);

• definition modules – the values defining structures, tuning, resources, periods, and store tokens (kinds WIRING, VALUES, RESOURCES, PERIODS, TOKENS, TOKENBASES, TOKENNAMES);

• 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. A library module declares no kind.

The kind names in parentheses are the ones the ECS file reference defines, one per kind of module. Every program module declares its kind in a comment before its MODULE line: the kind name, followed by the module's own identifiers for the kind's roles, in the order the reference gives:

(* ECSKIND: SYSTEM Manifest Name Run *)
MODULE ActuateSystem;

The listings in this document carry the declaration; the chapters below present the constructs under the names the programs give their modules.

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.

The program-level modules are one letter each: P, R, T, N, C, B.

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

The modules of a partition lie in a directory of their own, named as the partition module by convention; the program-level modules lie in the program directory. The placement is a fact of the tree: which partition a module belongs to, if any, is read off its directory.

The Definition Modules

Kinds: WIRING, VALUES, RESOURCES, PERIODS, CONS, TOKENS, TOKENBASES, TOKENNAMES

Overview

Every partition authors its own definitions; five 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 schedules, which span 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

(* ECSKIND: RESOURCES *)
MODULE R;

  IMPORT UART, TIMER, LEDext, EXC;

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

    (* chip peripherals *)
    UartUnit_Drain* = UART.UART1;
    TimerUnit_Kernel* = TIMER.TIMER0;

    (* exception prios *)
    ExcPrio_Systick* = EXC.ExcPrioLow;

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

    Pin_LedLeader0* = LEDext.LED0;
    Pin_LedLeader1* = LEDext.LED2;
    Pin_LedFollower0* = LEDext.LED1;
    Pin_LedFollower1* = LEDext.LED3;

END R.

Two groups of choices concern the infrastructure: the kernel's timer is a claim like any device's, a handle and a unit, passed to the kernel when it is installed; and the exception priority of the kernel's tick is a resource – the priority scheme of a program, which interrupts outrank the tick and where the fault path sits, is authored here, and the framework modules take their priorities as installation parameters.

UartUnit_Drain* = UART.UART1 and Pin_LedLeader0* = LEDext.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 error console", one comment long.

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

(* ECSKIND: WIRING *)
MODULE Wprint;

  IMPORT Errors;

  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 *)

BEGIN
  ASSERT(Ix_PrintBuf_Term < PrintBuf_Num, Errors.ConsCheck)
END Wprint.

Ix_PrintBuf_Term is a role-binding index – which instance plays a role, remappable, so the name survives its value; the body asserts that the index is within the population it indexes. 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, and the agreement asserted at composition by the consistency module C (The Main Program and the Partitions, below) – the follower doctrine of the concepts document, in two lines that must be edited together, deliberately.

The periods module carries one tick period per schedule, and each System's period against the tick of the schedule it runs on:

(* ECSKIND: PERIODS *)
MODULE P;

  CONST
    (* kernel scheduler ticks, milliseconds *)
    TickPeriodS0* = 50;
    TickPeriodS1* = 10;

    (* kernel-based periods are in kernel ticks *)
    (* system periods *)
    (* note: some systems use in-system tickers *)
    EachTickPeriod* = 0; (* for systems to run at each tick *)

    (* blink partition *)
    BlinkPeriod* = EachTickPeriod;
    CouplePeriod* = EachTickPeriod;
    ActuatePeriod* = EachTickPeriod;
    SensePeriod* = EachTickPeriod;

    (* coord partition *)
    PeriodPeriod* = 5000 DIV TickPeriodS1;

    (* mon partition *)
    TickMonitorPeriod* = EachTickPeriod;
    HeartbeatPeriod* = 600 DIV TickPeriodS0;

    (* print partition *)
    DrainPeriod* = EachTickPeriod;
    PrintClipPeriod* = 600 DIV TickPeriodS0;

    (* adapt partition *)
    PrintAdaptPeriod* = 600 DIV TickPeriodS1;

END P.

Which schedule a System runs on is thereby stated in P, as the tick its period divides by; here the coordination partition runs on schedule 1 at a 10 ms tick. A program with one schedule has TickPeriodS0 alone.

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 per schedule. 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 (Components State); V authors what the V-to-CL derivation consumes (Components Locked); the token definitions Tx and T have a chapter of their own (Tokens).

Components State

Kind: 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

(* ECSKIND: STATE S Build *)
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
      ledLeader*: RECORD
        setpoints*: LedSetpointArray;
        measureds*: LedMeasuredArray
      END;
      ledFollower*: RECORD
        setpoints*: LedSetpointArray;
        measureds*: LedMeasuredArray
      END;
      blinker*: RECORD
        tickers*: BlinkTickerArray
      END
    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: ledLeader.setpoints holds one set-point Component per LED role, and these are what a System iterates;

• the store variable is a leaf field of the store record – the unit above the Components: a single Component or a whole population of them. The leaf fields are grouped in records, by the role that writes them (ledLeader, ledFollower) or the facility they belong to (blinker), and a store variable is named by its path below the store record: ledLeader.setpoints;

• 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, in two groups: 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 (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 two transports it hosts, the print buffers and the observation ports; the drain command port is hosted by the adaptation partition that issues the commands:

(* ECSKIND: STATE S Build *)
MODULE CSprint;

  IMPORT W := Wprint, Errors, Observations, PrintBuffer, ObservationPorts;

  TYPE
    PrintBuf* = RECORD
      buf*: ARRAY W.PrintBuf_Size OF CHAR;
      state*: PrintBuffer.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;

    DrainTickArray* = ARRAY W.PrintBuf_Num OF INTEGER;

    Store* = POINTER TO StoreDesc;
    StoreDesc* = RECORD
      printBuf*: RECORD
        bufs*: PbBufArray
      END;
      printBufClip*: RECORD
        tallies*: PbClipsTallyArray
      END;
      bufDrain*: RECORD
        tickers*: DrainTickArray
      END;
      clipsDistiller*: RECORD
        accounts*: PbClipsAcctArray
      END;
      clipsObsPort*: RECORD
        ports*: PbClipsObsPortArray
      END
    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 (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, in two groups. 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 (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. ObservationPorts.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 (System Modules); the hosted transports make CS one side of the partition crossing (Ports and Adapters).

Components Locked

Kind: 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

(* ECSKIND: LOCKED L I *)
MODULE CLprint;

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

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

  VAR
    L*: RECORD
      bufDrain*: RECORD
        uartHandles*: ARRAY W.PrintBuf_Num OF INTEGER; (* handles in UART.mod *)
        cfgs*: ARRAY W.PrintBuf_Num OF DrainCfg
      END
    END;

    I*: RECORD
      termPrintWriter*: INTEGER;
      drainMaxCmdNo*: INTEGER; (* same for all DrainCfg *)
    END;

BEGIN
  ASSERT(LEN(L.bufDrain.uartHandles) = 1, Errors.ConsCheck);
  ASSERT(LEN(L.bufDrain.cfgs) = 1, Errors.ConsCheck);
  ASSERT(LEN(L.bufDrain.cfgs[0].periods) = 3, Errors.ConsCheck);
  CLEAR(L); CLEAR(I);

  L.bufDrain.uartHandles[0] := R.UartHandle_Drain;
  L.bufDrain.cfgs[0].periods[V.DrainSlowCmd] := V.DrainPeriod_Slow;
  L.bufDrain.cfgs[0].periods[V.DrainMidCmd] := V.DrainPeriod_Mid;
  L.bufDrain.cfgs[0].periods[V.DrainFastCmd] := V.DrainPeriod_Fast;

  I.termPrintWriter := R.WriterHandle_Term;
  I.drainMaxCmdNo := LEN(L.bufDrain.cfgs[0].periods) - 1
END CLprint.

The adaptation partition's locked part derives its values rather than assigning them, and publishes half of the result as its interface:

(* ECSKIND: LOCKED L I *)
MODULE CLadapt;

  IMPORT V := Vadapt, Observations;

  VAR
    L*: RECORD
      clipsAdapter*: RECORD
        adaptCalib*: Observations.AdaptCalib
      END
    END;

    I*: RECORD
      distCalib*: Observations.DistCalib
    END;

BEGIN
  CLEAR(L); CLEAR(I);
  (* print clipping observations *)
  Observations.Calibrate(V.pbClipsCalibDef, I.distCalib, L.clipsAdapter.adaptCalib)
END CLadapt.

Six 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. CLadapt's 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 and I. That is, derivation is a legitimate way to populate CL, and the lock is unchanged by it.

• The body asserts the structure it assumes, and clears before it assigns. The index assignments of CLprint are written against populations of a known size; the body states that size as an assertion first. And nothing zeroes memory at load in Oberon: both records are cleared before the first assignment, so that every value is a designed one.

• 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

Kinds: TOKENS, TOKENBASES, TOKENNAMES

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 (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:

(* ECSKIND: TOKENS L I Names *)
MODULE Tprint;

  IMPORT T, Errors;

  CONST
    printBuf_bufs = 0;
    printBufClip_tallies = 1;
    bufDrain_tickers = 2;
    clipsDistiller_accounts = 3;
    clipsObsPort_ports = 4;

    NumTokens = 5;
    Base = T.TprintBase;

  VAR
    L*: RECORD
      printBuf*: RECORD
        bufs*: INTEGER
      END;
      printBufClip*: RECORD
        tallies*: INTEGER
      END;
      bufDrain*: RECORD
        tickers*: INTEGER
      END;
      clipsDistiller*: RECORD
        accounts*: INTEGER
      END;
      clipsObsPort*: RECORD
        ports*: INTEGER
      END;
    END;

    I*: RECORD
      print*: SET;
      clipsObs*: SET
    END;

    Names*: ARRAY NumTokens OF T.TokenName;

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

  (* local tokens *)
  L.printBuf.bufs := Base + printBuf_bufs;
  L.printBufClip.tallies := Base + printBufClip_tallies;
  L.bufDrain.tickers := Base + bufDrain_tickers;
  L.clipsDistiller.accounts := Base + clipsDistiller_accounts;
  L.clipsObsPort.ports := Base + clipsObsPort_ports;

  (* interface token sets *)
  I.print := {L.printBuf.bufs, L.printBufClip.tallies};
  I.clipsObs := {L.clipsObsPort.ports};

  (* token names *)
  Names[printBuf_bufs] := "printBuf.bufs";
  Names[printBufClip_tallies] := "printBufClip.tallies";
  Names[bufDrain_tickers] := "bufDrain.tickers";
  Names[clipsDistiller_accounts] := "clipsDistiller.accounts";
  Names[clipsObsPort_ports] := "clipsObsPort.ports"
END Tprint.

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

• One token per store variable.

• The token's path is the store variable's path, verbatim: L.printBuf.bufs names S.printBuf.bufs, in the L record – grouped as the store record is grouped – 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); I.clipsObs is the surface a foreign partition reads through the partition's port. A surface is a transport the partition hosts, under one name: the set of tokens a peer's access to that transport reaches – the transport itself, and any observation its adapter records beside it, which the peer's access writes and the peer's manifest must therefore cover. The peer declares the surface wholesale and need not know its members. 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. A surface is also what crosses a schedule boundary (Schedules and the Boundary, below).

• 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 the program's token module T – counts authored, bases derived, overlap impossible by construction:

(* ECSKIND: TOKENBASES *)
MODULE T;

  IMPORT
    Kernel, Errors;

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

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

    Tnum = TblinkNum + TcoordNum + TmonNum + TprintNum + TadaptNum;

  TYPE
    TokenName* = ARRAY 32 OF CHAR;

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

Each partition's token module asserts its count against T (the back-check above); T asserts the total against the kernel's capacity. A miscounted partition fails at creation with its own error, not with a phantom dataflow edge. One token space serves all schedules: a token names the same store variable on every core.

N aggregates the partitions' name tables for the plan report, an instrument of the review and nothing in steady state:

(* ECSKIND: TOKENNAMES Names *)
MODULE N;

  IMPORT PlanView, T, Tblink, Tprint, Tcoord, Tmon, Tadapt;

  VAR
    Names*: PlanView.TokenNames;

  PROCEDURE setName(base, token: INTEGER; name: ARRAY OF CHAR; VAR allNames: PlanView.TokenNames);
  BEGIN
    allNames[base + token] := name
  END setName;

  PROCEDURE init;
    VAR i: INTEGER;
  BEGIN
    CLEAR(Names);
    i := 0;
    WHILE i < LEN(Tblink.Names) DO
      setName(T.TblinkBase, i, Tblink.Names[i], Names); INC(i)
    END;
    i := 0;
    WHILE i < LEN(Tprint.Names) DO
      setName(T.TprintBase, i, Tprint.Names[i], Names); INC(i)
    END;
    i := 0;
    WHILE i < LEN(Tcoord.Names) DO
      setName(T.TcoordBase, i, Tcoord.Names[i], Names); INC(i)
    END;
    i := 0;
    WHILE i < LEN(Tmon.Names) DO
      setName(T.TmonBase, i, Tmon.Names[i], Names); INC(i)
    END;
    i := 0;
    WHILE i < LEN(Tadapt.Names) DO
      setName(T.TadaptBase, i, Tadapt.Names[i], Names); INC(i)
    END;
  END init;

BEGIN
  init
END N.

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 (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 N; the T-beside-CS walk – path against path – 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.

System Modules

Kind: SYSTEM

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 belongs to a System.

The Module

A typical System module, from the blink partition:

(* ECSKIND: SYSTEM Manifest Name Run *)
MODULE ActuateSystem;

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

  CONST
    SystemName = "Actuate";

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

  PROCEDURE runLed(set: INTEGER; measured: INTEGER; pin: INTEGER);
  BEGIN
    IF measured # set THEN
      LEDext.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(setp[i], meas[i], pins[i]);
      INC(i)
    END
  END runSystem;

  PROCEDURE Run*;
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    runSystem(S.ledLeader.setpoints, S.ledLeader.measureds, CL.L.ledLeader.pins);
    runSystem(S.ledFollower.setpoints, S.ledFollower.measureds, CL.L.ledFollower.pins)
  END Run;

BEGIN
  Name := SystemName;
  CLEAR(Manifest);
  Manifest.C := {T.L.ledLeader.setpoints, T.L.ledFollower.setpoints, T.L.ledLeader.measureds, T.L.ledFollower.measureds}
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 modules, and of no definition module but the partition's own V. 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. A System may read a tuning value from its own V, a sentinel, say; what it reads is recorded in the ECS file, and a V constant is never an array length or an index, since structure lives in W (The Definition 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.

A System that reaches a foreign partition's transport does so through the hosting partition's adapter, and the adapter's procedure enters the System as a parameter:

(* ECSKIND: SYSTEM Manifest Name Run *)
MODULE BlinkSystem;

  IMPORT T := Tblink, Tc := Tcoord, CS := CSblink, Kernel, PeriodPortAdapt;

  CONST
    SystemName = "Blink";

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

  PROCEDURE runSystem(VAR tickers: CS.BlinkTickerArray; VAR setpoints: CS.LedSetpointArray;
                      ppGet: PeriodPortAdapt.GetValProc);
    VAR i: INTEGER; pv: PeriodPortAdapt.Value;
  BEGIN
    i := 0;
    WHILE i < LEN(setpoints) DO
      DEC(tickers[i], Kernel.ElapsedTicks());
      IF tickers[i] <= 0 THEN
        ppGet(i, pv); (* get blink period from coordinator *)
        setpoints[i] := ORD((BITS(setpoints[i]) / {0}) * {0});
        INC(tickers[i], pv.periodVal)
      END;
      INC(i)
    END
  END runSystem;

  PROCEDURE Run*;
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    runSystem(S.blinker.tickers, S.ledLeader.setpoints, PeriodPortAdapt.GetVal)
  END Run;

BEGIN
  Name := SystemName;
  CLEAR(Manifest);
  Manifest.C := Tc.I.readPeriods;
  Manifest.O := {T.L.blinker.tickers};
  Manifest.P := {T.L.ledLeader.setpoints}
END BlinkSystem.

ppGet: PeriodPortAdapt.GetValProc is the construct: the formal's type is the adapter's procedure type, which carries the direction of the access – a get, by its VAR result – and Run binds the adapter's procedure of that direction; binding a put where a get is declared does not compile (Ports and Adapters, below). The System's law reads a value through a procedure it was handed and knows no store but its own; its manifest declares the surface it consumes, Tc.I.readPeriods, wholesale. Whether the coordination partition runs on this System's schedule or on another is not visible in this module: in EcsControlSchedule-v30 it runs on the other core, and the module is unchanged.

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 sets 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. The form is mandatory: braced tokens and bare surfaces, nothing computed, every set assigned or the record cleared before the first assignment, so that the declaration is readable as written, by the reviewer and by the tools alike, and complete – nothing is zeroed at load, and an unassigned set is garbage. CLEAR(Manifest) then set only what applies – absent sets stay empty without naming them. The manifest stays in the System's module rather than in a partition-wide manifest module the Systems would assign from: the consistency such a module would protect is derived already, by the plan report and the kernel's checks, and the manifest is the System's signature, kept beside the code it binds, the System the single authority over its surface. 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). A manifest states what the System reads and writes, not where the producer runs: it is the same text whether the producer runs on this schedule or on another.

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.

Beside the store slices, Run's argument lines carry the adapter procedures the law uses, one per seam, each of the direction its type declares (PeriodPortAdapt.GetVal in BlinkSystem). The review walk reads these lines against the manifest as well: a consumed surface arrives through a get, a produced one leaves through a put.

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 subject: 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 sets.

• 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 reaches a transport only through an adapter procedure it was handed, whose type names the direction.

• 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 belongs to a System. 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

Kinds: SPORT, QPORT, RBUFFER, BUFFER, ADAPTER

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 belongs to a System;
• 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 mark their memory-barrier spots, and every crossing between two schedules runs over one of them: where the schedule is no longer the mutual exclusion, the barriers are what keep a crossing sound. Under one schedule, the schedule itself is the mutual exclusion, and the protocols cost nothing extra.

A third protocol belongs to the set: the queueing port – delivery semantics, every value crossing in order, the counterpart of the sampling port's latest-value semantics (kind QPORT). EcsControlSchedule has no seam that needs it.

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:

(* ECSKIND: SPORT *)
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 a reference implementation – copied and adapted per seam, deliberately never imported: the payload type is the seam's own fact.

A port module of this shape is a sampling port of the canonical form: the interface the kind SPORT names – Put, Get, Init over a Port record – with the statement order above as the algorithm. The ring buffer has a canonical form of its own (kind RBUFFER: Init, Put, Get, PutMultiple, GetMultiple, Empty, Full, Free, Count over a state and a buffer the client owns), and so has the queueing port (kind QPORT). A transport module of another interface is a BUFFER: its adapter is then written by hand against that interface.

Adapters

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

(* ECSKIND: ADAPTER DrainCmdPorts *)
MODULE DrainCmdPortsAdapt;

  IMPORT CS := CSadapt, DrainCmdPorts;

  TYPE
    Command* = DrainCmdPorts.Command;

    PutCmdProc* = PROCEDURE(h: INTEGER; cmd: Command);
    GetCmdProc* = PROCEDURE(h: INTEGER; VAR cmd: Command);


  PROCEDURE PutCmd*(ix: INTEGER; cmd: Command);
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    DrainCmdPorts.Put(S.drainCmdPort.ports[ix], cmd)
  END PutCmd;


  PROCEDURE GetCmd*(ix: INTEGER; VAR cmd: Command);
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    DrainCmdPorts.Get(S.drainCmdPort.ports[ix], cmd)
  END GetCmd;

END DrainCmdPortsAdapt.

One procedure per direction the seam is used in, each handle-first where the store path it reaches is an array – ix selects the port instance – and beside each procedure its procedure type. An adapter over a single instance takes no handle: the procedure addresses the one Component by itself, and an index into a one-element array would select nothing; one adapter does it one way, all its procedures take the handle or none does. The type's shape carries the direction: a VAR result is a get, none is a put, a function result is a read. A System binds the procedure of the direction it declared into a runSystem formal of that type (System Modules, above), and binding the wrong direction does not compile. Both sides of the seam go through the adapter: the hosting partition's own commander puts through PutCmd, the print partition's drain gets through GetCmd, so that every access to the transport, from either side, is a procedure with a direction in its type. The adapter resolves the hosting store internally – the consumer imports the adapter and nothing of the hosting partition's store, not even the port module: the Command type is re-exported. Stateless, so everything it forwards is attributed to the calling System: a route, not a party – it appears in no manifest.

Preconditions

A sampling port has no capacity: a put and a get always succeed. A queueing port and a ring buffer have, and for them the precondition of every access is the caller's to meet: Put needs ~Full, PutMultiple(n) needs n <= Free, Get needs ~Empty, GetMultiple(n) needs n <= Count. The transport exports Free and Count so that the caller can meet them, asserts the precondition, and never clips, drops or corrects silently. The print partition's ring buffer, with the procedures the partition uses:

(* ECSKIND: RBUFFER *)
MODULE PrintBuffer;

  IMPORT RingBuffer, Errors;

  TYPE
    State* = RingBuffer.State;
    Value* = CHAR;


  PROCEDURE Init*(VAR state: State; buf: ARRAY OF Value; size: INTEGER);
  BEGIN
    ASSERT(size <= LEN(buf), Errors.ConsCheck);
    RingBuffer.Init(state, size)
  END Init;


  PROCEDURE Get*(VAR state: State; buf: ARRAY OF Value; VAR val: Value);
  (* precondition: ~Empty(state) *)
  BEGIN
    ASSERT(~RingBuffer.Empty(state), Errors.PreCond);
    val := buf[RingBuffer.GetIndex(state, 0)];
    RingBuffer.Release(state, 1)
  END Get;


  PROCEDURE PutMultiple*(VAR state: State; VAR buf: ARRAY OF Value; v: ARRAY OF Value; n: INTEGER);
  (* put the first n elements of v; precondition: n <= Free(state), n <= LEN(v) *)
    VAR i: INTEGER;
  BEGIN
    ASSERT((n <= LEN(v)) & (n <= RingBuffer.Free(state)), Errors.PreCond);
    i := 0;
    WHILE i < n DO
      buf[RingBuffer.PutIndex(state, i)] := v[i];
      INC(i)
    END;
    RingBuffer.Publish(state, n)
  END PutMultiple;


  PROCEDURE Free*(state: State): INTEGER;
  (* elements that can be put *)
    RETURN RingBuffer.Free(state)
  END Free;


  PROCEDURE Empty*(state: State): BOOLEAN;
    RETURN RingBuffer.Empty(state)
  END Empty;

END PrintBuffer.

Two reasons hold the standard. Putting less than given loses data, so the transport must never decide it. And every transport is single-producer single-consumer, so the caller's check-then-act needs no lock, also across cores: between the producer's Free check and its put only the consumer acts, and it can only increase Free.

The caller is the adapter, and the adapter is where the consequence of a precondition is decided (next section).

Observations in the Adapter Layer

Every observation about a transport – a clip, a dropped put, a queue found full – is recorded in the adapter: not in the transport, and not in the Systems. The adapter is the one place that knows both sides, the transport's interface and the partition's store. Where the event is a precondition the adapter meets, the adapter also detects it, as a by-product of the check it makes anyway; where a transport can detect an event the caller cannot foresee, the transport reports it through its interface, and the adapter reads the report and records it. Either way the adapter keeps the record. The print partition's buffer adapter meets the ring buffer's precondition and counts what it had to clip, in the partition's tally beside the buffer:

(* ECSKIND: ADAPTER PrintBuffer *)
MODULE PrintBufferAdapt;

  IMPORT CS := CSprint, PrintBuffer, Texts, Observations;

  TYPE
    PutMultipleProc* = Texts.PutStringProc;
    GetProc* = PROCEDURE(h: INTEGER; VAR ch: CHAR);
    EmptyProc* = PROCEDURE(h: INTEGER): BOOLEAN;


  PROCEDURE PutString*(ix: INTEGER; s: ARRAY OF CHAR; numChar: INTEGER);
    VAR S: CS.Store; free, failed: INTEGER;
  BEGIN
    S := CS.S;
    IF numChar > LEN(s) THEN numChar := LEN(s) END;
    free := PrintBuffer.Free(S.printBuf.bufs[ix].state);
    failed := 0;
    IF numChar > free THEN (* clipping observations *)
      numChar := free;
      failed := 1
    END;
    Observations.UpdateTally(S.printBufClip.tallies[ix], failed);
    PrintBuffer.PutMultiple(S.printBuf.bufs[ix].state, S.printBuf.bufs[ix].buf, s, numChar)
  END PutString;


  PROCEDURE GetChar*(ix: INTEGER; VAR ch: CHAR);
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    PrintBuffer.Get(S.printBuf.bufs[ix].state, S.printBuf.bufs[ix].buf, ch)
  END GetChar;


  PROCEDURE Empty*(ix: INTEGER): BOOLEAN;
    VAR S: CS.Store;
  BEGIN
    S := CS.S;
    RETURN PrintBuffer.Empty(S.printBuf.bufs[ix].state)
  END Empty;

END PrintBufferAdapt.

Three things to read off:

• The adapter is free to check and correct. It reads Free, clips, and calls the transport with what fits: the precondition met, the policy decided here, in the one place that knows both the transport's interface and the partition's store.

• The clip is an observation, taken where it is detected. It is recorded in a store variable of the partition, printBufClip.tallies, which a System of the partition collects and distils (Depositors and Collectors, below).

• A procedure type may be an alias. PutString exists to satisfy the framework's text writer, so its type is declared as that contract's type, Texts.PutStringProc, and the shape's origin is visible; the other two types are the adapter's own, the checkpoints for the drain System's signature.

The layering is a division of labour between three parties, and it is orthogonal: the transport detects what only it can see and notifies through its interface – a precondition it asserts, or an event it reports; the adapter handles – tallies, clips, distils; the System is impacted – data not available, a corrective action to take – and its manifest names the observation's token. Each can change without the other two moving: a transport can change what it detects, an adapter what it records, a System how it reacts. What the transport and the System are spared is the handling, which falls to the adapter alone.

The division has a consequence for the module kinds. A transport records no observation and so keeps the interface its kind names, a detection and reporting facility included where it has one; a System stays a function over the store; the adapter is the one module of the seam that is finished by hand. And it has a consequence for the manifests: the adapter appears in none, so the observation it records is attributed, like every access it forwards, to the calling System – the tally's token is in the manifest of the System that prints, written there as a store variable the System reaches through the adapter.

The layering reads as a rule: no observation about a transport is recorded in the transport, none in the Systems, all in the adapters.

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 belongs to a System. 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 observation it records included; the procedure types bound each access to its declared 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

Kinds: PARTITION, SCHEDULE, CONS

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:

(* ECSKIND: PARTITION Create AddSystems *)
MODULE BlinkPartition;

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

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

  PROCEDURE acquire;
    VAR S: CS.Store; i: INTEGER;
  BEGIN
    S := CS.S;
    i := 0;
    WHILE i < LEN(CL.L.ledLeader.pins) DO
      LEDext.Get(CL.L.ledLeader.pins[i], S.ledLeader.measureds[i]);
      LEDext.Get(CL.L.ledFollower.pins[i], S.ledFollower.measureds[i]);
      INC(i)
    END
  END acquire;

  PROCEDURE value;
    VAR S: CS.Store; i: INTEGER;
  BEGIN
    S := CS.S;
    i := 0;
    WHILE i < LEN(S.ledLeader.setpoints) DO
      S.ledLeader.setpoints[i]:= 0;
      S.ledFollower.setpoints[i] := 0;
      INC(i)
    END;
    i := 0;
    WHILE i < LEN(S.blinker.tickers) DO
      S.blinker.tickers[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.ledLeader.pins) DO
      LEDext.Put(CL.L.ledLeader.pins[i], S.ledLeader.setpoints[i]);
      LEDext.Put(CL.L.ledFollower.pins[i], S.ledFollower.setpoints[i]);
      INC(i)
    END
  END propagate;

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

  PROCEDURE AddSystems*;
  BEGIN
    Kernel.AddSystem(BlinkSystem.Run, BlinkSystem.Manifest, P.BlinkPeriod, BlinkSystem.Name);
    Kernel.AddSystem(CoupleSystem.Run, CoupleSystem.Manifest, P.CouplePeriod, CoupleSystem.Name);
    Kernel.AddSystem(ActuateSystem.Run, ActuateSystem.Manifest, P.ActuatePeriod, ActuateSystem.Name);
    Kernel.AddSystem(SenseSystem.Run, SenseSystem.Manifest, P.SensePeriod, 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.

A partition module imports nothing that says which schedule it runs on: AddSystems registers with the kernel, and the kernel registers into the context of the core that calls. The partition is placed by the schedule module that calls it, not by anything it contains.

Partition creations are mutually independent – no Create reads a peer's state – so the main program is pure composition. The main program of the program with one schedule, EcsControlSchedule-v26:

(* ECSKIND: SCHEDULE run *)
MODULE EcsControlScheduleV26;

  IMPORT
    Kernel, R, C, P, N, Main, PlanView, ErrConsole,
    BlinkPartition, PrintPartition, CoordPartition, MonPartition, AdaptPartition;

  PROCEDURE run;
    CONST Schedule = 0;
  BEGIN
    C.Assert;
    Kernel.Install(P.TickPeriod, R.ExcPrio_Systick, R.TimerHandle_Kernel, R.TimerUnit_Kernel);
    PrintPartition.Create;
    BlinkPartition.Create;
    CoordPartition.Create;
    MonPartition.Create;
    AdaptPartition.Create;
    Kernel.Begin;
    PrintPartition.AddSystems;
    BlinkPartition.AddSystems;
    CoordPartition.AddSystems;
    MonPartition.AddSystems;
    AdaptPartition.AddSystems;
    Kernel.Plan;
    PlanView.Report(ErrConsole.Werr, N.Names, Schedule);
    Kernel.Commit;
    Kernel.Run
  END run;

BEGIN
  run
END EcsControlScheduleV26.

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. C.Assert verifies the agreements between the partitions' definitions (The Consistency Module, below); Kernel.Install sets the tick, the tick's exception priority and the kernel's timer, all from P and R – an infrastructure claim, asserted at once; Kernel.Begin opens System registration. The sequence stands in a local procedure the module body calls, the form every schedule module shares (Schedules and the Boundary, below).

The Consistency Module

Where two partitions' definitions must agree, the agreement is asserted at one station of the main program, once, in the consistency module C:

(* ECSKIND: CONS Assert *)
MODULE C;

  IMPORT Wblink, Wcoord, Wprint, Wadapt, Vprint, Vadapt, Errors;

  PROCEDURE Assert*;
  BEGIN
    ASSERT(Wcoord.Periods_Num = Wblink.LedRole_Num, Errors.ConsCheck);
    ASSERT(Wprint.PrintBuf_Num = Wadapt.PrintBuf_Num, Errors.ConsCheck);
    ASSERT(Vprint.DrainSlowCmd = Vadapt.DrainInitialCmd, Errors.ConsCheck)
  END Assert;

END C.

The follower twins of the concepts document – a peer authoring its own copy of a fact it must agree on – are verified here, and the consistency module is the one module that imports several partitions' definitions, for that purpose only.

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 Create – 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 Create reads a peer's state, so the creations compose in any order, on any schedule.

• Every fact has one authority. The agreements between partitions' definitions are asserted once, in C, at the main program's consistency station; the consistency module is the one module that imports several partitions' definitions, for that purpose only.

• 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.

Schedules and the Boundary

Kinds: SCHEDULE, BOUNDARY

Overview

Everything above this chapter is schedule-agnostic: a partition's modules do not change when the partition changes schedule. This chapter adds the constructs that place partitions on schedules and let schedules share data: the schedule module of each schedule, the boundary module that declares what crosses between schedules, and the deployment facts a program with several schedules states.

The constructs of this chapter contribute to the following invariants:

• stores are partition-private; partitions meet only through transports;
• every Component instance has exactly one writer;
• structure is fixed at creation; steady state changes values;
• every fact has one authority;
• the operational invariants.

The Schedule Modules

A schedule module runs the station sequence of its schedule: consistency, deployment, installation, creation, registration, boundary, plan, report, commit, run. The schedule module of schedule 0 is the program's main module: it asserts the agreement of the definitions first, since a program whose definitions disagree has no business starting another core, and then starts the other schedules. EcsControlSchedule-v29:

(* ECSKIND: SCHEDULE run *)
MODULE EcsControlScheduleS0v29;

  IMPORT
    Kernel, C, R, P, N, B, Main, PlanView, Cores, ErrConsole,
    BlinkPartition, PrintPartition, CoordPartition, MonPartition, Core1Prog := EcsControlScheduleS1v29;

  PROCEDURE run;
    CONST Schedule0 = 0;
  BEGIN
    C.Assert;
    Cores.StartCoreOne(Core1Prog.Run, NIL);
    Kernel.Install(P.TickPeriodS0, R.ExcPrio_Systick, R.TimerHandle_Kernel, R.TimerUnit_Kernel);
    PrintPartition.Create;
    BlinkPartition.Create;
    CoordPartition.Create;
    MonPartition.Create;
    Kernel.Begin;
    Kernel.SetBoundary(B.Crossings);
    PrintPartition.AddSystems;
    BlinkPartition.AddSystems;
    CoordPartition.AddSystems;
    MonPartition.AddSystems;
    Kernel.Plan;
    ErrConsole.Claim;
    PlanView.Report(ErrConsole.Werr, N.Names, Schedule0);
    ErrConsole.Release;
    Kernel.Commit;
    Kernel.Run
  END run;

BEGIN
  run
END EcsControlScheduleS0v29.

Every other schedule's module exports its sequence as Run, which schedule 0's deployment station starts on the other core; its own first station configures that core's infrastructure:

(* ECSKIND: SCHEDULE Run *)
MODULE EcsControlScheduleS1v29;

  IMPORT
    Kernel, R, P, B, N, Main, ErrConsole, PlanView, AdaptPartition;

  PROCEDURE Run*;
    CONST Schedule1 = 1;
  BEGIN
    Main.ConfigC1;
    Kernel.Install(P.TickPeriodS1, R.ExcPrio_Systick, R.TimerHandle_Kernel, R.TimerUnit_Kernel);
    AdaptPartition.Create;
    Kernel.Begin;
    Kernel.SetBoundary(B.Crossings);
    AdaptPartition.AddSystems;
    Kernel.Plan;
    ErrConsole.Claim;
    PlanView.Report(ErrConsole.Werr, N.Names, Schedule1);
    ErrConsole.Release;
    Kernel.Commit;
    Kernel.Run
  END Run;

END EcsControlScheduleS1v29.

The two sequences are the same sequence. What differs is the deployment station – Cores.StartCoreOne on schedule 0, Main.ConfigC1 on the others – and the consistency station, which runs once, on schedule 0. Each schedule module installs its own tick period and registers its own partitions; each reports its own plan. Moving a partition from one schedule to the other is moving its Create and AddSystems calls from one schedule module to the other, and its periods in P to the other tick – four program-level files, no partition file; the how-to gives the prescription.

The main program of the program with one schedule (The Main Program and the Partitions, above) is this sequence with the deployment station and the boundary station absent.

The Boundary Module

Where schedules exchange data, the program declares the crossings once, in the boundary module B. It is a definition module: one record, assignments, no procedures. EcsControlSchedule-v30:

(* ECSKIND: BOUNDARY Crossings *)
MODULE B;

  IMPORT Kernel, Tprint, Tadapt, Tcoord;

  CONST
    S0 = 0; S1 = 1; (* schedules *)

  VAR
    Crossings*: Kernel.Crossings;

BEGIN
  CLEAR(Crossings);
  (* from -> to *)
  Crossings.flow[S0, S1] := Tprint.I.clipsObs;
  Crossings.flow[S1, S0] := Tadapt.I.drainCmd + Tcoord.I.readPeriods
END B.

The observation surface flows from schedule 0 to schedule 1; the command surface and the period surface flow back. A crossing names surfaces only, never a token: what a partition publishes is what may cross, and the rule is the same for a partition boundary and a schedule boundary. The kernel keeps the record, two matrices of token sets over schedule pairs:

Crossings* = RECORD
  flow*: ARRAY NumSchedules, NumSchedules OF SET;    (* flow[from, to]: dataflow tokens, P -> C *)
  deposit*: ARRAY NumSchedules, NumSchedules OF SET  (* deposit[from, to]: deposit tokens, Px -> Cx *)
END;

Every schedule module passes the same record to Kernel.SetBoundary, and the kernel derives from it this schedule's view of the others: a manifest in which what the other schedules produce for this one appears as produced, and what this one produces for them appears as consumed. Against that manifest this schedule's plan is checked like any other (The Kernel, below): a token produced here and declared as flowing elsewhere thereby has its consumer, a token consumed here and declared as flowing in has its producer, and a token written on two schedules is found after every schedule has planned.

Deployment Facts

Every program states two facts about its deployment, both outside the partitions:

• The number of cores, in the memory map: the kernel sizes its per-schedule contexts by MemMap.NumCoresUsed, and the map allocates each core's stack, heap and vector table. The framework's memory map for the RP2350 serves both cores. A program with one schedule carries its own memory map, with NumCoresUsed* = 1, so that the kernel keeps one context and the second core's memory is not reserved: EcsControlSchedule-v26 has its own MemMap module beside its definition modules.

• The reach of peripherals: a partition on another core uses the devices its Systems need from that core. On the RP2350 both cores reach every peripheral alike, except the ones on the private peripheral bus, which are per core; the how-to lists what to verify on a chip where they do not.

The Error Console

A program has one single terminal for its errors and diagnostics, but possibly two cores that may want to write to it. The framework module ErrConsole implements the terminal: one UART, one writer handle Werr, shared by the cores, with a hardware spinlock behind it. Schedule 0's start-up installs it by importing Main, the other schedule via Main.ConfigC1. ErrConsole implements claim, release, and reset procedures, of which it plugs claim and reset into the corresponding braces of RuntimeErrorsOut so that a run-time error report from either core claims the error console before printing.

The Claim and Release procedures of ErrConsole can also be called explicitly from the program to brace diagnostic messages that must not interleave with the other core's, as shown for the PlanView.Report output above. A program using one core does not need the braces.

Note that ErrConsole is strictly reserved for diagnostic and error messages. It employs simple busy-waiting for FIFO-full conditions to ensure that the message will be printed also under error conditions, but this will most likely disturb the schedules' timings. A program that needs terminal output as part of its normal execution should implement a non-blocking print service, as the example programs do.

Contributions to Invariants

• Stores are partition-private; partitions meet only through transports. The boundary adds a second cut on the same seam: a schedule boundary passes surfaces, which are transports, and nothing else; a partition's module set does not change when its schedule does.

• Every Component instance has exactly one writer. The boundary's derived manifest extends the check across schedules: a token written on two schedules is found when every schedule has planned.

• Structure is fixed at creation; steady state changes values. The station sequence is creation's order, the same on every schedule.

• Every fact has one authority. The crossings are declared once, in B, and read by every schedule module.

• The operational invariants. Each core's infrastructure is configured by its schedule module's first station before anything else runs on that core.

Depositors and Collectors

Overview

The deposit sets carry the shared facilities. Of the concepts document's two facility kinds, EcsControlSchedule 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 belongs to a System.

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.printBuf.bufs, L.printBufClip.tallies};

A participant declares the surface wholesale – the monitoring partition's heartbeat system:

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

Px is the one deliberately multi-writer set – 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.printBuf.bufs}), the observation distiller collects the tally (Cx := {T.L.printBufClip.tallies}) – the tally the buffer adapter keeps on every deposit (Ports and Adapters, above).

All depositors of a facility run on one schedule. What makes the multi-producer sound is the schedule as the mutual exclusion, and nothing else: the architecture excludes locks on Components altogether, within a schedule and across schedules alike. Systems run synchronously within their schedule, the kernel synchronises the schedules at creation only, and across the boundary the only coordination is a transport's protocol – one producer, one consumer, data published and read; a facility coordinated across schedules would need a lock, which is exactly what the architecture excludes. Depositors on two schedules would be two concurrent writers of one transport, which no protocol here allows. A facility whose participants sit on both schedules is therefore two facilities, one per schedule, each collected on its own; a collector may sit on the other schedule, since the collector is the facility's single consumer – that is a deposit crossing, declared in the boundary's deposit matrix. The kernel's cross check covers the single-writer sets O and P, not Px: that every depositor of a facility is on one schedule is a review item.

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 belongs to a System. 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 still belongs to the System.

Bindings and Handles

Kinds: BINDING, OTHER

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. Beside them stand the other modules: program modules of no kind the architecture names.

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, configured at the partition's creation and operated by its Systems: UARTbinding configures the drain UART and its pins, UARTdrain writes to it. A binding is configured, never informed by import: it imports device modules and nothing of the definition, and every fact it needs – the handle, the pins, the baudrate – arrives as a parameter from the partition's creation code, which draws it from R, V and CL under fact authority. The LEDs are driven through the framework's board module LEDext, whose pins R names.

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.bufDrain.uartHandles[0] := 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.bufDrain.uartHandles[W.Ix_PrintBuf_Term], 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.

Other modules are the program modules of no other kind: EcsControlSchedule-v26's own memory map (Schedules and the Boundary, Deployment Facts) is one; a helper the Systems of a partition share would be another. The definition places such a module and says nothing further about it. Like a binding, it is configured and never informed by import: a fact it needs arrives as a parameter – a value, a handle, a procedure, never an array length or a type – which keeps a helper portable between programs; a helper that would need a W cardinality for a declaration is playing a role that belongs in CS or CL.

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, once per schedule: registers Systems, checks the manifests, derives the run order, runs the tick loop – over a context per schedule, selected by the core that calls, so that every procedure of its interface acts for the calling schedule. Its state is readable, never writable, from outside; it prints nothing and does not know a terminal exists. One token space serves all schedules, 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 of the schedule 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 manifest the boundary derived for this schedule (Schedules and the Boundary, above) takes part like any other.

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.

The last two checks are the cross checks. With several schedules Plan has a second half: after its own plan the schedule waits until every schedule has planned – a rendezvous, two words per schedule and no further kernel state – and then checks its aggregates against the other schedules'. No schedule proceeds to Commit before every schedule has planned.

Commit is the gate's final station – three assertions: the kernel's timer is bound, a plan exists, and no unrelaxed check failed. A rejected plan is a hard fault with its own error code – a static construction fault, never retryable.

The Plan Report

The report is inserted, it never restructures. Between Plan and Commit, a schedule module may add one call: PlanView.Report prints its schedule's manifests, crossings, dependency list, derived order, and every violation by name – in store-variable vocabulary: the token definitions of the Tx modules, aggregated by N. With several cores the call stands between the error console's claim and release, so that the two schedules' reports do not interleave.

The reports EcsControlSchedule-v30 prints at every start, one per schedule – the coordination and the adaptation partition on schedule 1, the other three on schedule 0, and three surfaces crossing (the boundary module B above):

Kernel.Plan schedule: 0
manifests (registration order):
S0 Drain
   Cp:
     drainCmdPort.ports
   O:
     bufDrain.tickers
   Cx:
     printBuf.bufs
S1 PrintClip
   O:
     clipsDistiller.accounts
   P:
     clipsObsPort.ports
   Cx:
     printBufClip.tallies
S2 Blink
   C:
     periodPort.ports
   O:
     blinker.tickers
   P:
     ledLeader.setpoints
S3 Couple
   Cp:
     ledLeader.setpoints
   P:
     ledFollower.setpoints
S4 Actuate
   C:
     ledLeader.setpoints
     ledLeader.measureds
     ledFollower.setpoints
     ledFollower.measureds
S5 Sense
   P:
     ledLeader.measureds
     ledFollower.measureds
S6 TickMonitor
   Px:
     printBuf.bufs
     printBufClip.tallies
S7 Heartbeat
   O:
     heartbeat.status
   Px:
     printBuf.bufs
     printBufClip.tallies
schedule crossings:
   P there, C here:
     periodPort.ports
     drainCmdPort.ports
   P here, C there:
     clipsObsPort.ports
dependencies (registration order):
S0 Drain
     TickMonitor
     Heartbeat
S1 PrintClip
     TickMonitor
     Heartbeat
S2 Blink
     Couple
S3 Couple
S4 Actuate
     Blink
     Couple
     Sense
S5 Sense
S6 TickMonitor
S7 Heartbeat
derived scheduling order:
 0 Couple
 1 Blink
 2 Sense
 3 Actuate
 4 TickMonitor
 5 Heartbeat
 6 Drain
 7 PrintClip
plan checks: all pass

Kernel.Plan schedule: 1
manifests (registration order):
S0 AdaptDwell
   C:
     clipsObsPort.ports
   O:
     clipsAdapter.runs
   P:
     drainCmdPort.ports
S1 Period
   O:
     mission.periodStep
   P:
     periodPort.ports
schedule crossings:
   P there, C here:
     clipsObsPort.ports
   P here, C there:
     periodPort.ports
     drainCmdPort.ports
dependencies (registration order):
S0 AdaptDwell
S1 Period
derived scheduling order:
 0 AdaptDwell
 1 Period
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); Drain's command arrives from the other schedule, consumed as the previous pass's value. The crossings are readable too, by their tokens: schedule 0's report lists the observation port as produced here and consumed there, and the command port and the period port the other way round, so that Blink's dependency on Period has no edge in schedule 0's plan – its producer runs on schedule 1, and the crossing stands in for it; schedule 1's report shows the mirror image, with AdaptDwell and Period in its order and no edge between them. Because Plan collects everything before Commit gates, a broken program reports all its violations in one run, before the fault; each schedule module reports its own plan, after every schedule has planned.

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. The report call and the Relax call are the two optional lines of the station sequence; a waiver in force is a fact of the program the review reads, and Plan and Commit appear identically with and without them.

The Tick

Steady state is one loop per schedule: sleep until the tick, then run every System once, in the derived order, to completion. Each schedule runs on its own core, with its own tick and its own period; within one schedule, nothing needs a lock, and nothing has one. The kernel's timer is one, shared: schedule 0's installation binds it, every schedule reads it, so that pass times and timestamps are comparable across cores.

Run is the last station. It locks the schedule first – from then on, every station procedure (Install, Begin, AddSystem, SetBoundary, Relax, Plan, Commit) refuses with an error, and so does the report's access to the plan: no configuration after Run. It then waits until every schedule has committed, the second rendezvous, before it enables the tick: no schedule runs before every schedule may.

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.

Open and Locked

The kernel has two states, and Run is the transition. Open, from load until Run: the station procedures – Install, Begin, AddSystem, SetBoundary, Relax, Plan, Commit – accept calls, and the world is created, registered, planned and committed. Locked, from Run on: every station procedure refuses with an error, the plan is no longer readable through GetRunCtx, and the only procedures that answer are the ones that query defined kernel data – TickTime, TickPeriod, TickCount, ElapsedTicks, MissedTicks. The lock is per schedule, set by the schedule's own Run; it is never released, since nothing after Run is entitled to configure.

The kernel's lock is one instance of a general shape: a resource is open during world creation and locked for steady state, with the lock set by the last station that configures it. The same shape is available at other levels, and each level has its own means:

• direct hardware locking: a chip may offer lock bits that, once set, can only be cleared by a reset – on the STM32 several configuration registers lock this way; the driver sets the bit as its last configuration step, and the hardware refuses every later write;

• indirect hardware locking: where the chip offers no lock bit, the driver holds the lock in software and refuses configuration calls after it, as the kernel does;

• software locking of the program's own resources: Memory.LockHeaps closes the heaps after creation, so that a NEW in steady state yields NIL and the assertion that follows every NEW fails – "creation is NEW's only home" enforced rather than reviewed.

The kernel's lock is not the program's to take or leave: Run sets it, in every program. The other levels are open: which resources lock, by which means, and whether a module locks itself at its last configuration step or exports an explicit lock are design questions not yet settled, and the evaluation programs exercise none of them.

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 set-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 Run locks it – after the gate the System set is closed, and the kernel implements steady state with no way to add, remove, or reorder Systems, nor to call any station procedure again.

• Groundwork. All kernel state is readable through its access procedures, never writable – the kernel is a sensed device, which is what lets monitoring arrive as ordinary Systems – and the printed plan is per-run evidence: manifests, crossings, 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. The matrix in data form is the library's allow-lists file: one group per kind, in the ECS file's notation, which the import check-points of the review guide read against and the tools load; a project may keep a copy of its own, reviewed as a diff against the library's. Library modules stand outside the matrix: an import of one is recorded in the ECS file, never judged.

One consequence of the matrix is worth naming: infrastructure modules appear in the schedule modules' import lists and nowhere else. The start-up anchor must be imported there (importing the framework's Main is what places the program start-up ahead of everything), each schedule module's first station is the only configuration of its core's infrastructure, 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 infrastructure modules are library modules, which the tools record and never judge, so the reviewer holds this reading alone.

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 our programs; the tick monitor observes the kernel, a framework module read as a sensed device --, and Systems can print to the error console.

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 the schedule modules' import lists only; 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 on each core, before its schedule module'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 – 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.

• Procedure types – an adapter's procedure type carries the direction of a store access by its shape; a System's formal of that type accepts only a procedure of that direction, and the type may be an alias of a library contract's type where the procedure exists to satisfy it.

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.

• A record of sets over schedule pairs – the boundary as values, from which the kernel derives each schedule's view of the others; the same set operations check it.

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: The ECS File
• EcsControlSchedule
• ECS for Control: Schedules
• ECS for Control: Review Guide
• ECS for Control: check-ecs
• ECS for Control: extract-ecs
• ECS for Control: Observations – Concepts

Last updated: 2 November 2026