Every claim on the previous four pages 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 — and then it prints the twenty-seven retractions, the fourteen limits, and the three poisons.
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. A course that does not take the advantage has thrown away the only thing it had that the x86-64 section did not.
And this course took it further than any of the eleven before it, because the thing the advantage buys is a decoder, and a decoder turns out to be the most productive kind of thing to point a method at. Twenty-seven claims in this course were stated, then measured, then found wrong. Seven of them were found in a single afternoon and all seven by one change to a comparison.
$ python3 courses/a64simd/assets/samples/a64data.py --run | sed -n '/concept /,/^$/p'
concept label the claim section
------------ ----------------- -------------------------------------------- --------
neon MEASURED-ON-BYTES the access size is bits[31:30] PLUS bit 23 sec 2, 3
neon MEASURED `fadd h0, h1, h2` is REFUSED at baseline sec 2
neonspace MEASURED-ON-BYTES the SVE word is 0x04c00020 at 128..2048 b sec 4
atomic MEASURED-ON-BYTES in CAS acquire is bit 22, release bit 15 sec 7
atomic MEASURED-ON-BYTES in LDADD acquire is bit 23, release bit 22 sec 7
order MEASURED-ON-BYTES the barrier option field is bits[11:8] sec 8
order MEASURED zero barriers in every atomic of the corpus sec 9
dataflow MEASURED-ON-BYTES the encoder, decoder and assembler agree sec 11
dataflow MEASURED a normaliser that deletes an operand hides 85 sec 11
...
33 MEASURED, 19 MEASURED-ON-BYTES, 10 QUOTED, 62 total
16% of the claims in this course are QUOTED
neon 10 MEASURED, 5 MEASURED-ON-BYTES, 2 QUOTED (12% quoted)
neonspace 4 MEASURED, 3 MEASURED-ON-BYTES, 2 QUOTED (22% quoted)
atomic 8 MEASURED, 7 MEASURED-ON-BYTES, 2 QUOTED (12% quoted)
order 8 MEASURED, 2 MEASURED-ON-BYTES, 3 QUOTED (23% quoted)
dataflow 3 MEASURED, 2 MEASURED-ON-BYTES, 1 QUOTED (17% quoted)
Sixteen percent quoted, and that is lower than the machine course's fifty-four percent. The distribution is not random: it follows from what each concept is about. Concepts 1, 3 and 4 are about encodings and compilers, which is exactly what a host without hardware can measure; concept 2's quoted third is the shared-resource rule, which is a statement about an architecture and not about a byte. The moment a course needs to say what something does rather than what it is encoded as, the quoted fraction goes up — and that is a design constraint on any course in this collection, not a property of the subject.
Here is the finding, in the file's own words, because the paraphrase loses the part that matters.
A ZERO FROM A NORMALISER IS NOT A ZERO
Every number in section 11 is a number about a COMPARISON
as well as about the decoder, and this file has now produced
four normaliser bugs that each left the printed disagreement
count at zero while eighty-five real defects sat behind it:
a comma split that ignored brackets,
an operand list truncated after its first element,
a zero-offset rule written for the one spelling neither
reader emits,
and a shift-modifier rule for a spelling that does not exist.
Not one of them printed a wrong word. All four made the file
stop COMPARING, which is worse, because the number is believed.
Not one of them printed a wrong word. Every one of them made the file stop comparing — and that is strictly worse than printing a wrong word, because a wrong word would have shown up as a disagreement and a stopped comparison reports the same number as a working one. The encoding course filed the same shape as its R14; this course filed it four times in one file.
[CLEAN] 1038 instructions read, 1031 NAMED by reader 1, 0 DISAGREEMENTS
[POISON A] m_exclusive removed: 1038 read, 970 named (-61), 0 disagreements (+0)
[POISON B] m_lse removed: 1038 read, 1031 named ( +0), 5 disagreements (+5)
0x4862fc06 reader 1: ldaxp reader 2: caspal
0x48227c06 reader 1: stxp reader 2: casp
0xf8e10008 reader 1: ldur reader 2: ldaddal
[POISON C] bit 0 of every word: 1038 read, 945 named (-86), 837 disagreements (+837)
the control is LIVE if each poison moved its own
number: named MOVED, disagreements MOVED.
The first version of this file had one poison, and it could not fail. Removing m_exclusive moved the named count by 61 and the disagreement count by 0 — and the sentence printed underneath the numbers claimed that both had moved and that every difference was an exclusive. Both sentences were false, and the false number was printed right beside them. That is retraction R27.
So there are now three poisons, one per reported number, and each must move the number it claims to test or the run prints [POISON FAILED] and the harness fails. Poison B is the one worth understanding: removing m_lse changes no named counts at all and creates five disagreements, which is the only way to find out whether a decoder's wrong answers happen to be the same wrong answers as the second reader's. A decoder with a shared spec error does not move that number, and there is no other check in this file that would notice.
dispatch read named coverage
---------------------------------------- -------- -------- ----------
the 14 models of THIS course 1038 1031 99.3%
the 6 the machine course adds 1038 1024 98.7%
the 21 the encoding course imports 1038 860 82.9%
Three runs, three dispatch sets, because a coverage number is a number about a corpus and not about a decoder. And the corpus itself has a lesson attached that cost the course a retraction: for most of this file's life the exclusive-pair path was built to a .s and never to an .o, so the two-reader pass never saw a ldaxp at all — and m_lse was free to read 0xc87fa009 as caspal x31 for a whole draft, with a 99% coverage figure printed the entire time. A coverage number is a number about what was fed to it, and the build script now says so in a comment next to the line that was missing.
Twenty-seven, every one with the measurement that killed it and the source that asserted it. The five kinds, and the counts are read off the list rather than written beside it — because the first version of this summary printed the literal string "%d of them" and a retraction list with a wrong summary is the failure the list exists to catch.
about what an ENCODING is 14: R1, R2, R3, R4, R5, R12, R16, R18, R19,
R21, R23, R24, R25, R26
about what a COMPARISON is 1: R22
about a COMPILER VERSION is 4: R9, R11, R14, R15
about what an INSTRUMENT is 4: R6, R8, R17, R27
about what a SPEC says 4: R7, R10, R13, R20
Four of the five kinds are about tools. That is the section's real finding across twelve courses, and it is worth stating plainly: encoding bugs are common, and tool bugs are at least as common, and the tool bugs are the ones that survive review because a tool's output looks authoritative.
R22 "the corpus has no disagreements between the two readers"
-> it has EIGHTY-FIVE, and every one was a real decoder
defect hidden behind a normaliser
R23 "the scaled imm12 offset of a vector load is the access size
in BITS"
-> BYTES: `str s0, [sp, #12]` is 0xbd000fe0 with imm12 = 3
and 3 x 4 = 12. Five sizes at one source offset of 4080
give imm12 = 4080, 2040, 1020, 510 and 255
R24 "in CCMP the NZCV immediate is the second register field"
-> it is ALL FIVE BITS of bits[4:0] and the CONDITION is
bits[15:12]
R25 "the lane index of the scalar element copy is `imm5 >> 1`"
-> imm5 = (esz/8) * (2*index + 1), and the first version was
right for NO arrangement in the table
R26 "the 64-bit MOVI immediate is a number the decoder can decline"
-> it is a BYTE MASK: bit j of the field is byte j of the
value, 40 probes, 40 agreements
R27 "removing one model from the dispatch poisons the cross-check"
-> it poisons ONE of the two numbers
Read R23 and R25 together, because they are the pair worth having. R23 is off by a factor of eight — bits instead of bytes — and produced [sp, #96] where the byte offset is 12. R25 printed lane 6 where the lane is 1, and 6 is inside the legal range for that arrangement. Both produced a plausible number rather than an error, and a plausible number is the one thing nothing downstream can catch. That is why the second reader is necessary: not because a decoder is bad at arithmetic, but because a wrong number in the legal range is invisible from the inside.
And R26 is the subtlest. The first version of the model declined the 64-bit MOVI form and gave a true reason about the wrong field. A decoder that declines is the safest kind of wrong — it can never print a false number — and that is exactly why it is the kind that hides: a table showing reader 1: (none) reads like a known gap rather than an unasked question.
python3 courses/a64simd/assets/samples/crosscheck.py. (Expect 268/268 checks passed, with no assembler, no emulator and no network. It reads the committed a64data.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.)CORPUS_OBJECTS in a64data.py and re-run. (Expect the coverage row to change and the poison rows to still pass — and then notice that the disagreement count did not move, because a model whose words are simply absent from the corpus cannot disagree with anything. That is the R4 lesson from the machine course, restated for this course's own dispatch: a count of unmodelled words is a fact about a corpus.)_norm and add one of your own. (Expect it to fire zero times, and expect the zero to be invisible unless you count it. Every rule in this file is printed with the number of times it applied, and a rule that fires zero times is an error rather than a convenience — that is what the four bugs above were, and not one of them announced itself.)Backwards, all four. Acquire and Release Are Access Modes contributed the largest measured content and therefore most needs this page, because a page that is mostly measurements is exactly the page a reader is most likely to over-trust. The exclusive monitor contributed the retraction that made the section's method testable against itself — R21 was found by a cross-check disagreeing with an assembler, not by reading a specification.
Back into the section's earlier courses. The machine course's evidence concept is where the three labels and the poison come from, and the encoding course's cross-check is the first application of the method — it retracted its own 100% twice before this course was written. This course is the fourth application and the first to find that the poison itself was broken.
Sideways, and the contrast is the point. The x86-64 machine course had hardware and had to prove its boundary; the neutral smp course had hardware and could measure a lost update. Every course in this collection that had a machine had to work harder to say what it could not conclude, because a number is available and a number looks like an answer. The AArch64 section's contribution is not that it covers an architecture; it is that it built a method for a course whose subject is unavailable, and then checked the method against itself until it produced twenty-seven retractions and three working poisons.
Outward, and this is where the section ends. Four courses, four subject areas, one method: registers, memory, instructions, exceptions, page tables, calls, vectors, atomics, ordering. Measured where a host can measure them, quoted where it cannot, and retracted loudly where the two disagreed. The reader who takes the habit out of here has something that transfers to a machine they can run, where the temptation is different — to treat a duration as a mechanism, or a coverage figure as a correctness statement, or a zero as evidence — and where the discipline costs nothing and saves a week.