Added the ZoneX Phase-0 partitioning demonstrator - #5
Merged
Conversation
ZoneX started as a repository with four files and no code. This is everything that has to exist before the hypervisor can be written: the build system, the C17 baseline, the verified Armv8-R EL2 register sheet, the recorded design decisions, and CI that runs from the first commit. No hypervisor logic is here, deliberately. Every translation unit is empty of implementation and every one of them compiles, so the change that writes the code opens a tree that already configures, builds and links in five configurations. Writing any of it earlier would have meant writing it against register names nobody had checked, and terminology bleed -- AArch64 spellings on an AArch32 core, an A-profile hypervisor shape on an MPU-only architecture -- is the single easiest way to get this architecture wrong. docs/armv8r-el2-reference.md is the answer to that. Every line in it was read out of the Cortex-R52 TRM or measured on the part, and each carries its source. Two things it settles that matter for the design. There is no HPRBAR.AP encoding that grants a guest access while denying EL2, so isolation between partitions can only come from which regions are enabled while a partition runs, never from the permission bits. And HSCTLR.BR=1 gives EL2 the background map for its own accesses while EL0/EL1 misses still fault regardless of BR, so ZoneX spends no regions on its own code and data -- which matters when the hypervisor's own mapping and every guest's stage-2 mapping share one 20-entry region set. BR grants permission, not attributes, and that distinction is recorded because the model hides it. Table 8-4 fixes the background map as Normal cacheable below 0x60000000, and the S32Z280's console sits at 0x4298_0000 -- inside it. So the hypervisor needs Device-attributed regions for its own console and GIC even with BR set. On the FVP those devices land in the Device band and the background map is accidentally correct, so a green model run cannot show that the regions are missing. It is the same shape as the region-count trap, and both are written down for that reason. It also closes one of two documented ambiguities. The TRM's section 3.3.48 says direct access stops at HPRBAR15; section 8.4 lists HPRBAR16-HPRBAR24 at opc1 = 5 and the register summary agrees. So the EL2 MPU avoids the penalty measured at EL1 for high regions -- 542-604 cycles through PRSELR against 434-470 direct -- and the whole budget is directly addressable. The HPRENR width question stays open: the TRM contradicts itself and only the part can settle whether a bit above 15 is honoured or merely stored. ZoneX is built to C17 with extensions off, the first component of the suite born on that baseline rather than migrated to it, and the strict warning set is in place from here rather than from a later hardening pass. Both are cheaper now than later: retrofitting a codebase to a warning set costs far more than building to one, and the certification back end for ZoneX is funded. CI exists before there is anything to run, for the same reason. The FVP workflow builds and executes; there is no static check for "the partition still runs", and ThreadX added its equivalent eight years in, after a period where nothing in CI ran a single instruction of any port. Every workflow triggers on pull requests against dev and main and on pushes to both -- ci_cortex_m.yml ran on master only while dev was the integration branch, so it gated no pull request anybody opened and the ports drifted for eight months. scripts/check_terminology.sh is the mechanical half of the terminology argument. It rejects the register and concept names that belong to other architectures, and it runs as its own CI job so its answer is unambiguous. Its one exception is deliberate: a suite build option may legitimately end in _EL1 -- TX_R52_BOOT_AT_EL1 is the ThreadX option that builds a guest starting there, and the guest work has to name it repeatedly -- while an AArch64 system register never carries a component prefix, so requiring the absence of one separates the two. CONTRIBUTING.md's "Building and testing" and "Continuous integration" sections described a repository with neither. They now describe what is here. Its C99 line is corrected to C17 for ZoneX, the sentence implying a PowerShell script set is qualified -- Phase 0 is Linux, FVP and silicon, and an untested build_host.ps1 would be a promise the project cannot keep -- and its section on agent-instruction files is replaced by one that does not claim a file this repository does not carry. No other Eclipse ThreadX repository ships agent instructions, and this one does not either; CONTRIBUTING.md is the single authority, and it now says what to point an agent at. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
An EL2-resident ZoneX now programs stage-2 MPU regions, drops to EL1, and a stage-2 violation by the EL1 payload is taken to EL2, decoded and reported by name -- on the Armv8-R AEM FVP and on S32Z280-594EVB silicon. Nothing else in Phase 0 was worth building until that worked, because everything else assumes it. There is still no ThreadX guest, no partition manifest and no scheduler. The image is one EL2 program, one trivial EL1 payload and one deliberate fault, shared between both targets so that the same program answers the same questions on a model and on a part -- which turned out to matter more than expected. WHAT IT SETTLED HPRENR really is wider than 16 bits. The TRM's prose says regions 0 to 15 and its own bit tables say [19:0] for 20 regions; the tables are right. The S32Z280 implements exactly [19:0], and -- proven functionally rather than by reading the register back -- a bit above 15 genuinely disables its region: an EL1 read of the granule region 16 covers succeeds with the bit set and takes a stage-2 fault with it clear. A register that accepted the bit and ignored it would have passed a read-back test and made a one-write partition switch silently leave the outgoing partition's regions live. Regions above 15 are directly addressable at opc1 = 5, confirmed on both parts by programming region 16 directly and reading it back through the selection register. So the EL2 MPU avoids the 542-604 cycle penalty measured at EL1 during the Cortex-R52 Modules port work for reaching a high region. HPFAR does not mean the same thing on the two targets. The TRM describes it two ways in one section -- FIPA[39:12] at HPFAR[31:4] in its figure, "bits [31:4] of the faulting address" in the table beside it -- and the FVP implements the first while the S32Z280 implements the second. The two differ by a factor of 256 and each is plausible alone, so there is no portable decode of HPFAR here. ZoneX uses HDFAR, which carries the full faulting address on both. The fault report prints HPFAR raw, computes both readings and names which one the target implements, because the divergence is a fact the next person needs. The FVP implements an EL2 MPU and reports 32 regions at both stages, which is not an architecturally legal Cortex-R52 value -- so a green model run still proves nothing about a real part's budget. The image says so in its own output. THE ONE THAT CHANGED THE DESIGN HSCTLR.BR grants permission, not attributes, and on the S32Z280 that bites before the hypervisor can print anything. Reached through the background map, LINFlexD_9 at 0x42980000 is Normal Write-Through memory, and Normal memory reorders and gathers even with caches off -- which corrupts a polled UART's register protocol. The first version printed its whole identity block as legible-but-wrong text, looking exactly like a marginal baud rate. So enabling protection is two steps, not one: the hypervisor's own MMIO regions and HSCTLR.M come up before the console, and HCR.VM only after the partition regions exist. zx_stage2_enable refuses to set HCR.VM while HSCTLR.M is clear, because that combination would run a guest unprotected while every check appeared to pass. HOW A FAULT COMES BACK zx_el2_run_payload saves EL2's context, ERETs to EL1, and does not return through that ERET; the trap handler resumes the saved context with a result code, so a guest fault reaches the hypervisor as a value rather than as a jump into a handler with no context to decide policy in. That is also what lets one run demonstrate several violations instead of only the last one. A fault taken FROM Hyp mode is the exception and reports differently: its own vector, EC 0x25 rather than 0x24, its own message and its own exit code. It has been provoked deliberately on both targets, because a hypervisor bug reported as a partition being stopped at its boundary is a run that passes while proving nothing. EVIDENCE THAT IT CAN FAIL Three builds of the same image, two of which must fail and are registered WILL_FAIL in CTest: the deliberate violation aimed at an address the payload IS granted, and the image told it needs more regions than exist. Both have been seen to fail on both targets, naming what went wrong. The deliberate-EL2- fault build is not registered, because its expected outcome is a failure report and a suite taught to accept that would accept it everywhere. The host suite covers the fault decoder to 100% of its lines, asserting on real syndromes captured from both targets -- including the HPFAR divergence, so a later simplification back to one reading breaks the build. Also fixed along the way: the two example options are now mutually exclusive, because the board's reset state and console are properties of the port library and a PRIVATE definition on an image never reached it -- which had produced an S32Z280 image with an A32 entry point and a semihosting console that built, linked and would have printed nothing. The gcc and clang lanes now build the images rather than only the libraries, since images are EXCLUDE_FROM_ALL and a compile error in one was slipping past both. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The two negative FVP tests could pass for the wrong reason. CTest's
WILL_FAIL inverts the exit status and nothing else, so it could not
distinguish the outcome the suite wants -- the image ran and reported its
own failure -- from the ones it does not: the image was never built, the
model would not start, or the run hung. All of those exit non-zero, and
WILL_FAIL called all of them passes.
The images are EXCLUDE_FROM_ALL, so this was reachable from a clean tree:
with them unbuilt, `ninja && ctest` reported zx-fvp-probe-negative and
zx-fvp-probe-starved as Passed on "application file not found" -- two
green lines asserting nothing whatever about stage 2. A negative test
that passes because nothing ran is worse than no test, because it is
counted. CI was not affected; it names the images as build targets
before running the suite.
The runner now takes --expect {pass,fail} and judges the verdict itself,
and checks the image exists before launching the model. The property
WILL_FAIL was chosen for is kept: a negative build that starts PASSING,
meaning the violation stopped being detected, still fails the suite.
Verified in all three directions: with the images absent all three tests
fail; with them built all three pass; and pointing --expect fail at the
positive image fails by name.
Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Several comments cited a numbered section of a planning document that is not in this repository. The facts were fine; the citations were useless to anyone reading the repository, since that document is not here to read, and they date badly besides. Each one is reworded to keep the fact and drop the reference. The check is the actual fix. These went in one at a time while the work was fresh, and a manual sweep is what let them through -- it looked for absolute paths but not for a citation, and would have missed the hyphenated spelling even if it had. scripts/check_references.sh now rejects local absolute paths, numbered references to documents that are not present, and a tracked agent-instruction file, with the same skip-marker convention as the terminology check. It found the hyphenated one immediately. It runs in CI beside scripts/check_terminology.sh, in the same job and with if:!cancelled() so that one push reports both checks' findings rather than one per re-run. Deliberately narrow: a check that cries wolf gets bypassed. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The manifest is the user-facing contract of a ZoneX system, so this change is mostly about which vocabulary it is written in. ZoneX adopts the suite's own integer type names -- the eight typedefs every ThreadX port carries -- rather than spelling the manifest in <stdint.h> terms. The suite-wide C17 upgrade settles the question: it changes no struct layout, no calling convention and no type name, and it regression-tests that a C99 application still compiles against the new headers, which makes those names load-bearing for that promise and therefore permanent. A manifest written in uint8_t would make ZoneX the one component of the suite whose contract used a different vocabulary, for no gain. Addresses stay zx_addr_t: ULONG is not pointer-width on every ABI the suite targets. ZoneX keeps its own copy of the typedefs rather than reaching for tx_port.h, because a manifest has to be readable with no ThreadX checkout in sight; the copy is deliberately unguarded so that a divergence is a hard error at the include rather than a quiet one. The attribute fields are UCHAR and not an enum, and that was measured rather than assumed: a four-value enum is 1 byte under arm-none-eabi-gcc, which uses AAPCS short enums, and 4 bytes under ATfE clang and on the host. ZoneX builds with all three, so an enum field would give the manifest a different layout in each lane. The descriptor's layout is now asserted -- the four attribute bytes consecutive in every lane, and the whole descriptor pinned to 12 bytes on a 32-bit port, so that a change in either target toolchain fails the build instead of producing two images that disagree. The shared-memory type carries the reasoning it needs. Phase 0 shares one read-only granule so the demonstrator has a positive channel to show rather than only proving isolation by what faults, and a single region cannot express it: stage-2 AP belongs to a region, not to a partition, so the publisher covers the granule writably and each reader read-only. Those ranges coincide, which is safe only because one partition runs at a time -- exactly the kind of reasoning that must be written down. What it weakens and what it does not is stated on the type. The region descriptor and the AP/SH/XN encodings move out of the port header into the manifest, because the host-side validator has to build and check the same objects with no Cortex-R52 header in reach. Nothing in assembly used them, which is what made the move free. The port keeps the field positions they shift into and the HMAIR byte layout, which is this port's choice rather than an architectural fact. Also carries three of the reference rewordings from the previous commit, in the three files that changed for both reasons. Verified: both repository checks, the host suite, and the FVP suite under GCC and ATfE clang, plus S32Z280 builds under both toolchains. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
D19 records why the manifest uses the suite's own type names with zx_addr_t for addresses, including the measurement that settled the attribute fields: a four-value enum is 1 byte under arm-none-eabi-gcc and 4 under ATfE clang and host gcc, so an enum in a published struct would give each build lane a different layout. D12 is corrected rather than extended. It claimed ZoneX "is the reference implementation of the suite-wide C17/CMake plan rather than an exception to it." The plan makes no such claim -- it states it is independent of this roadmap and asks only that ZoneX start directly in C17 with the capability macros -- and ZoneX is in fact an exception on one point: the plan proposes extensions off in the CI preset and on in the default build, while ZoneX has them off in the default build. That is stricter and worth keeping, but it is a deviation, and the entry now says so. The claim mattered: it was load-bearing in an argument for spelling the manifest in <stdint.h> terms before anyone checked it. CONTRIBUTING.md and the pull request template gain the new reference check, with a note on what a comment may cite. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Almost nothing that can be wrong with a manifest faults, which is the reason this function exists. An under-aligned base does not abort: its low bits land on the SH, AP and XN fields and silently change the region's attributes. An unmasked limit lands on AttrIndx and selects an unwritten MAIR byte, which reads as Device-nGnRnE -- memory that works, slowly, and passes a careless test. Two enabled regions covering one address is CONSTRAINED UNPREDICTABLE. A wrong entry point by four bytes costs a hardware session to find. The defects worth catching are exactly the ones with no symptom, so they have to be caught before the regions are programmed rather than debugged after. One error code per rule, and the fault record carries TWO locations rather than one: the overlap rules have two offenders, and naming only one leaves the reader hunting for the other. Unused index fields hold an explicit sentinel, because zero is a valid partition and region index and a zeroed field would be indistinguishable from a real one. The validator is pure and takes the facts it cannot know -- the hypervisor's MMIO regions, which MAIR bytes were actually written, the region budget -- as an argument. That is what lets one function serve both callers: the host suite hands it values and gets coverage, the boot path hands it the real HMPUIR. The cross-partition overlap rule is waived only for a pair of regions that BOTH exactly cover the same declared shared range. Exact, because waiving it for anything merely touching a declared range would turn one published granule into a licence to overlap around it. The shared declaration and the regions are also checked against each other: a range declared read-only whose reader was given a writable region would be a two-way channel described as one-way, and both partitions would simply work. 150 checks. Every error code has a case, every case asserts the reported indices as well as the status, and the arithmetic has its own: adjacent regions that touch are legal and must not be rejected, a one-granule region is the smallest legal one, and ranges at the top of the address space must not wrap -- which is why the overlap test is two comparisons and computes nothing. 100% line and branch coverage on the validator. Two harness fixes came out of getting there: The coverage report was stale. gcov ACCUMULATES into .gcda files, and nothing deleted them, so a second run over the same build tree reported the union of both and coverage could only ever appear to rise. Measured: with one rule's tests disabled the report still said 100% and the new floor still passed. CI never saw it because every run is a fresh checkout -- the machine getting the wrong answer was the contributor's, asking whether their own change had dropped coverage. The counters are now deleted before the instrumented run. And the floor itself is enforced, scoped to the validator rather than set repository-wide: much of core/ is only true on hardware and the host suite cannot reach it, while a floor pinned to whatever the tree measures today would assert nothing about the code. Verified to fail, at 97.5% with a rule's tests removed, and to name the uncovered lines. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
THE READBACK. At stage 2 the alignment bugs fail in the attributes and not in the address: a base one byte past a granule boundary does not fault, because its low bits ARE the SH, AP and XN fields. The region is programmed successfully with permissions nobody asked for, and runs, and nothing ever reports it. zx_stage2_region_readback decomposes a programmed region back into the descriptor a manifest would have declared, and zx_stage2_region_matches compares one against its intent. The EN bit is deliberately not decomposed: a manifest declares what a region IS, while whether it is enabled belongs to the running system. Folding it in would make a region read back unequal to the one written purely because a different partition is current. THE SWITCH. zx_stage2_enable_set replaces the whole HPRENR mask in one write with ONE barrier pair, DSB before ISB. That order is load-bearing: issuing the ISB before the write has retired would let the following fetch be permitted under a mask no longer in force, which is a partition briefly running with its predecessor's memory. The direct region encodings above index 15 are NOT generalised, and that is a decision the measurement enables rather than an omission. The 542-604 against 434-470 cycle figure only applies if regions are reprogrammed per switch; with fixed blocks and mask switching they are programmed once at boot, so unrolling 25 indices -- coprocessor register numbers must be compile-time constants, so it means roughly a hundred inline MCR/MRC statements -- would speed up an operation that happens once. The barrier policy for the switch path now lives in one function, because "how long does a partition switch take" needs an answer that is not assembled from three files. THE PLANNER. zx_mm_plan turns a manifest into a region-index layout and a set of HPRENR images, and touches no hardware: the caller walks the plan and does the writing. The split is what makes the interesting part -- which index each region lands on, which bits each mask carries, whether the total fits the part -- reachable from a workstation. Passing the programmer in as a function pointer would have kept one function at the cost of an indirect call on the switch path. Fixed blocks rather than packing, so a switch is one register write for any manifest instead of a loop whose length depends on the incoming partition. The hypervisor's MMIO occupies the lowest indices and is enabled in every mask, because a partition switch must not blind the hypervisor's own console. The layout is printed once at boot. Every later fault report names a region INDEX, and the same index is a different window on the two targets -- the model spends none of them on hypervisor MMIO and silicon spends two -- so without the printout a diagnostic cannot be mapped back to the manifest. Tests assert the exact mask patterns and then the property behind them: no two partitions' masks share a bit outside the always-on block, and every mask carries that block. The patterns catch an arithmetic slip; the property catches a redesign that is internally consistent and wrong. On hardware the symptom of a wrong mask is that everything works. The coverage floor now covers the planner as well as the validator, both at 100% line and branch, and was re-verified to fail when a rule's tests are removed. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
TWO PARTITIONS, BOTH DIRECTIONS. A run in which partition A reaches
its own memory and faults on B's is equally consistent with B's memory
being mapped by nobody, which is not isolation but an empty address
space with one tenant. So both directions run: B then executes, in its
own memory, and faults on A's. The same address is reachable in one
region set and unreachable in the other, which is what a partition
switch is.
Measured on the model: cross-partition probes fault with DFSC 0x04, no
enabled region covering the address, and the refused write to the shared
granule faults with DFSC 0x0C -- a region matched and its AP said no.
Distinguishing those two was the point of checking the status code
rather than the fault alone: "read-only" and "not mapped here" are
different claims and only one of them describes a shared granule.
The adjacent granule carries more weight than the neighbour does.
Faulting on the other partition's data proves the sets differ; two sets
a kilobyte apart would prove that too. The ungranted granule sits
immediately after partition A's data window, by linker-script
construction and with an ASSERT to keep it there, so touching it is what
says the LIMIT is exact.
A RELOCATABLE GUEST BLOB. Two partitions cannot run the same program in
different memory while its data addresses live in literal pools, so the
blob takes its data window base in a register and reaches everything at
a fixed offset from it. Nothing to relocate: branches were already
PC-relative, a literal holding a constant survives the copy, and a
literal holding an ADDRESS is what the base pointer removes -- there is
not one in the section. EL2 copies the blob into each code window,
which is the path a real guest image takes, so the manifest's image
bounds and the IMAGE_TOO_LARGE rule are load-bearing now rather than
hypothetical.
Entry points sit at declared offsets because the hypervisor computes
them as window_base + constant. .org places them, and .org refuses to
move backwards, so a routine that outgrew its slot fails the assembly
instead of silently displacing the next entry point. The obvious
alternative -- a .space guarded by ".if (. - blob_start) > offset" --
assembles under GNU as and is rejected by LLVM's, which will not treat a
label difference as absolute before layout. ZoneX builds with both.
THREE NEGATIVE VERIFICATIONS, each its own image because they fail at
different points and one image would only show whichever came first:
widened a region limit one granule too generous, swallowing the hole.
The manifest is VALID -- covering the hole breaks no rule --
and only the runtime probe catches it, which is the clearest
statement of why both layers exist.
overlap two partitions' data windows on one address. Refused with
PARTITION_OVERLAP naming both offenders, before a single
region is programmed.
badattr a region naming an HMAIR index this image never wrote.
Refused with ATTR_NOT_WRITTEN. The hardware would not
object: the region gets Device-nGnRnE and works, slowly.
THE PMU, so a switch can be measured rather than estimated. The generic
timer is not usable -- CNTFRQ reads zero on both targets -- and cycles
are the unit a WCET argument is made in anyway.
PMCCFILTR is under CRn = c14, not c9 with the rest of the PMU, and it is
the register that decides whether Hyp mode is counted at all. Writing
it at c9, c14, 7 is UNDEFINED: it took an undefined-instruction
exception at EL2 on the first PMU write, reported through the vector
because +0x04 carries no syndrome. Encoding corrected against TRM Table
3-15 and recorded where the next reader will look. The counter is also
asked whether it is advancing before anything is timed, because a
measurement from a stopped counter reports zero cycles for everything.
Verified: both repository checks, the host suite, the FVP suite at 6/6
under GCC and ATfE clang, and S32Z280 builds under both toolchains.
Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The reference sheet gains the PMU cycle counter, with the encoding trap that cost a run: PMCCFILTR is under CRn = c14, not c9 with the rest of the PMU, and writing it at the plausible c9, c14, 7 is UNDEFINED. It also decides whether Hyp mode is counted at all -- the TRM defers the bit layout to the architecture, and without bit 27 the counter reads zero forever, which is indistinguishable from a part that has no PMU. The hypervisor-to-guest mailbox is documented as a convention rather than left to be read out of the example: it exists because a guest excursion carries one argument while a probe needs both a target and somewhere to report, and it is free because stage-2 AP cannot deny EL2. The same property that stops AP from isolating partitions is what lets the hypervisor write into a partition's memory for nothing. D4 is settled on mechanism. The cost ratio that the preference rested on is measured -- 13 cycles for a mask switch against 54 for one region descriptor write -- and the mask's cost, unlike a block rewrite's, does not grow with the incoming partition's region count, which is the property a WCET argument cannot do without. It also records why the direct encodings above index 15 stay ungeneralised: they would speed up an operation that happens once. Both sets of figures are labelled as the model's. A functional model does not model timing, so the numbers to quote still have to come from the part; the measurement path is in the image and runs on every target, so that closes with a board session rather than with new code. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Everything before this ran a payload written to be run: a few dozen instructions with no kernel, no stack use worth the name and no vectors of its own. This loads a whole ThreadX, which is the difference between "stage 2 works" and "a hypervisor works". A REAL, UNMODIFIED KERNEL. The sources and the Cortex-R52 port are built exactly as they are standalone. What differs is one build option the port has carried since it was written -- for the case its own comment describes, "a vendor EL2 monitor has already dropped privilege to EL1" -- a linker script describing one partition window, and a board file with no devices in it. On the model that is the whole story: the guest builds from unmodified upstream sources, which is why CI can pin a public commit and boot a kernel on every pull request. WHAT THE GUEST PROVES, and each milestone is one the previous cannot fake: it reaches bsp_main, so the ERET landed; tx_application_define runs, so the kernel initialised inside a confined window; two threads take slices, so the ported context switch works underneath stage 2; a queue carries every message CHECKED BY VALUE AND IN ORDER, because four deliveries of the wrong thing would satisfy a count; and a semaphore grants once and refuses the second get. The hypervisor reads all of it out of the guest's own memory afterwards rather than trusting anything the guest printed. THE READBACK IS SEALED, which was the open question and is now a structure rather than a word. A single progress word cannot tell three failures apart: a window nobody wrote reads as zero and zero is plausible; a guest torn off mid-update leaves words individually valid and jointly nonsense; and a report read from the wrong partition's window looks exactly like a report. So the guest writes every field, then a sequence, then a checksum with the HYPERVISOR'S OWN SENTINEL folded in -- and a report can be attributed rather than merely found. AN HVC CONSOLE, settling the open half of D8. One hypercall per character, and the hypervisor tags each line with the partition it SCHEDULED, so a guest cannot claim to be another one. That last part is free and it is what a safety reviewer asks about. The tagging rules are text, so they are asserted against a capture buffer in the host suite: one tag per line and no more, no dangling tag after a final newline, a partial line closed before the hypervisor speaks, and a guest's forged tag appearing as ordinary text inside a correctly attributed line. THE TWO STAGES ARE DISTINGUISHABLE, and by construction rather than by decode. A stage-2 violation is taken to EL2 and reported there; a stage-1 fault is taken to EL1 and reaches the hypervisor only because the guest's own vector records it and hands control back. Different code, different privilege levels. Both are demonstrated, and the demonstration of the first needed a fact worth writing down: both stages are checked and the stricter wins, so an address outside the guest's own EL1 regions is denied by STAGE 1 first. A guest whose own MPU stops at its window boundary cannot show that stage 2 stops anything. It has to grant itself the granule -- its own MPU then claiming memory the manifest never gave it -- and stage 2 refuses anyway. ONE GUEST IMAGE SERVES EVERY CASE. The hypervisor selects between a stage-2 violation, a stage-1 fault and an access that is genuinely permitted by writing an ADDRESS into the mailbox, not by building a different guest. A binary per case is a set of binaries that can drift apart, and the one demonstrating isolation would stop being the one demonstrating that the kernel runs. The permitted-address build must report FAILED, and its failing is what makes the other two evidence. A GUEST DECLARES THE WINDOW IT WAS BUILT FOR, because a guest linked for the wrong one STARTS. Its entry is a PC-relative branch that survives being copied anywhere; every other absolute address in it is baked in. So the failure is not a guest that will not run -- it is one that boots, schedules, and then faults at an address that looks perfectly reasonable in the report, with nothing anywhere saying the image was built for somewhere else. Three words in the image and one comparison in the loader turn that into a refusal. The magic among them earns its four bytes twice: an .incbin whose file is missing, and a linker pattern that matches nothing, both produce an EMPTY section rather than an error. The loader splits the way the region planner already does: core/ decides where the image goes and holds the state machine, and neither copies a byte nor touches a register, so all of it is reachable from a workstation. It joins the coverage floor at 100% on lines and branches, along with the guest console. The manifest validator gains a rule for an image of zero length, and its size rule is tightened to measure the window the ENTRY is in rather than any executable region -- the weaker form passes a manifest whose copy then overruns into a neighbour. MEASURED ON SILICON, and two corrections were needed before the numbers meant anything. Stage 2 costs a warmed guest nothing resolvable: 27,052 cycles against 27,154 with HCR.VM clear, agreeing to 0.4%. Getting there needed the console suppressed -- one trap per character is 5,051,788 cycles against 27,052, so a loud run can only bound the cost from above -- and a warm-up excursion discarded, because measuring only two passes made stage 2 look 28% FASTER. A hypervisor does not give cycles back; the pair differed in ORDER as well as in HCR.VM, and on a real core the first execution of anything is not the second. D4's carried figure also comes off the part: 235 cycles for the HPRENR mask switch against 472 for one region descriptor write. The decision is unchanged and its margin is not -- the model's ratio was 4.2 and silicon's is 2.0, so a per-region cost extrapolated from the model would have been optimistic by half. What the design actually rests on is untouched: the mask does not grow with the incoming partition's region count. Green on both targets: ten FVP images through CTest, six host suites, and all four one-partition images run on a S32Z280-594EVB with the negative one reporting its expected failure. Both toolchains. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The cooperative guest proved a real ThreadX kernel BOOTS and SCHEDULES inside a stage-2 window. A cooperative kernel is a kernel with the interesting half removed: nothing takes the core from a thread, so nothing can go wrong in the place a partitioning hypervisor most needs nothing to go wrong. This adds the interrupt. WHO OWNS THE GIC, which is the decision the rest follows from. ZoneX owns every byte of memory-mapped GIC state and a partition gets its own CPU interface, which on this part is system registers. The argument is not "shared things belong to EL2", which is true and weak. It is that the redistributor's SGI frame holds the enable bits for all thirty-two SGIs and PPIs of this core -- INCLUDING PPI 26, the hypervisor's own timer, which is what will end a partition's window. A partition able to write that frame could clear that bit and never be descheduled again, and nothing about that is a memory-isolation failure, so no region set would show it. Doing it this way costs the partition nothing: its manifest is unchanged and it is granted no device region of any kind. The alternative -- mapping the redistributor into the partition so it could enable its own PPI -- would have cost two extra EL2 regions on silicon, because PMSAv8-R has no region priority and the window has to be split three ways, AND opened the hole above. Recorded as D24. HCR.IMO STAYS CLEAR, so the timer PPI is a physical interrupt taken straight to EL1: no injection, no List Register, no EL2 work per tick. The cost is written down because it is the next phase's whole problem -- with IMO clear the hypervisor cannot take an interrupt of its own while a partition runs either, so a tick that ENDS a window needs IMO set, and with IMO set every guest interrupt has to be injected. That is a change to the hypervisor and to no guest, which is why this shape is worth having first. ONE GUEST IMAGE, and whether it has a clock is a word in the mailbox rather than a build option. The run that demonstrates isolation and the run that demonstrates preemption are the same bytes, so they cannot drift into two binaries where only one is the one being quoted. The guest is still built from unmodified port sources; the only change is that it now uses the port's own TX_R52_USE_THREADX_IRQ, whose EL1 IRQ vector body it reaches with one branch out of its own vector table -- so the interrupt entry sequence is the port's, unmodified, and VBAR stays the guest's. WHAT IS PROVED, on both targets: a thread that never yields is DISPLACED, two equal-priority threads that never yield are TIME SLICED, the partition receives INTID 27 and no other, and its clock does not advance while it is not running. The last is CNTVOFF, and it is exact: on the S32Z280 the offset was credited with 1,969,637 counts against an interval of 1,969,637. TWO MEASUREMENT MISTAKES ARE IN THE HISTORY BECAUSE BOTH WERE MADE. The gap the freeze is measured across was first taken over a block of console output, on the grounds that a polled UART is millions of cycles. It is -- on silicon. On a model whose console is semihosting it costs no simulated time at all, so the counter advanced by ZERO and the check was green, and so was the build that deliberately breaks the freeze. The gap is now a deliberate dwell, and the image asserts that a real interval happened before it asserts anything about it. Then the check was built on counter reads taken from outside the mechanism, and reported the partition's clock advancing by 64 counts on a run where the freeze was perfect: on the S32Z280 a CNTPCT read crosses into an 8 MHz clock domain, so the handful of reads between the CNTVOFF write and the check cost 11.6 microseconds of real time. It was measuring the cost of measuring. It now compares only instants the mechanism itself took, against the offset read back out of the register, so every term is a hardware read and a CNTVOFF write that had not landed still fails it. TWO NEGATIVE BUILDS, breaking different halves and each failing exactly one check on both targets. One leaves the partition's PPI disabled -- which is the isolation claim showing up as a test result, since the guest cannot enable it itself -- and one does not give the partition back the time it spent descheduled. The second keeps the bookkeeping and drops only the credit, deliberately: skipping the resume outright left the recorded instants stale and its observable check then PASSED, comparing a real interval against the time since boot. The loader is now shared rather than copied. Two images launch the same guest and they differ in what the hypervisor configures and in what they claim, not in how a guest is loaded -- and the mailbox layout, the header check and the seal are a contract with the guest image, which cannot have two implementations. The mailbox grew to two granules for what a preemptive guest has to say, which moves the entry branch to +0x80 and costs nothing at stage 2. FOUR THINGS A REVIEW OF THIS CHANGE FOUND, all of them real. GICR_CTLR.RWP and GICD_CTLR.RWP are now polled. A DSB says a write has left the core and says nothing about whether the GIC has finished acting on it, and bring-up disables all thirty-two of this core's SGIs and PPIs and then enables one of them in the same frame a few instructions later. An in-flight disable retiring after that enable would undo it, leaving a partition arming a timer whose interrupt was disabled -- a guest that never ticks, on some boots. The distributor's group enables are now CLEARED before ARE is set and restored afterwards. Changing ARE while the GIC is enabled is UNPREDICTABLE, so setting ARE first is correct only if the enables were already clear -- a claim about reset state, which this file argues against making everywhere else and then made here anyway. The guest blob's minimum-size ASSERT was still 0x50 after the header moved to 0x8C, so a blob of 0x51 to 0x8F bytes linked cleanly and the magic check read past the end of the section -- the out-of-bounds read the assert exists to prevent. And the build that probes an address it IS granted was aimed at mailbox offset zero, which is ZX_GD_PROGRESS: the probe's sentinel was ORed into the progress word and the seal then certified it. Harmless noise until this change gave two of those bit positions meaning, at which point a cooperative build with no clock reported PREEMPTED and NO_CLOCK both. The probe now has a word of its own that nothing reads. Green on the Armv8-R AEM FVP under both toolchains, and logged ALL CHECKS PASSED on an S32Z280-594EVB, where two identical quiet excursions differed by 90 cycles out of 1,952,856. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The gcc and clang check workflows exist to hold this project to its warning set, and they were not looking at the ZoneX code compiled into a ThreadX image: the guest support and both partition images, several thousand lines. Neither workflow set ZX_THREADX_SOURCE_DIR, so the example CMakeLists skipped the guest images -- correctly, and with a message, which is right for a contributor who has no kernel sources to hand and wrong for the lane whose whole job is strictness. TWO LAYERS HAD TO GIVE WAY, and the second is the one worth reading. The first is a ThreadX checkout in both workflows, pinned to the commit zx_fvp.yml already pins, and the variable passed through to CMake. The second is that fixing only the first would have changed nothing. The guest is an ExternalProject -- a separate CMake invocation with ThreadX's own toolchain file -- and an ExternalProject inherits nothing that is not listed in its CMAKE_ARGS. CMAKE_COMPILE_WARNING_AS_ERROR stops at that boundary, so the guest images would have built in the strict lanes with their warnings merely printed. FORWARDING IT WHOLESALE WOULD HAVE BEEN WORSE THAN NOT FIXING IT. That sub-build compiles ThreadX's kernel as well as ZoneX's guest support, and ZoneX does not get to decide how the kernel is compiled -- which is the argument that makes the guest a separate project in the first place. So the flags are applied PER SOURCE FILE, to the three files that are ZoneX's, and to nothing else. The two files the executable takes from ports/cortex_r52 keep the port's settings, which matters more than it looks: with -Werror a target-wide setting could fail this build on a warning ZoneX neither owns nor can fix here. The list itself comes from cmake/zx_warnings.cmake, which now publishes ZX_WARNING_FLAGS as a variable alongside the interface library it already built. The guest project cannot see the hypervisor's targets, and restating eleven flags over there would have been a second source of truth that agrees until the day it does not. -Wlogical-op is selected by compiler at both ends for the same reason it always was: ATfE clang rejects the GNU spelling outright, which is noise until warnings are errors and a failed build afterwards. ThreadX's own build sets no warning flags at all, so before this those three files were compiled with NONE. The lane found one thing immediately, which is the sort of thing it is for: bsp_main was defined with no prototype -- a MISRA Rule 8.4 finding, and a function whose signature nothing was checking. The four entry points the port calls are now declared in zx_guest_bsp.h rather than forward-declared where they happen to be defined. Not by including the port's board.h, which declares all four: the two boards' copies of that header differ, and the files implementing these are shared between the boards. Verified by running what the workflows run: all three gcc configurations and both clang configurations configure, build and link every image with warnings as errors and the guest images present. The FVP suite is unchanged at 13 of 13. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
…ction D24 was written when the single partition was first given a clock, and its closing argument was wrong in a way that made the next step look far larger than it is. It reasoned that because HCR.IMO is clear, the hypervisor cannot take an interrupt of its own while a partition runs, and concluded that a tick which ENDS a partition's window therefore needs IMO set -- and that with IMO set every guest interrupt would have to be injected through a List Register. ROUTING IS BY EXCEPTION TYPE, NOT BY INTID, which is the fact the argument missed. HCR.FMO sends physical FIQ to EL2 while HCR.IMO, left clear, leaves IRQ with EL1. So the hypervisor's own timer goes in GROUP 0 -- which is what the GIC delivers as FIQ -- and arrives at EL2 while every partition interrupt stays Group 1, stays an IRQ, and is still delivered straight to EL1. No injection, no List Register, and no change to any guest. And it is BETTER than injection rather than merely cheaper. With FMO set, PSTATE.F is ignored at EL0 and EL1, so a partition cannot mask the interrupt that ends its own window. A tick delivered as an IRQ to EL1 could be deferred by any guest that disabled interrupts, which is precisely the property time partitioning must not concede. The guest half is already in place and was already right: a partition is granted no Group 0 interrupt and never enables ICC_IGRPEN0, so nothing can deliver an FIQ to it. Only the prose drew the wrong conclusion from what the code does. What is missing is all at EL2 -- FMO, PPI 26 in Group 0, and a body on the FIQ vector -- and none of it has been run. Injection through the List Registers goes back to where it belongs: a later phase, for making interrupt latency a hypervisor-controlled and WCET-bounded quantity, rather than a prerequisite for a partition tick. Comments only; no code changed and no behaviour with it. The three files that repeated the claim -- zx_gic.c, zx_timer.c and the preemptive example's header -- are corrected with it, because a wrong reason repeated in four places is four things to re-derive. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The workflows pin ThreadX to a commit, and that pin went stale the moment the S32Z280 boot-at-EL1 bracket was upstreamed. The pin still named the dev tip from BEFORE that merge, so every guest image CI built for the S32Z280 was built against a port that had never heard of TX_R52_BOOT_AT_EL1. A DEFINITION NAMING AN OPTION THE SOURCE DOES NOT TEST IS NOT AN ERROR. It is inert. So the build did not fail -- it produced a guest containing the port's entire EL2 reset path, ERET included, which drops to EL1 from EL1 and dies on its first instructions. Confirmed by building one: the guest from the stale pin carries an `eret` and the correct guest carries none, and both link without a single warning. That is the shape of failure this suite exists to refuse. Nothing executes a guest on a hosted runner, so the only symptom was an instruction in a binary nobody ran, and the lane reported success. The warnings-as-errors lane added for the guest support made it worse rather than better: it started building the S32Z280 guest for the first time, against that pin, and called it green. TWO FIXES, BECAUSE THE PIN WILL GO STALE AGAIN. The pin is bumped to the dev commit that carries the bracket, in all three workflows. That is the immediate fix and it has the lifespan of the next upstream option a guest depends on. The lasting one is a guard in the guest's own build: it reads the port's entry.S and REFUSES if TX_R52_BOOT_AT_EL1 does not appear in it, naming what would otherwise happen. Grepping the source is crude, and it is the only check available -- the guest is a separate CMake project, it cannot ask the port which options it supports, and there is no version to compare. Crude and loud beats invisible. Verified both directions: against a checkout without the bracket the build now FAILS with that message, and against one with it the FVP suite is 13 of 13 and both boards build under both toolchains. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Carried out of the single-partition work as findings, all outside its scope and all inside this one. THE VALIDATOR AND THE LOADER DISAGREED ABOUT ONE BYTE. zx_manifest_verify compared an image's length against (limit - base) while the limit is INCLUSIVE, so an image that exactly filled its window was refused at boot with a message saying it was too large for a window it fits. zx_partition_prepare has always had the rule right. The two now read identically, and the host suite pins the boundary from both sides -- a one-sided test cannot tell a rule that is off by one from a rule that is right. The loader's own boundary test already existed, which is exactly why nothing caught the disagreement. THE REGION PLANNER BUDGETED AGAINST THE WRONG REGISTER. It checked HMPUIR, which says how many region DESCRIPTORS a part has, and ignored the measured width of HPRENR, which says how many of them a one-write partition switch can turn OFF. The Cortex-R52 TRM disagrees with itself about that width and both ZoneX targets came out twenty bits wide, so it does not bite today; on a part where the two differ, a partition seated past the mask would have its descriptor programmed with its own enable bit set and left there, and the outgoing partition's window would stay live underneath the incoming one. No fault, no diagnostic, and an isolation claim that is simply untrue. zx_mm_plan now takes both budgets and refuses with a code of its own. A NEGATIVE BUILD ANNOUNCED THE VERDICT IT WAS SUPPOSED TO EARN. The probe's negative banner contained the literal fail mark, and the fail mark is what proves a negative run REPORTED its failure rather than crashing -- so every negative run satisfied that condition in its first few lines and a hang afterwards would have been judged a correct result. The banner is reworded and the runner now matches a verdict at the START OF A LINE, which closes it at the reader rather than at the writer. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
core/src/zx_schedule.c was the last empty file in the repository. It now holds the window table, the round-robin advance and the arithmetic that says where each boundary falls on the physical counter. EVERY BOUNDARY IS AN ABSOLUTE COUNT FROM ONE EPOCH, never a countdown re-armed at each tick. Re-arming a relative interval inside the handler adds the handler's own latency to every window, so a frame declared as 10 ms becomes 10 ms plus the switch -- cumulatively, for the life of the run. The schedule still looks fixed and the windows stay in the right proportion; the frame simply stops being the length it was declared to be. It is the most common way a deterministic frame stops being one and it is invisible in any run short enough to read. WHICH IS WHY THIS FILE JOINS THE 100% LINE-AND-BRANCH FLOOR, and the decision was made rather than defaulted either way. Catching drift needs ten thousand frames, which is a millisecond on a workstation and two minutes on the S32Z280 -- and the central host case asserts the ten-thousandth boundary is EXACTLY the epoch plus the tick count times the tick length. The arithmetic is also 64-bit against a counter that has been running since reset, so an epoch just below 0xFFFFFFFF is a fixture here and nine minutes of waiting on a bench. The rest is deliberately absent. One window per partition, in manifest order, lengths fixed at build time; no priorities, no admission control, no yielding into a neighbour's window. An idle partition BURNS its window, which is not a limitation to be fixed later but what a static frame means: handing the remainder to the next partition would make one partition's start time depend on another's behaviour, and the independence of those two things is the entire purchase. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The partition switch, and the routing that makes one possible. HCR.FMO SET, IMO AND AMO CLEAR. The hypervisor's own timer goes in GIC Group 0, which the GIC delivers as an FIQ, so it arrives at EL2 -- while every partition interrupt stays Group 1, stays an IRQ, and is still delivered straight to EL1 with no injection and no List Register. Routing is by exception TYPE and not by INTID, which is what makes this two register writes rather than an interrupt-virtualization layer. It is better than injection rather than merely cheaper: with FMO set, PSTATE.F is IGNORED at EL0 and EL1, so a partition cannot mask the interrupt that ends its own window. FMO IS BIT 3 AND AMO IS BIT 5, AND THIS PORT HAD THEM THE OTHER WAY ROUND from its first commit -- the mnemonic order a reader reaches for is the alphabetical one. It survived because IMO is bit 4 either way and because every use of the three until now was a single BIC of all three at once. The first image that SET one of them routed nothing: bit 5 is AMO, so physical FIQ never reached EL2 and no window ever ended, while the comparator expired, the GIC made the interrupt pending and every set-up check printed green. A check written as (HCR & ZX_HCR_FMO) could not have caught it; the positions are now asserted and the image checks the BIT. AND SETTING FMO MOVES THE GUEST'S ICC_PMR TO THE VIRTUAL INTERFACE. TRM 9.3.5: an EL1 access to any register common to both interrupt groups is redirected once FMO or IMO is set, and ICC_PMR is one of them. Every guest writes ICC_PMR = 0xFF at start-up; from that moment the write lands in ICV_PMR while the physical mask -- which resets to zero, masking everything -- is left closed. A partition that was receiving its timer end to end stops receiving anything, with no fault and no message. The hypervisor now owns the physical mask. The same redirection closes D24's last gap: a partition cannot reach the physical Group 0 enable either. THE SWITCH IS FIFTEEN WORDS OF ASSEMBLY AND THE REST IS C. Hyp mode banks only SP, LR and SPSR, so r0-r12, ELR_hyp and SPSR_hyp are all that cannot wait; a guest's banked registers, its EL1 system registers and its whole EL1 MPU are still in the machine and are reached from C. That keeps the twenty- region loop -- which measures at 85% of the switch on both targets -- eight readable lines instead of a hundred and twenty coprocessor moves. The FPU is DENIED to a time-partitioned system rather than saved, because nothing saves the register bank and two guests would share it; the failure mode is a wrong ANSWER and not a fault. The traps bracket the frame exactly, because with them set the S32Z280's debug probe cannot read the core's registers at all. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The image this repository has been building to. Two ThreadX kernels, each in
its own stage-2 window, time-sharing one logical core under a major frame
taken from the manifest: partition A holds seven ticks of every ten and
partition B three, for twenty frames.
MEASURED ON THE S32Z280-594EVB, twenty frames and thirty-nine boundaries,
with no missed deadline and no interrupt the hypervisor's own timer had not
raised:
partition A 11,157,245 counts on the core, 139 of its own ticks
partition B 4,822,000 counts on the core, 51 of its own ticks
A x 3 = 33,471,735 against B x 7 = 33,754,000, within 0.84% of exact. That
equality IS the temporal claim rather than a symptom of it: a partition able
to see wall clock would be out by a factor of three, not by a percentage.
The 20,755 counts unaccounted for against the frame's 16,000,000 are the
thirty-nine switches, charged to neither partition.
The switch costs 5,630 / 5,684 / 5,944 cycles min / mean / max, and the
guest's own EL1 MPU is 85% of each direction on BOTH targets -- across a
32-region model and a 20-region part. A partition switch is not expensive
because the hypervisor does much; its per-partition state is three register
writes. It is expensive because a guest has a lot of registers.
FOUR BUILDS, AND WHICH ONES MUST PASS IS THE POINT.
the frame both partitions run to the limit, clocks in ratio
hog B masks IRQ and FIQ at EL1 and spins for ever. It is
preempted anyway, and the masking costs it exactly its
OWN kernel's tick: its tick count froze at 4 while its
liveness counter reached 229,233. A frame driven by an
interrupt taken at EL1 would HANG on this build.
cross B grants itself a granule inside A's window in its own
EL1 MPU and writes to it. Stage 2 refuses, B is
stopped, and A runs to the end of the frame with its
schedule untouched -- which is the half of isolation a
single partition can never demonstrate.
no_tick, overlap must FAIL, and now REPORT their failure rather than
hanging: a hypervisor that cannot deliver its own tick
refuses to start a frame at all, for the same reason a
guest is never allowed to arm a timer against a stopped
counter.
A SECOND PARTITION WAS MEANT TO BE A DATA CHANGE AND IT WAS NOT. It was
going to be a second copy of a two-hundred-line build file and a second copy
of a linker script, differing in one address each. The guest project is now
configured once per partition from a template instead, which is the
generality that was missing rather than a special case for partition B.
Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
D25: how a partition's window ends. D24's Design A, built, run on both targets, and carrying what it cost that the design did not predict -- the ICC_PMR redirection, the deliberate omission of HCR.AMO, and the FPU denied rather than saved. The reference sheet gains what no session should have to re-derive: HCR's routing bits are FMO[3], IMO[4], AMO[5] -- not the alphabetical order a reader reaches for, and this port had two of them swapped. The three questions that localised it are written down with it, because a window that never ends looks identical whether the comparator did not expire, the GIC was never told, or the core never took the exception. CNTHP: TVAL, CTL and the 64-bit CVAL a frame is actually built on, with why the absolute form is right here and the relative form is right one level down inside a guest's own handler. Which CPU-interface registers an EL1 access is redirected for once FMO is set, from TRM 9.3.5, and why ICC_PMR being in the "common to both groups" row is the one that bites. That the floating-point traps block the S32Z280 debug probe's register read, measured by comparing an image that stops before them with one that stops after. The state-a-switch-must-save table is now what a switch DOES rather than what it will have to, with the measured cost of each group on both targets beside it -- and one figure that disagrees with D4's by half on both targets, which is recorded as unexplained rather than quietly replacing the published one. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Two went in while the partition switch was being written, and both were in CODE COMMENTS rather than in documents -- which is where nobody thinks to look for them. The existing check rejects a local path and a numbered step and had nothing to say about either. The planning documents such identifiers name live outside every repository, so a comment citing one points a reader at something they cannot obtain and never will. The FACT is almost always worth keeping and is almost always citable another way: those measurements were taken during a named piece of work on a named board, so "measured on the S32Z280 during the Cortex-R52 Modules port work" carries everything the identifier did and survives the reader. Checked case-sensitively and separately from the rest, because folding it into the case-insensitive pattern would make an ordinary lower-case word an error. Seen to fail before it was believed. The pattern spells the shapes it rejects, because a denylist has to. That is the same bargain scripts/check_terminology.sh makes and states: one place holds the spellings, so the list cannot drift away from what is enforced. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Every switch cost this suite publishes is in core CYCLES, which is the right unit for a worst-case-execution-time argument and is not a self-contained one. Nobody could convert them: CNTFRQ reads zero out of reset and this part reports its core clock nowhere, so "5,715 cycles" was a number no reader could turn into a duration -- or argue with, which is not the same as one they should accept. MEASURED AGAINST THE SYSTEM COUNTER, whose frequency is the one in this system that has actually been established -- three independent ways, during the Cortex-R52 port work. 48,050,135 Hz on the S32Z280-594EVB, over one millisecond of counter time. AND THE ANSWER EXPLAINS ITSELF. The S32Z27 reference manual gives FIRC as 48 MHz and says FIRC_CLK is the default clock for the entire system at power-up. ZoneX configures no clock tree, so the core spends every run on the part's backup oscillator. THAT QUALIFIES EVERY CYCLE FIGURE, AND IN THE OPPOSITE DIRECTION FROM THE OTHER CONDITIONS. The EL2 caches are off and the image is built -Og, so a warm, optimised switch can only be faster: both make the figure an over-estimate. A backup-clocked core makes it an UNDER-estimate -- at 48 MHz the memory a switch touches is cheap in core cycles, and raising the core clock without raising the memory's makes the same code cost more cycles, not fewer. So a switch figure from this bench is an over-estimate for two reasons and an under-estimate for a third, on one board, and it is NOT a worst case in either direction until it is taken again with the clock tree configured. Listing only the conservative conditions and letting a reader conclude it was an upper bound would have been the easy thing to do and the wrong one. The image now prints all four conditions, the measured clock, and a nanosecond conversion ABOVE its own numbers, together with the two things deliberately excluded from them -- so a figure quoted out of a log carries its conditions with it instead of leaving them in a document. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Its status section said there was no ThreadX guest, no partition manifest and no scheduler. All three exist, and two partitions now time-share a core under a static frame on both targets, so the front page had drifted three pieces of work behind the tree. WHAT THE REWRITE IS CAREFUL ABOUT, because a front page is where a number gets quoted from and the conditions do not travel with it: IT LEADS WITH MATURITY. "This is not production software and is not close to it." The heading keeps "under construction" and gains "demonstrator". The section below it already said an overclaimed demonstrator is worth less than an honest one; the top of the file now says the same thing first. IT SEPARATES MECHANISMS FROM MEASUREMENTS, and does not hedge both the same way. A partition cannot reach its neighbour's memory, a window ends whether the partition agrees or not, and each clock advances only in its own windows -- none of those move when a number does, and burying them under the caveats the numbers need would underclaim the results that are settled. An underclaimed demonstrator is worth less than an honest one too. IT MARKS WHICH NUMBER IS ROBUST. The seven-to-three ratio is a ratio of two readings of the system counter, whose frequency was established three independent ways, so it cancels the core clock, the caches and the optimisation level outright. The switch cost does not, and says so. IT COMMITS RATHER THAN CAVEATS. Configuring the clock tree is named as a later phase and the switch figure is stated to be expected to change when it lands -- with why it will move in each direction, and why it is worth publishing now anyway: the next measurement needs something to be compared against. IT NAMES THE EXCLUSIONS. The guest console and boundaries that had to wait out a stopped partition's window are both left out of the per-switch figures, both for stated reasons. An exclusion a reader discovers reads as concealment whatever its justification. The third architectural finding replaces the region-budget one, because the ICC_PMR redirection is the more useful warning to somebody about to set HCR.FMO for themselves. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The regression this phase exists to produce, on the model and on silicon. Fourteen isolation cases in one run, seven in each direction: the neighbour's data read and written, its code branched into, the ungranted granule immediately next door, the hypervisor's own manifest, the GIC distributor, and each partition's own window marked granule by granule and read back. Every case aims at an address of its own, so the fault it provoked is attributable to it; every row is judged from two independent sources, because a partition resumed past a faulting instruction cannot report having been denied and a case that was never attempted leaves the hypervisor nothing to look at. And the critical partition's window period, measured continuously while the untrusted one is steered through five behaviours in phases of one run. On silicon its period is 800,000 counts and it moves by nine while its neighbour idles, fifteen while it computes with its own interrupts masked, and sixty-nine while it violates its boundary a hundred and seventeen thousand times. Nothing a partition does through the schedule reaches its neighbour. What does reach it is the hypervisor's own console: a guest's output is one hypercall per character through a polled UART, and a window ending with a partial line has that line closed by the boundary handler, which delays the next partition's entry by 24,000 counts. That is measured, bounded by one line of output, and left to be fixed by buffering the console off the boundary path. A stage-2 violation still STOPS the partition. A build may ask at build time to be resumed past the access instead, so that one image can sweep the matrix rather than needing fourteen images and fourteen debug sessions; the mode is the image's to enable, its default is the value of zeroed memory, the trap vector takes the same route in every build, and halt is tested rather than assumed by a build of the same image without it. Four negative builds, each of which must fail and does, with its text archived: a region limit one granule too generous, the per-partition time freeze removed, a shared read-only granule its reader may write, and the manifest overlap rule. Three of them were WRONG first and passed, and each time it was the runner's --expect fail that noticed rather than anything in the image. The whole of core/ is now on the 100% line-and-branch coverage floor. The README's switch figure is requalified with it. Re-measuring the PREVIOUS commit's own code on the same bench reads three per cent higher than the number it was published with, and this commit's tree a further two -- none of which is attributable to any instruction added to the switch. With the caches off the cost depends on where the code sits in memory, and the oscillator the core runs on drifts. Four significant figures was over-precise; it is about six thousand cycles, plus or minus four per cent on one bench. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
THE STRICT BUILD DID NOT BUILD, and had not since the major frame landed. -Wconversion on three ULONG-to-uint32_t console calls in the schedule report, and four (void) casts that do not silence warn_unused_result -- GCC deliberately ignores a cast there. CI enforces that preset on every push, so this was one pull request away from being found in public. Then the MISRA-aligned warning set, by the method the Cortex-R52 Modules port work established: re-compile every translation unit in every configuration with the candidate flags and adopt the ones that come back clean. Twenty flags adopted over 293 distinct (source, -D set) compilations across the host, the model and the board. Two candidates were run and REJECTED on evidence, and both are recorded with what they found: -Wwrite-strings collides with ThreadX's pre-const _txe_*_create signatures, and -Wunused-macros would force a fake use on every register bit a driver deliberately leaves clear. -Wredundant-decls paid for the exercise: zx_board_init was declared in two headers, which is Rule 8.5. AN EXCEPTION CLASS ZONEX DOES NOT HANDLE IS NOW PROVOKED. HCR.TID1 and an EL1 read of MPUIR give EC 0x03 on both targets: classified, named, vector and syndrome agreeing, and the run carries on -- which is the property that distinguishes an unhandled class from a hang. Until now the trap vector's ZX_RUN_TRAPPED arm and the classifier's last branch were dead code. Two routes were tried first and are recorded: WFI under HCR.TWI hangs if the trap is absent, and a floating-point instruction under HCPTR is UNDEFINED AT EL1 on the model, which has no FPU. AND THE VECTORS THAT CANNOT RESUME NO LONGER RUN ON A SUSPECT STACK. They reset SP_hyp before calling C -- the stack the fault arrived on may be the reason for it -- and the C side counts its depth so that a fault inside the fault report parks with its own exit code instead of recursing for ever. Neither guard has been provoked; that is recorded rather than left to look finished. THE CONSOLE. A window ending mid-sentence had that line closed by the BOUNDARY HANDLER: CR and LF into a polled UART, at EL2, with FIQ masked, on the switch path, with a trip count decided by what the outgoing guest had been printing. It moved the critical partition's window period by 24,420 counts of the board's 8 MHz counter, against 69 counts for that same neighbour violating its boundary a hundred thousand times. The newline is now deferred to whoever speaks next, inside a window that party owns. The character stream is identical -- only the moment of the write moves -- which is what makes it safe, and the host suite asserts the text rather than a flag. Sixty frames now measure 999, 1,159 and 1,196 counts. A rare excursion of about 15,300 counts remains on the HYPERCALL path, in roughly two six-hundred-frame runs in five; it is measured, bounded, and NOT explained, and the console phase keeps its own bound because of it. AND THE HPRENR FIGURE THAT TWO IMAGES DISAGREED ABOUT WAS ARITHMETIC. The switch measurement divided a loop's span by the round count and THEN subtracted a whole counter read, charging one read to every iteration where one is paid per loop. Same bench, same session, after the fix: 217 cycles from the probe against 219 from the frame, where it had been 235 against 117. Every per-component switch figure published before this was understated by about one counter read. Codegen identity, checked ELF by ELF before the fault-path work: all 49 hypervisor images byte-identical, with only the two guest images moving, by 16 bytes in one function, from one deliberate fix. Full silicon matrix run: five images pass, six negatives fail, each on the check it was built to fail and no other. FVP 24/24. Host coverage holds at 100% of lines and branches. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
…WCET Four new documents and two amended ones. They exist because the certification back end asks for evidence rather than for assertions, and because most of what this pass produced is a REASON rather than a diff. docs/hypercall-abi.md freezes the SHAPE the later phases inherit: a sixteen-bit id space divided by what a call does to control flow, half of it reserved to an integrator so nobody has to fork the list, a discovery call that reports feature bits rather than a version to branch on, and the rule that Phase 0 implements console output and the empty vector and NOTHING else. Sections 3 and 6 specify behaviour that is not built -- discovery and a defined error for an unimplemented id -- and say so in both places: the two arrive together with the first fourth hypercall or neither is worth having. docs/errata.md is the sweep, and a sweep with no findings is only worth something if what was searched is written down. The part is r1p3, from its own MIDR. Seven Cortex-R52 errata are open there, four of them debug and trace only; the other three do not apply and the reasoning is given so a reader can check it rather than take it. Two leave a standing constraint -- HSCTLR.FI must stay clear, and an ISB before any SETEND -- and the first is the kind of bit a hypervisor arguing about interrupt latency would be tempted by. No S32Z2 erratum mentions EL2, stage 2, HPRENR or HCR at all; one bears on device isolation in a later phase and is recorded there rather than here. docs/coverage.md is the other half of the decision not to hold the suite's usual threshold repository-wide: which seven files are held to 100% of lines AND branches, what covers the port instead -- a build that must fail, or one that must pass with a named check -- and the three conditional-compilation axes whose every arm is assembled and executed somewhere in the matrix. Structural coverage of target code is named as a later, funded concern and no number here stands in for it. docs/wcet-inputs.md is the data-dependence list, read path by path. The dominant cost is CONSTANT: the EL1 MPU walk, whose trip count is a part constant read once at boot. What is data-dependent is named with what is known about each -- the console on the hypercall path, the board driver's guard spin bounded by an iteration count rather than by time, and burning a stopped partition's window, which is bounded and deliberate. decisions.md gains the counter-read arithmetic correction to D4 with the corrected component table, the finding that D23's FPU argument cannot be demonstrated on a model with no FPU, and an amendment to D28 saying what the console phase was really measuring. D29 records the lazy line close; D30 records the stack and depth guards on the vectors that cannot resume, including that neither has been provoked. armv8r-el2-reference.md gains a table of which exception classes have actually been TAKEN and how, and the measured fact that the model implements no FPU. One claim in it -- the CPACR-before-HCPTR check order -- is marked as read from the architecture manual and NOT verified, because the attempt to verify it is what found the model has no FPU, and this sheet's convention is that anything unmarked was measured. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
D30 recorded two guards on the unresumable EL2 vectors -- SP_hyp reset before calling C, and a depth count so that a fault inside the fault report parks instead of recursing -- and recorded that NEITHER HAD BEEN PROVOKED. A branch nothing has ever taken is not evidence that it works, which is the standard that put the tick-refusal build in the suite, so the admission was a gap rather than a completed item. zx_probe_refault.elf closes it. It makes the region covering the board's OWN CONSOLE read-only at EL2 and prints one character: the store takes a data abort from Hyp mode, the vector resets the stack and calls the report at depth one, the report's first console write faults for the same reason, and the depth guard stops the second entry without printing. On the S32Z280 it parks with zx_run_failures = 0x5C and the harness stops cleanly on zx_console_run_parked rather than timing out. Both guards are now paths something has taken. Without the depth guard the sequence has no end and does not even overflow the stack -- each fault resets it -- so it spins silently for ever, which is the failure the entry exists to prevent. THE RUN HAS NO CONSOLE AFTER ITS BANNER, by construction, so it is the first build judged entirely from memory. The model builds it and reports it UNPROVOKABLE rather than passing: semihosting is not reached through a region, so no access permission can refuse a write to it. It is not in CTest, for the reason the EL2-fault build is not. AND IT FOUND A DEFECT IN THE HARNESS RATHER THAN IN THE GUARDS. The gdb script read zx_run_failures as a count of failing checks, so it reported 0x5C as "92 failing check(s) -- the console log is where they are named": wrong about the number, and wrong about there being a log, for the one build that denies itself a console on purpose. The three fault-path exit codes are named there now. It had been misreporting 0x5A the same way for as long as the EL2-fault build has existed. MIDR_EL1 IS AN AArch64 SPELLING and had reached the errata document. The terminology check exists for exactly that and did not catch it, because it selects files with git ls-files and the document was still untracked when the check was run. Corrected to MIDR, and worth knowing about the checkers: they say nothing about a file until it is added. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The console phase of the determinism regression carried an unexplained excursion of about 15,300 counts that appeared in roughly two runs in five, with the board driver's write-one-to-clear guard as the leading suspect. The image now measures the whole path on the run it reports: the longest guest console hypercall in core cycles, how many bytes that one hypercall put on the wire, both of the driver's spins in iterations, and -- directly -- how late each window boundary arrived against the absolute deadline the ending window was armed with. The suspect was wrong. The guard has never spun: nought iterations, every phase, every run. The cost is the LINE TAG. Nearly every console hypercall writes the one byte the guest asked for; the one that opens a line writes twenty-two -- the owed newline, the tag naming the partition, and the guest's character -- at EL2 with FIQ masked, so the boundary interrupt is held off for all of it. 106,214 to 106,352 core cycles over seven runs: 2.2 ms, about 17,640 counts of this board's 8 MHz counter. Nor was the residual rare. A deferral that is constant costs a period nothing, because a period is a difference and a constant cancels in it; what reaches the number is the change. Whether a boundary falls inside a line tag is decided by a phase relationship between a fixed schedule and a guest printing a fixed message, and two cycle-counter reads per character -- under one per cent of a character time -- were enough to move it. Instrumented, the excursion is on every run: 17,830 · 17,889 · 17,943 · 17,963 · 18,101 · 18,141 · 18,327. That also closes the widened build, carried as unexplained for a step. Instrumented it measures 12,557 · 13,132 · 13,714, and the correct sixty-frame build now measures 15,909 and 17,327 -- larger. The two builds were never doing different things. Both spins in the board driver are now bounded by TIME as well as by iterations, sharing one deadline of ten character times computed from the counter frequency and the baud rate. The wait for the byte to go out had no bound at all before this, which is the larger hole of the two. Both bounds are kept for the reason zx_el2_dwell keeps both: the time bound is what a WCET argument reads, and the iteration bound is what survives a counter that is not running. The console phase's bound stays at half a window and is now derived rather than observed: the worst deferral is one line tag, a period sees it as one long entry and one short correction, so the worst jitter the mechanism can produce is 35,280 counts against a bound of 40,000. Host suite 100% lines and branches, full FVP suite green, and the silicon matrix run on the S32Z280-594EVB with every negative build failing on the check it was built to fail and on no other. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Two kinds of statement, both of which asked a reader to trust something they have no way to reach. Eleven pointed at planning documents that are not in this repository. A contributor who has only this repository learns nothing from "stays where the roadmap put it", "the plan this work came from expected the opposite", or "the spelling the focused task list uses" -- and a citation of a document nobody else can open dates badly besides. Each one kept its fact and dropped its citation, because the fact was always the content: the interrupt work is a later phase, the split into assembly and C is better than one large routine, and tx_hv_* was rejected for reading as a ThreadX subsystem. None of those needed a source outside the tree to stand up. One asserted a third party's design rationale with no source at all. The EL2 reference sheet said that Phase 0 had been expected to paravirtualise interrupts because NXP's EL2M does, and that EL2M's reason is the shared GIC Distributor rather than absent injection hardware. Every other claim in that sheet is either measured here or cited to the technical reference manual, and this one was neither. It has been replaced by what was actually established: the part implements four List Registers, so injection is available, and Phase 0 keeps interrupt handling simple as a scope decision rather than a limitation inherited by assumption. The conclusion is unchanged; what goes is an unverifiable claim about somebody else's product. The reference check passed on all twelve, and that is worth recording rather than fixing blind. It matches path shapes and document identifiers, not prose, so "the roadmap" walks straight through it. It has deliberately not been extended: "the plan" is ZoneX's own name for the region layout that zx_mm_plan produces, with eleven legitimate uses in the core and the examples, so a pattern broad enough to catch the prose form would fire on every one of them. A check that cries wolf gets bypassed and then catches nothing, which is the reasoning already written into that script. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
It carried four checks and only three of them are the project's business. The three that stay are ordinary hygiene, and CONTRIBUTING.md already describes exactly these: a local absolute path, which resolves nowhere for anybody else and in a build script means the script runs on one machine; a citation of a numbered stage of something not in the tree, which a reader cannot follow; and a tracked agent-instruction file, which no Eclipse ThreadX repository carries. The fourth enforced an authoring convention belonging to one working setup. It rejected the identifiers of documents that live outside any repository -- and to reject them a denylist has to spell them, which made this file the single place those names appeared. Their spelling is of no use to anybody reading this repository, and enforcement of how one contributor cites their own notes does not belong in a project's continuous integration. It was also not the check that works, and that is the part worth recording. The shape that actually occurs is prose -- a sentence deferring to an external document by description rather than by name -- and the removed pattern matched none of it. Twelve such sentences were found by hand while preparing to publish, in the documentation and in code comments both, every one of them after that pattern had passed. What replaced it is a hook on the authoring side, where the risk is, and where a commit message can be read as well: the committed checks never see one. Each remaining check was provoked and seen to fail before this went in, and the removed one was confirmed silent, because a check nobody has watched fail is not evidence that it can. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Five changes, and two of them correct something wrong rather than stale. THE CONSOLE PARAGRAPH DESCRIBED A MECHANISM THAT IS NO LONGER THERE. It said a window ending on a partial line has that line closed by the boundary handler, at a cost of 24,000 counts. The boundary handler now writes nothing, and the residual is on the hypercall path: one line tag, twenty-two bytes, 17,640 counts, with the boundary interrupt masked throughout. It also said the fix is to buffer the console, and buffering was the rejected option -- what removes it is an interrupt-driven driver with a polled fallback the fault path can force, because the fault reporter prints when ZoneX has already failed once. The claim is now split by cause: nothing a partition does through the schedule reaches its neighbour, and what does reach it is the hypervisor's own driver. That is a defect here rather than a limit of the partitioning, and the bound is derived from the mechanism -- 35,280 counts against a half window of 40,000. AND THE EL1 MPU WAS GIVEN THE WRONG DENOMINATOR. "A partition switch costs about 6,000 cycles and the EL1 MPU is 85% of it" reads as 85% of the switch. It is 3,407 cycles: 85% of the save and restore, and 60% of the switch. docs/wcet-inputs.md had this right, so the README was the only place the two were conflated. Both denominators are now stated. The claim that the split holds "on a 32-region model" is gone with it: that is a timing proportion, and timing on a functional model describes nothing. The regression figures move to the six-hundred-frame run -- 21, 21, 22 and 304 counts -- because they are the larger and therefore the honest ones; the sixty-frame numbers they replace read better and prove less. The switch figure is quoted as a band across five readings rather than one run's triple, since the paragraph's own point is that it moves. A region-budget section is new, and it is the portability statement a reader needs before choosing a board rather than after: the permitted EL2 region counts, what the hypervisor's own device memory costs out of them and why that is a property of the board, and the switch mask as a second budget that a region can fall outside of with nothing left to fault on. A part configured with no EL2 MPU cannot run ZoneX at all, and there is no software fallback. Every number in it is measured on both targets, the model included. The claim section is retitled from what Phase 0 WILL prove to what it does, gains the positive claim it never carried, and loses one overclaim: a later phase was described as delivering a CERTIFIED worst-case interrupt latency. Nothing here is certified and that phase bounds rather than certifies. That interrupt latency is not measured at all now leads its own paragraph instead of sitting inside a list, because it is the first thing a safety reader has to know, and the conditions every figure was taken under sit beside the claim so that a quotation carries them. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
zx_api.h declared a major, a minor and a patch and stopped there, where every other component of the suite declares five. Phase 0 is 0.1.0.202603 with no hotfix, so ZX_BUILD_VERSION is 202603 and ZX_HOTFIX_VERSION is a space. THE BUILD NUMBER IS YYYYQQ -- the year and then the QUARTER of publication, not the month -- and that is written into the header rather than left to be looked up, because the value reads as a month. 202603 is the third quarter of 2026. The neighbouring components carry the same shape and 202602 was Q2. CONTRIBUTING.md already documents the scheme under "Version numbers"; what was missing was the constants and a check. So the host suite range-checks the quarter rather than pinning the whole value. A version carrying a month satisfies every other property a version has: it is an integer, it sorts, it is six digits, it looks like a date. It is simply wrong by two quarters, and nothing would have said so. Pinning 202603 outright would have caught it too and would need editing every release, which means being edited without being read. The lower bound is Q3 2025, when the quarterly model was adopted. The hotfix character is checked for being a space or a letter, because a digit there would mean somebody had treated it as a number. Both checks were provoked and seen to fail before this went in -- 202609 rejected, '1' rejected -- since a check nobody has watched fail is not evidence that it can. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
A manifest could not name a memory type without a Cortex-R52 header. ZX_ATTR_NORMAL_WB, ZX_ATTR_DEVICE and ZX_ATTR_NORMAL_NC were defined in platform/cortex_r52/inc/zx_port.h, while the other three fields of the same region descriptor -- AP, XN and SH -- were in core/inc/zx_manifest.h. That split was an oversight against a rule this tree already states. The include of zx_manifest.h in the port header carries the reason next to it: the port programs what a manifest declares, so the descriptor belongs to the manifest and not to the port, because the host-side validator has to build and check the same objects with no Cortex-R52 header in reach. The consequence was in the test suite the whole time. test/host cannot include a port header, so test_zx_partition.c set an attribute index of bare 0 where it meant Normal write-back -- the one field of four that had to be a magic number. It names the type now. WHAT SPLITS, AND WHERE THE LINE IS. The INDEX each memory type occupies is a manifest's vocabulary and is now a contract in zx_manifest.h: a port may choose the attribute byte that expresses "Normal, write-back" on its own hardware, but not the index it sits at, because a manifest names the index. The BYTES and the register values stay in the port, which is the only thing here that is Cortex-R52-specific. AND THE CONTRACT IS ASSERTED RATHER THAN DESCRIBED. zx_stage2_mpu.c now extracts, from the HMAIR0 value it actually programs, the byte sitting at each contracted index, and fails the build if it is not the byte that index promises. Extraction rather than restatement: a restatement would be a second copy of the same number and the two would drift together. A byte moved to the wrong index would otherwise give every region naming that type the wrong memory attribute, silently, with the validator satisfied and the hardware not objecting -- which is the same failure mode the unwritten-index rule already exists to prevent, one level up. A range check runs first and masks the index inside the shift, so that an index moved into HMAIR1 reports itself rather than reporting an undefined shift by 32. Both were provoked: swapping two bytes in HMAIR0 fails the build naming the type, and moving a type to index 4 fails it naming the register, with no pedantic warning in either case. No runtime behaviour changes. The values are the same values at the same indices; what changed is which header owns them and that the agreement is now checked. Verified by the case that exposed it: a static const manifest compiles and passes zx_manifest_verify against common/inc and core/inc alone, with no port header and no local workaround. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
ZX_MPU_GRANULE was the last piece of a manifest's vocabulary living outside the manifest header. It is a rule about what a manifest may DECLARE -- every base and every limit one carries is checked against it, and someone writing one needs it to hand -- so it now sits with the AP, XN, SH and attribute-index encodings rather than in the general API two headers away. Nothing was broken before this and nothing is fixed by it; both headers are architecture-independent, so this is cohesion rather than layering. It follows the memory-type move for the same reason: a reader looking for what a region descriptor may contain should find all of it in one place. THE TESTS FOLLOWED THE CONSTANT, and that mattered more than the move. test/host/test_zx_api.c includes zx_api.h and no other ZoneX header, which is what makes it evidence that the header stands alone -- so it could not simply gain an include. Its granule assertions moved to the manifest suite, beside the alignment rules they underwrite, and the named memory types are asserted there too. What stays behind is the alignment arithmetic itself, now written against an explicit alignment argument: it was always exercising zx_addr_t and the ZX_NODISCARD declaration rather than the constant, and saying so makes the division obvious. Verified from both ends: zx_api.h compiles as the only ZoneX header included, and a static const manifest still compiles and passes zx_manifest_verify against common/inc and core/inc with no port header. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
The figures came from a run taken before the three commits that moved the memory-type vocabulary and the region granule between headers. Those changes are behaviour-neutral and the assertions binding them are compile-time, but a README quoting silicon should quote the silicon the code ships as. Re-run on the same board: the critical partition's period moves by 22, 20, 24 and 185 counts across the quiet and fault phases, and 17,951 while its neighbour storms the console, whose longest hypercall is 106,116 cycles and still exactly 22 bytes. The switch reads 5,662 / 5,703 / 5,982. THE EARLIER RUN IS CITED BESIDE IT RATHER THAN REPLACED. Two independent runs six days and three commits apart, agreeing to within the run-to-run scatter and showing the identical 22-byte line tag, is a different claim from one run's numbers -- and it is the only basis on which a single bench is worth quoting. The 22 bytes matter most: that is the mechanism the half-window bound is derived from, so its reproducing is what the bound rests on. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Four findings from reading the file against what the repository does. Two were wording; two were the repository being wrong and the file describing it faithfully. THE TWO CHECKS WERE PATH-FILTERED, AND THEY MUST NOT BE. check_terminology.sh and check_references.sh ran as a job inside host_tests.yml, which gates on the build files, cmake/, common/, core/, scripts/ and test/host/. Both checks select their input with git ls-files and scan EVERY tracked file, so any file at all can carry a finding -- and a change touching only docs/ and platform/ ran neither of them. That is not hypothetical. The commit earlier on this branch that removed twelve unpublishable references touched exactly docs/ and platform/, and its message notes that the reference check passed on all twelve. As a pull request it would have merged with neither check having run. The file states the principle this violates: a workflow that gates no pull request anybody opens is worse than no workflow, because it looks like coverage. A path filter is a property of a workflow rather than of a job, so the checks move to repo_checks.yml with no paths on either trigger. A fifth workflow rather than wider filters on the fourth: widening host_tests.yml would run a full instrumented build and a coverage pass on every typo, where these two need no toolchain, no build and no cache. AND THE REFERENCE COMPILER WAS NOT THE ONE CI USED. The file names GCC 14 as the Linux reference and says CI pins these versions. install.sh installed build-essential, which on ubuntu-24.04 is GCC 13.3 -- measured, not inferred. install.sh now installs gcc-14 and g++-14 alongside it, and host_tests.yml names CC and CXX so the version is exact where it has to be. It deliberately does NOT rewire the default gcc: a dependency installer should not change which compiler every other build on a contributor's machine picks up, and the file already says a local build with a different version is fine while a verified one is not. Built strict with GCC 14 before pinning it, because a newer compiler under warnings-as-errors is exactly where new diagnostics appear: clean, and the suite passes. THE COVERAGE FLOOR WAS DESCRIBED AS A REPORT. "Pass coverage for a gcovr report" undersold the strongest quality statement here: it writes a report and then runs gcovr a second time over the seven fully reachable files of core/src, and FAILS THE BUILD below 100% of lines or of branches. The failure condition is now written down, along with why branches carry as much as lines. The workflow step was called "Coverage"; it is now called what it does. AND ZX_THREADX WAS NOWHERE IN THE FILE. A contributor reading only this one could not learn that the model and silicon runners need it to build the ThreadX guest images. Both runner rows now name it, with a worked invocation and what happens without it -- the guests are skipped with a configure-time message rather than an error, so most of the suite still runs, but a change to the launch path or anything temporal is not verified until it has been run with the variable set. Verified while here: CMake 3.28 matches cmake_minimum_required, the gcovr pin matches install.sh, the seven-file floor matches the script, the dev-targeting rule and the component list are both still right. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Five places said the certification back end is funded, or called work "funded": two in comments on the partition-switch path and the validator, and three in docs/coverage.md and docs/wcet-inputs.md. All five publish with the component. None of them broke a rule and both checkers passed on all five. But a statement about a project's budget is not a fact about the code, and a header comment is an odd place to assert one -- it dates faster than anything around it, it is not something a contributor can verify or act on, and where it sat it was doing no work: what those comments needed to say is that the code is INTENDED FOR CERTIFICATION, which is why MC/DC coverage has to stay achievable and why an indirect call does not belong on the switch path. That reasoning stands on its own and now says so without the budget. The two headings lose it too. "Where the funded work should start" is a list of the places a worst-case-execution-time analysis would begin from; whether that work is resourced is somebody else's question and does not change the list. "Structural coverage of target code belongs to the certification phase" says what the section says and nothing more. Comments only, plus two headings. No behaviour changes, and nothing that rests on the reasoning moves: verified with both cross builds, the host suite at 100% of lines and branches under GCC 14, and both repository checks. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Both failures were real and neither reproduced on this machine before it was made to behave like a runner. That is the finding worth keeping. THE ATfE PATH NEVER CROSSED INTO THE GUEST SUB-BUILD. ZoneX's clang toolchain file takes ZX_ATFE_TOOLCHAIN_PATH; the ThreadX one the guest images are built with takes ATFE_TOOLCHAIN_PATH, without the prefix. Nothing bridged the two, and an ExternalProject inherits nothing that is not listed in its CMAKE_ARGS -- which the file next door already says, about warnings-as-errors, for the same reason. So the guest fell back to whatever clang was on PATH. On a machine that keeps ATfE at the default location that is the right compiler, which is why this built here and has probably never been exercised anywhere else: the workflows trigger on dev and main, and a fork's feature branch reaches neither, so the clang lane had never seen this code until the pull request opened. On the runner, ATfE is unpacked into the workspace and the default does not exist, so it picked the system clang and could not compile for a bare-metal Cortex-R52. The compiler's own directory is forwarded rather than the variable, because that is right however the toolchain file found it -- passed on the command line, or defaulted. Both boards, since both configure guest sub-projects. AND THE COVERAGE FLOOR BROKE ON A gcov THAT DID NOT MATCH ITS gcc. That one is mine, from the commit before: pinning CC=gcc-14 without pinning gcov left gcovr shelling out to the image's default gcov, which refuses a .gcno written by a different major -- "version 'B42*', prefer 'B33*'" -- and ends the run with no coverage rather than with wrong coverage. run.sh now derives gcov from CC when CC names a versioned gcc, and fails loudly if the matching gcov is absent rather than producing that error a second time. A run with CC unset is unchanged, so a plain local invocation behaves as it did. Verified by reproducing both conditions rather than by reasoning about them: the clang lane with HOME pointed at an empty directory so the default ATfE path is unavailable, and coverage from a clean build tree with CC=gcc-14 -- 974 of 974 lines and 469 of 469 branches, and again with CC unset. Both GCC cross builds and both repository checks still pass. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Contributor
Author
|
A note on what the green checks cover: the That evidence exists and is in the pull request body — 24/24 on the Armv8-R AEM FVP and the full silicon matrix on an S32Z280-594EVB, both re-run on this revision — but it comes from a workstation and a development board rather than from CI. #6 records the gap and what closing it needs. |
Every one of the seventeen was headed "MISRA C:2012 deviations (justified)",
and several contained the opposite: an argument that the rule is OBSERVED.
Two said so outright -- "observed rather than violated" -- and others
described assembly isolated in a one-line function, which is Directive 4.3
being complied with rather than deviated from.
The cost of that was a heading nobody could count from, and not slightly:
Directive 4.3 appears in eleven blocks and exactly two of them are deviations.
Anyone auditing by grepping the headings would have found eleven.
Three headings now, chosen per block by reading it:
MISRA C:2012 deviations (justified) 7 blocks, one of which
records having none
MISRA C:2012 notes: deviations and compliance 7 blocks carrying both
MISRA C:2012 compliance notes 3 blocks arguing a rule is
observed, recorded because
the question arises there
Ten blocks retitled; the seven that were already accurate are untouched.
Comment text is otherwise unchanged -- no justification was rewritten, added
or removed, and the box width of each line is preserved exactly, including the
three files whose header row was already one column wider than its
neighbours.
Verified as a no-op on the build: host suite at 974 of 974 lines and 469 of
469 branches under GCC 14, both cross builds, both repository checks.
Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
Two documents for two readers neither of the existing ones serves. docs/phase-0-evidence.md answers "what did this establish, what did it cost, and what should be built next" in one place. README.md is written for someone cloning the repository, docs/decisions.md for someone changing the code, and the documentation site for a ThreadX user; none of them is a summary of the evidence. It carries the claim and the non-claim, the six-phase run that is the central exhibit, the numbers with their conditions, the eleven builds that must fail, the certification posture, and what the measurements de-risk. It cites rather than restates wherever a derivation already has a home, so what it adds is one copy of the measured figures rather than one copy of the reasoning. What it will not do is imply more than was measured: interrupt latency is not measured at all, there is no structural coverage of the port, boot to first partition entry is not instrumented, and each of those is said in the document rather than left to be noticed. It also carries the maintenance rule the repository lacked. A silicon figure lives in four prose files that have to move together, and two further copies carry the DERIVED bound instead and do not move with a run. That distinction has been paid for twice in one week; it is now written down. docs/misra-deviations.md is the index over the per-site annotations. The convention -- name the rule, justify it where it occurs -- was already met, but a per-site record cannot answer how many deviations there are or where they cluster. There are EIGHTEEN, across seven rules, and the useful fact is the distribution: every one is in the port, the board support or the examples except two, a single-point-of-exit deviation in the fault decoder and one narrowing assignment in the schedule printer. Neither touches isolation or timing, so the architecture-independent core that carries the coverage floor is very nearly deviation-free and the deviations sit where the code meets the hardware. Compiling it is what found the heading problem fixed in the commit before, and it lists the compliance notes separately so that the count is not inflated by them. Both are explicit about what they are not. The deviation index is assembled by reading source rather than by a checking tool, so it is evidence of discipline and not of coverage; a qualified record, tool-produced against a stated rule set and accounting for every rule rather than only the deviated ones, belongs to the certification package and does not exist. Assisted-by: Claude Code (Opus 5) <noreply@anthropic.com>
This was referenced Sep 9, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
ZoneX is a deterministic partitioning hypervisor for Armv8-R, and this is the whole of its Phase 0: 37 commits introducing a new component into an empty repository. It is a component introduction rather than a change, so this describes what is here rather than what moved.
This is not production software and is not close to it. It is a demonstrator, built to establish that a small set of mechanisms work on real Armv8-R silicon and to measure what they cost.
What it does
Two ThreadX kernels run at EL1 on one logical Cortex-R52 core, each confined to its own stage-2 window, time-sharing the core under a static major frame taken from a manifest — on the Armv8-R AEM FVP and on the NXP S32Z280-594EVB. Partition A holds seven ticks of every ten and partition B three, and each partition's clock advances by its own windows and by nothing else.
Neither partition can read, write or execute the other's memory or the hypervisor's, and not because it is asked not to: a partition that grants itself its neighbour's memory in its own EL1 MPU is still refused by stage 2, stopped, and reported with the partition, the address and the guest PC. The other partition runs to the end of the frame with its schedule untouched.
A window ends whether the partition agrees or not. The hypervisor's timer sits in GIC Group 0, so it arrives as an FIQ at EL2, and with
HCR.FMOsetPSTATE.Fis ignored at EL0 and EL1. One build proves it by trying: a partition that masks IRQ and FIQ and spins for ever is preempted exactly on schedule, and all its masking costs it is its own kernel's tick.What it measures, and the one thing that is wrong
A regression sweeps fourteen isolation cases in one run and measures the critical partition's window period continuously while the untrusted one is steered through five behaviours. On the board, over six hundred major frames, A's 800,000-count period moves by 22 counts while its neighbour idles, 24 while that neighbour computes with its own interrupts masked, and 185 while it commits a hundred and three thousand boundary violations. An independent run six days earlier, on an earlier revision, gave 21, 22 and 304 with the same 22-byte console hypercall — so these are a reproduced measurement rather than one run's luck.
Nothing a partition does through the schedule reaches its neighbour. Computing, masking its own interrupts and violating its boundary without pause each move the critical partition's period by tens of counts.
What reaches it is the hypervisor's own console driver. A guest that prints moves that period by up to one line tag — 22 bytes at 115,200 8N1, 17,640 counts of the board's 8 MHz counter — every run. That is a defect in ZoneX, not a limit of the partitioning, and it is bounded, derived and reproducible.
That defect is in the repository with its mechanism named, its cost measured and its cure scoped, rather than smoothed out of the claim.
docs/decisions.mdD31 has the measurement;docs/wcet-inputs.mdsection 4 has what removing it takes — an interrupt-driven driver with a polled fallback the fault path can force, because the fault reporter prints at the moment ZoneX has already failed once.It is tracked as the next change rather than as part of a later phase, and deliberately so: it is far smaller than any phase, it is the highest-value change available at its size, and grouping it with work of a different order of magnitude is the surest way to leave the qualification standing indefinitely.
What it does not do
Dual-core lockstep presents as one logical core, so this is temporal and memory partitioning on a single core. It is not spatial partitioning across multiple cores; that needs split-mode SMP and is deferred. Interrupt virtualisation with a bounded worst-case latency, inter-partition communication, the full time-partition scheduler, supervised partition restart, TraceX integration and the safety-artifact package are later phases.
Interrupt latency is not measured at all: guest interrupts go straight to EL1, and bounding them needs the GIC List Registers this phase does not use.
Every timing figure comes from one part on one bench, with the EL2 caches off, built
-Og, and with no clock tree configured — the core runs on the part's power-up RC oscillator. They are a first measurement with its conditions stated, not characterisation.How it is tested
Two suites, and which one a change belongs in is deliberate.
test/host/run.sh— the architecture-independent logic. 8 tests. 100% of lines and 100% of branches over the seven fully reachable files incore/src, enforced as a floor by the build rather than reported. Branches are the half that does the work: the failures those files exist to prevent live in the arms nobody took.test/fvp/run.sh— 24 tests on the Armv8-R AEM FVP, each judged by the image's own self-reported verdict. 24/24.test/s32z280/run.sh— the same images on the S32Z280-594EVB, loaded and judged over a debug probe. This is where every timing claim comes from; a green model run is not evidence about a part.The suite includes builds that must fail, registered as such, because a check that has never been seen to fail is not evidence that it can: a violation aimed at an address the payload is granted, an image told it needs more MPU regions than exist, a manifest whose two windows overlap, a hypervisor whose own tick cannot be delivered, a region limit one granule too generous, the per-partition time freeze removed, a shared read-only granule its reader may write, and ZoneX faulting inside its own fault report. Each must report failure on the check it was built to violate and on no other. One starting to pass fails the suite.
The port itself — CP15 assembly, the EL2 vectors, MPU programming, the context switch — is not gcov-measurable from a workstation, and instrumenting it on the target would change the code generation of the thing being measured.
docs/coverage.mdrecords which files are held to the floor, which are not, and what stands in for them. No number in this repository should be read as structural coverage of the port; that needs its own tooling and is a later concern.Verified on this revision
Host suite: 8 tests, 100% of 974 lines and 469 branches, enforced as a floor, under the pinned
gcovrand GCC 14 with warnings as errors. FVP suite: 24/24. Silicon, on the tree this pull request publishes: the probe, the two-partition image and the six-hundred-frame regression all pass;HMAIR0reads0x004400ff, which is the value the port's static assertions bind; and two negative builds each fail on exactly the check they were built to violate and on no other.The silicon run was taken because three of these commits moved the memory-type vocabulary and the region granule between headers. Those moves are behaviour-neutral and their agreement is asserted at compile time, but only a real part confirms the programmed memory attributes still work — and legible console output is that confirmation, since Normal attributes corrupt it.
Certification posture
Written MISRA-aware and coverage-friendly from the first commit, because the question a safety audience asks first is whether the code was shaped for it.
MIDRreads r1p3 and is printed by the probe on every run, so a different part reports itself rather than inheriting the conclusion. Seven Cortex-R52 errata are open at r1p3; four are debug and trace only; the three in scope do not apply, and the reasons are indocs/errata.mdso a reader can check the reasoning rather than take the conclusion. Two standing constraints fall out of the sweep and are recorded for code not yet written.MPUIR— a property of the part, not of a guest, not of a manifest, and not of anything that can change during a run.docs/wcet-inputs.mdis the input to the worst-case-execution-time work: every path a switch or a trap can take, read with one question — is anything here data-dependent? — with what is known about each. It is not a WCET analysis; it is the list of places one would have to start, so that later work begins from measurements rather than a fresh reading of the source.Conventions this repository settles
-Wpedanticin force.scripts/check_terminology.shrejects the register and concept names that belong to other architectures. It runs in CI, unfiltered, on every pull request.docs/decisions.mdrecords the design decisions and why each was taken, including the ones that were corrected by measurement.docs/armv8r-el2-reference.mdis the verified register sheet — it exists so that no session re-derives an encoding, and it records what was measured where the manuals disagree. Three of those disagreements were consequential enough to change the code.Review notes
Squash-merge, per project convention. Every commit carries an
Assisted-by:trailer: this work was AI-assisted, as the Eclipse Foundation's Generative AI Usage Guidelines require to be disclosed, and the file headers carry the matching AI Disclosure paragraph.Companion documentation pull request: eclipse-threadx/rtos-docs-asciidoc#59
Closes #3. Closes #4.