Keyboard Shortcuts

Ctrl+K
Open search
Esc
Close search / dialog
↑
Back to top

What Is Measured Here, What Is Quoted, and What You Cannot Conclude

22 minadvancedModule 1: The Modes: Getting In, Getting Out, and Being InterruptedContinues from a64-pagetables
22 min · The AArch64 Machine: Modes, Memory and Faults

Why this matters

Everything in the last five concepts carries one of three labels, and on most pages you would be forgiven for not noticing. This page prints all of them, in one table, with the count.

The reason to do that is not fastidiousness. It is that this course is about a machine that does not exist on the machine that wrote it, and a course with that property has exactly one advantage over a course with hardware — it is forced to be explicit about which claims are which kind — and a course that does not take the advantage has thrown away the only thing it had that the x86-64 section did not. So this page is the concept that makes the other five trustworthy, and it is last for the same reason a64-verify is last in the encoding course and a64-unwind is last in the ABI course.

THE THREE LABELS, and the only honest treatment MEASURED an experiment on the compiler, the assembler, the object file or the bytes. Reproducible with one command. MEASURED-ON-BYTES a property of the emitted BYTES, read TWICE -- by the decoder in the artifact and by llvm-objdump-21 -- and the two readers are compared word by word. QUOTED a manual claim, with the document and the section printed beside it, and never mixed in with a measurement.

The table: fifty-seven claims, and the ratio is the finding

$ python3 a64sys.py --section 10 | tail -60
  The whole course, one line per claim, with the label it carries
  and the section that establishes it.  57 claims.

  1 syscall
    MEASURED-ON-BYTES   the syscall number is a 16-bit unsigned field at     sec 3, 4
    MEASURED           the assembler accepts 0..65535 and refuses both     sec 3
    MEASURED           Linux puts the same number in x8, and clang uses    sec 4
    MEASURED           x0-x7 receive the arguments in argument order      sec 4
    MEASURED           the ninth argument is not a register               sec 4
    QUOTED             a Linux syscall takes at most six arguments        sec 2, 4
    QUOTED             __NR_write is 64 and __NR_read is 63                sec 2
    QUOTED             the SVC traps to EL1 and the kernel returns in x0   sec 2
    ...
  6 evidence
    MEASURED           the two readers agree on every word of this corpus  sec 9
    MEASURED           the check detects a poisoned guard                  sec 9B
    MEASURED           the inherited HINT guard is one bit too narrow       sec 3

  21 MEASURED, 5 MEASURED-ON-BYTES, 31 QUOTED, 57 total
  54% of the claims in this course are QUOTED
                

That ratio is the finding, not a disclaimer. The subject of this course is a machine, and the machine is the one thing this host does not have, so a majority of the claims about the machine are quotations. What the course can measure — and does, twenty-six times — is the encoding, the compiler and the object file, and those are exactly the three things a learner writing a backend has to get right and exactly the three that do not need a CPU.

The distribution is also not random, and the shape is worth noticing: concept 5 is almost entirely measured, concept 3 is half measured, and concepts 2 and 4 are mostly quoted. That is a direct consequence of what each one is about. A descriptor format is a document; a relocation is a file.

The two absences, printed before the first measurement

$ python3 a64sys.py --section 1 | sed -n '1,40p'
  ==========================================================================
  a64sys -- the artifact for "The AArch64 Machine: Modes, Memory and Faults"
  ==========================================================================
  THE METHOD IS FORCED AND IT IS STATED FIRST:
    there is no AArch64 machine on this host, no AArch64 emulator and
    no AArch64 linker, so NOT ONE INSTRUCTION IN THIS COURSE HAS
    BEEN RUN, and there are NO TIMINGS anywhere in this file or on any
    of its six pages.  The x86-64 section measured a 4.92x and a
    27.65x; nothing here has a counterpart and nothing here fakes one.

  ...
     aarch64-linux-gnu-ld     ABSENT  (AArch64 linker)
     qemu-aarch64             ABSENT  (AArch64 emulator)
     aarch64-linux-gnu-as     ABSENT  (a SECOND AArch64 assembler)
     aarch64-linux-gnu-gcc    ABSENT  (an AArch64 GCC)
                

Four absences, and the fourth is the one that is easy to forget: there is no second AArch64 assembler. Every refusal quoted anywhere in this course is a refusal by clang 21.1.8's integrated assembler and by nothing else, and both readers of the two-reader check come from one LLVM tree. So the check establishes that this decoder and one other piece of software agree on what the bytes mean — not that either agrees with silicon.

The measurement that makes the zero mean something: the poison

Six files, four optimisation levels, 1,516 instructions, 0 disagreements. And that number is worthless on its own, which is the entire reason section 9B exists.

$ python3 a64sys.py --section 9 | sed -n '/TOTAL/,/^$/p'
     TOTAL       1516 instructions read, 1516 NAMED by reader 1, 0 DISAGREEMENTS.

  [COVERAGE]         reader 1 names 1516 of 1516 words, so 0 are unmodelled
  [RECONCILED]       the alias rules that fired, each with its count, because
  []                 a normalisation that is not counted is a fudge:
     ldr      -> ldr       320
     adrp     -> adrp      298
     ret      -> ret       208
     ...
     movz     -> mov       46
     mrs      -> mrs        44
     ...
  [DISAGREE]         ZERO true disagreements.
                

Then one guard, one bit, and the same loop again:

  ==========================================================================
    9B  THE POISON: one guard, one bit, and the same loop again
  ==========================================================================

  [CLEAN]            1516 instructions read, 1516 named, 0 DISAGREEMENTS

  [POISONED]         with the poison in: 1459 named, 57 DISAGREEMENTS
     the named count moved from 1516 to 1459 -- 57 instructions
     the disagreement count moved from 0 to 57 -- 57 instructions

     the first few, printed BY NAME so a reader can check them:
     0xd5385208  reader 1: (op 0xd5385208)  reader 2: mrs x8, ESR_EL1
     0xd5384028  reader 1: (op 0xd5384028)  reader 2: mrs x8, ELR_EL1
     0xd5386008  reader 1: (op 0xd5386008)  reader 2: mrs x8, FAR_EL1
     0xd538c008  reader 1: (op 0xd538c008)  reader 2: mrs x8, VBAR_EL1
     0xd518c008  reader 1: (op 0xd518c008)  reader 2: msr VBAR_EL1, x8
                

1,516 to 1,459 named, 0 to 57 disagreements, and every one of the 57 is an mrs or an msr printed by name. A check that has never been seen to fail is a check with no reason to be believed, and this one has now been seen to fail, which is the only property that makes the zero mean anything.

And the choice of which guard to poison is not arbitrary: mrs/msr is the family this course added, so poisoning it measures this course's contribution rather than the inherited decoder's. Poisoning an inherited guard would produce a larger number and a less informative one, because a reader could not tell how much of the movement was the poison and how much was the twenty-one models that arrived with the file.

The bug that made the poison necessary

Before the poison there was a retraction, and it is the most valuable thing in the course. The encoding course's decoder has a model whose own claim is "NOP, WFI, YIELD and the rest: 27 fixed bits and a 5-bit hint number", and whose guard is bits[31:5]:

     hint      word        word >> 5   guard matches?
     nop       0xd503201f  0x6a81900   YES
     yield     0xd503203f  0x6a81901   no
     wfe       0xd503205f  0x6a81902   no
     wfi       0xd503207f  0x6a81903   no
     sev       0xd503209f  0x6a81904   no
     sevl      0xd50320bf  0x6a81905   no
     dgh       0xd50320df  0x6a81906   no
     bti       0xd503241f  0x6a81920   no
     bti c     0xd503245f  0x6a81922   no
     bti j     0xd503249f  0x6a81924   no
     bti jc    0xd50324df  0x6a81926   no

     ONE of ELEVEN.
                

The body of that model is correct — it reads the hint number and has the right eleven names — and the guard makes eight of them unreachable. And the reason it survived a whole course is the sentence that generalises further than anything else in this file:

R4, and the most transferable sentence in the course WHY IT SURVIVED The encoding course's own corpus, compiled with clang, contains no yield, no wfe, no wfi, no sev, no sevl, no dgh and no bti. A model that is wrong about eight words the corpus does not contain is INDISTINGUISHABLE from a model that is right, and that course's artifact reports its unmodelled words as "9, and the unmodelled ones are Advanced SIMD" -- a true sentence about a corpus in which the bug cannot appear. A count of unmodelled words is a fact about A CORPUS and not about A DECODER. And the second reader cannot help: `llvm-objdump` also prints `(op 0x...)` for a word no rule claims. Two readers that agree because they both DECLINE TO ANSWER is not a cross-check; it is a shared ignorance with two implementations.

And here is the number that makes the whole thing concrete. The same loop over the same corpus, with three different sets of models:

  [MEASURED] what each course's models contribute to THIS corpus

     dispatch                                read  named  coverage
     the encoding course's 21 alone        1516   1374   90.6%
     + the ABI course's 6                 1516   1385   91.4%
     + this course's 6                    1516   1516  100.0%

  [RESULT]           the encoding course names 1374 of 1516 of this corpus
                     (90.6%), and the two later courses add 11 and 131
                

A coverage number means nothing on its own — it is a number about a corpus. So the same loop is run three times with three different sets of models, and that is what turns "100% named" from a boast into a number. 1374 of 1516 words of a corpus whose whole subject is the SYSTEM class, and 142 of the 33 models written by the two courses that came after the first.

Worked: the retraction list, and the fifteen limits

Sixteen retractions, printed in full by the artifact in section 11 with a source for each, and asserted as text by the harness so that a retraction can be neither quietly dropped nor edited into being right. Here they are in one table, with what replaced what:

  R1   "the syndrome is a 32-bit field: EC, IL, ISS"
       -> it is 32 bits INSIDE a 64-bit register, bits 55:32
          are ISS2, and a 32-bit mask throws it away

  R2   "the syscall number is the immediate in the SVC"
       -> BOTH are in the emitted code: the field is the
          architectural half and x8 is the Linux half

  R3   the inherited decoder covers the encoding well enough
       -> it names FIVE words of the SYSTEM class, and every
          instruction in this course is outside those five

  R4   "NOP, WFI, YIELD and the rest"
       -> NOP alone: the guard is one bit too narrow, and
          matches 1 of 11 hints the assembler accepts

  R5   one relocation per address reference, as SYSCALL does
       -> TWO, always, for every reference on AArch64

  R6   "x8 is the syscall-number register, so a compiler must
        treat it as reserved"
       -> clang uses it as a scratch in all four functions
          that do not mention it, at all four levels

  R7   the natural test is to shift the syndrome right by 26
       -> clang does not shift, and does not need to: THREE
          instructions, because 0x24 and 0x25 differ in one bit

  R8   the table needs 16 x 0x80 and `.align 11` is the way
       -> the size is right and the DIRECTIVE is only
          necessary; both ends assemble with no diagnostic

  R9   "`.align 11` and it is valid"
       -> necessary and NOT SUFFICIENT, and nothing checks it

  R10  "52-bit" means the high half is 52 bits of address
       -> it means a REGION of 2^52, mapped at the TOP, with
          TTBR1 = 0xffff000000000000

  R11  a page table is an ordinary array, so nothing
       distinguishes it
       -> its ALIGNMENT does, and the alignment is a property
          of the SECTION: 4096 without, 0x200000 with

  R12  a page needs a PAIR because the adrp reach is 4 GiB
       -> the reach is 4 GiB and IRRELEVANT; ADRP MASKS OFF
          the low twelve bits of the target

  R13  the four levels and the block sizes read as a MENU
       -> 2^27 entries are needed for a 2 MiB block at L1
          and a table has 512, so a 48-bit regime cannot use it

  R14  100% two-reader agreement is the strongest evidence
       -> it is not, and section 9B is the demonstration

  R15  the two-reader check establishes the decoder is correct
       -> it establishes AGREEMENT; a corpus chosen to suit
          the decoder is the failure mode this course found

  R16  a 30-bit virtual address space is configurable
       -> T0SZ is FIVE bits and 64-30 = 34 does not fit; the
          floor is 2^33 bytes
                

Seven of those sixteen were asserted before this course was written — in docs/aarch64-section-plan.md or in the brief this course was built from — and the artifact prints the source next to each one, because a retraction with no prior source is a course disagreeing with itself. Three of the sixteen were found by this course's own measurements against a draft it had already written, and they say so rather than claiming a prior source.

  A course that reports ZERO retractions on a subject this
  size has either not looked or has not been reading the
  documents it cites.  16 retractions.
                

The limits, in the file's own words

Fifteen of them, and the first two decide what every other one may say:

What a reader therefore cannot conclude from this course

Printed in the artifact, not in a footnote, because a limit that is a footnote is a limit that gets forgotten. This list is the honest end of the course and it is not a formality:

What a reader CAN conclude, and check, with a hex editor

That is the shape of a course with no hardware: a small set of claims you can check with a hex editor, and a large set you have to take on the word of a document — and an exact statement of which is which. A course with hardware would have the second set too, labelled MEASURED, and would be worth more for the parts that need it.

Apply it

  1. Run the harness with no toolchain at all.python3 courses/a64sys/assets/samples/crosscheck.py. (Expect 210/210 checks passed, with no assembler, no linker, no emulator and no network. The harness reads the committed a64sys.out rather than re-measuring, on purpose: a course whose claims can only be verified by first rebuilding its own artifact is a course whose claims are only verifiable on the machine that wrote them, which is the same mistake as quoting a remembered number wearing a different hat.)
  2. Do the poison yourself, and break a different guard the second time. Delete m_sysreg from the dispatch and re-run. (Expect 1,459 named and 57 disagreements, all mrs/msr. Then delete m_hint_family instead and re-run: expect 1,391 named and 125 disagreements, and expect the 125 to include the eight hints from the R4 table. Two runs, two guards, two different numbers, and the difference between them is the seven hundred words those two guards together cover — which is a coverage measurement you made by breaking something rather than by reading a table.)
  3. Make a claim of your own and label it. Write down one fact you learned on the previous five pages and put one of the three labels on it, with the document or the command. (Expect about half of them to be QUOTED if you are honest, and the exercise is worth doing because the half you get wrong will be the numbers, not the prose. A reader who mislabels a structural fact as measured has learned nothing wrong yet; a reader who mislabels a measured fact as quoted will go looking for a document that does not say it.)
  4. Find the corpus-dependent claim and check it against a different corpus. The coverage table on this page says the inherited decoder names 1,374 of 1,516 words of this corpus. Take a large real-world AArch64 binary, disassemble it, and count how many words this course's decoder names. (Expect a much lower percentage, and expect the unmodelled ones to be Advanced SIMD and the floating-point families — which this course does not model and the next course in the section does. The generalisation is the one R4 is about: a coverage number is a number about a corpus, so the interesting experiment is always to change the corpus and see what moves.)
  5. Write the paragraph you wish this course had, and mark it UNKNOWN. Pick one thing this page says cannot be concluded — the page fault behaviour, the ADRP relaxation, the instruction length rule — and write the sentence you would need to publish it, along with the machine you would need. (Expect the answer to be "an AArch64 board and four hours" for most of them, and expect the list of sentences to be shorter than you thought, because the course already measured everything a host without hardware can measure. That is the design: it is a course about a machine you cannot run, built the way a compiler author builds one — from the encoding outward, with the specification as the oracle and the compiler as the witness. The constraint is the subject, not a limitation of the teaching.)

Connect

Backwards, all five, and specifically: concept 5 is the one with the most measured content and therefore the one that most needs this page, because a page that is mostly measurements is exactly the page a reader is most likely to over-trust. Concept 3 contributed the largest absence in the course and this page is where the habit of printing an absence lives. Concept 1 is where the two-labels rule was first needed, because a field in an instruction and a value in a register are different kinds of claim and both are in the same line of assembly.

Sideways, the collection's own method. The encoding course's cross-check is the first application of the poison and it retracted its own 100% twice; the ABI course's unwinding concept is the second; this is the third, and R4 — a bug in an inherited artifact that survived a whole course because the corpus did not contain the words it was wrong about — is the first time the method has found a defect in a sibling course's file. The x86-64 course's boundary concept is the same idea applied to a course that did have hardware, and it proves an absence rather than asserting one — which is the harder case and the better precedent.

Outward, and the general form is the one the whole section has been converging on for six courses. Every claim in a course should be classifiable as reproducible-by-a-command, readable-in-a-file, or attributable-to-a-paragraph — and a claim that is none of the three is a claim nobody should act on. That is not a rule about courses without hardware; it is a rule about all of them, and a course with hardware is simply better at the second category and no better at the first or the third. The AArch64 section's contribution is that it has been forced to be explicit, and the reader who takes the habit out of here will apply it to a machine they can run — where the temptation is to treat a duration as a mechanism, and where the discipline costs nothing and saves a week.

And where this course ends. Sixteen retractions, fifteen limits, and a decoder with six models of its own that found a bug in its predecessor's and printed the arithmetic that killed a row in its own first draft. That is the whole of what a course about a machine you cannot run can honestly claim, and the two courses after this one in the section — the NEON register file and the weak memory model — are the ones where a reader should ask whether the same method would find as much, because the subject changes from control to data and the encodings get denser rather than sparser.

render_lesson_js(&mut page)