Keyboard Shortcuts

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

Thirty Encodings, Round-Tripped and Cross-Checked

25 minadvancedModule 2: Atomics and Ordering, and the Instructions That Imply LOCKContinues from x86-order
25 min · The x86-64 Data Path

Why this concept is the course

Everything in the five previous pages is a measurement of the hardware. This one measures the artifact that measured the hardware, and it is here because of a specific failure: the first encoder in this course round-tripped 28 of 28 and was wrong.

$ ./vecdump | sed -n '/WHY A SECOND READER/,/proves it\./p'
  WHY A SECOND READER IS NOT OPTIONAL, and this file is the
  argument.  The first encoder in this course round-tripped
  28 of 28 and was WRONG: it wrote the two-byte VEX with the
  three-byte field order, and a decoder built from the same
  wrong table agreed with it perfectly.  A round trip is a
  tautology and it certified a broken encoder.  R9.
                

Twenty-eight out of twenty-eight, and the encoder was emitting legal bytes for a different instruction — which is the worst kind of wrong. There is no trap to catch it, because the bytes are valid; there is no length to be surprised by, because the length is right. Every test that compares a thing to itself passes, and the only test that would have caught it is one that brings in a reader nobody on the project wrote.

So this concept builds three readers instead of one: an encoder, a decoder, and objdump. The first two are written from the same table and are therefore a consistency check. The third was not written from that table by anybody on this project and is therefore a check. The difference between those two words is the entire content of this page.

Thirty cases, and three numbers that are not the same claim

The encoder emits its own bytes to a flat binary, the build script assembles that binary verbatim, and objdump -D -b binary disassembles it. That means the second reader is reading bytes this file produced, not bytes someone typed. Here is the table — nine legacy rows, seventeen VEX, four EVEX:

$ ./vecdump | sed -n '/^  MAP  | addps/,/^  MAP  | vpxor/p'
  MAP  | addps xmm0,xmm1                  | 0f 58 c1 | roundtrip | objdump agrees
  MAP  | addpd xmm0,xmm1                  | 66 0f 58 c1 | roundtrip | objdump agrees
  MAP  | movaps xmm0,xmm1                 | 0f 28 c1 | roundtrip | objdump agrees
  MAP  | movups xmm0,xmm1                 | 0f 10 c1 | roundtrip | objdump agrees
  MAP  | movdqa xmm0,xmm1                 | 66 0f 6f c1 | roundtrip | objdump agrees
  MAP  | movdqu xmm0,xmm1                 | f3 0f 6f c1 | roundtrip | objdump agrees
  MAP  | pxor xmm0,xmm1                   | 66 0f ef c1 | roundtrip | objdump agrees
  MAP  | mulps xmm0,xmm1                  | 0f 59 c1 | roundtrip | objdump agrees
  MAP  | addps xmm0,[rbx]                 | 0f 58 03 | roundtrip | objdump agrees
  MAP  | vaddps xmm2,xmm1,xmm0            | c5 f0 58 d0 | roundtrip | objdump agrees
  MAP  | vaddps ymm2,ymm1,ymm0            | c5 f4 58 d0 | roundtrip | objdump agrees
  MAP  | vaddpd ymm2,ymm1,ymm0            | c5 f5 58 d0 | roundtrip | objdump agrees
  MAP  | vaddps ymm10,ymm0,ymm0           | c5 7c 58 d0 | roundtrip | objdump agrees
  MAP  | vmovaps ymm0,[rbx]               | c5 fc 28 03 | roundtrip | objdump agrees
  MAP  | vaddps zmm0,zmm1,zmm2            | 62 f1 74 48 58 c2 | roundtrip | objdump agrees
  MAP  | vaddps zmm0{k2},zmm1,zmm2        | 62 f1 74 4a 58 c2 | roundtrip | objdump agrees
  MAP  | vaddps zmm0,zmm1,zmm2{ru-sae}    | 62 f1 74 58 58 c2 | roundtrip | objdump agrees

  30 cases, 30 round-tripped, 30 cross-checked against
  objdump, 0 disagreed.
                

Three numbers, and the artifact is explicit that they are not the same claim:

THE THREE NUMBERS ARE NOT THE SAME CLAIM. "round-tripped" the encoder and the decoder agree with each other. NECESSARY and NOT SUFFICIENT. Two readers built from one table will agree whether or not the table is right. "objdump agrees" an implementation that was NOT written from this table read the same bytes and named the same instruction. This is the claim worth making. "0 disagreed" a count, and the only one of the three that would change if the second reader were the thing that was broken.

That last row is the one that is easy to miss and it is where the most instructive failure in this course lives. The first version of the cross-check reported 28 disagreements out of 30, and the file reported them as evidence that the encoder was broken. The encoder was perfect. The reader of the disassembly was off by one row: objdump prints a section header before the first instruction, that line has no mnemonic in it, and the loader counted it as row 0. Every row was then compared against its neighbour’s text — and the two rows that reported agreement did so only because both of them happen to be vaddps.

THE LESSON, and it is worth more than the thirty bytes. A cross-check that DISAGREES with almost everything is as SUSPICIOUS as one that AGREES with everything. The two failure modes a misaimed check can have -- all-disagree and all-agree -- look nothing like each other and are EQUALLY WRONG. The only reason this one was caught is that the number was checked against what a CORRECT run looks like, and not against whether it felt right.

And the structural fix, which is the kind of thing worth copying: the loader now prints how many lines it skipped, and the harness asserts the counts.

$ ./vecdump | grep 'vecmaps_dis.txt'
  vecmaps_dis.txt                    loaded, 30 rows  (1 header, 290 padding skipped)
                

One header, 290 padding lines, thirty instructions. A harness that only checked “thirty rows loaded” would pass the broken loader, because both loaders read thirty lines. Asserting the shape of the input is what makes the parse checkable, and the same discipline is in the alignment probe, where the build script disassembles the probe bodies and the harness asserts the mnemonics are present — because a probe the compiler deleted also returns cleanly.

What the second reader found that the first could not

Three bugs, and all three had the same signature:

$ ./vecdump | sed -n '/AND THE CROSS-CHECK IS WHAT FOUND/,/surprised by\./p'
  AND THE CROSS-CHECK IS WHAT FOUND THE THREE BUGS that the
  round trip could not: the two-byte VEX field order, the
  inversion of R and X and B, and the fact that the L bit
  is TWO bits wide in EVEX and one in VEX.  All three
  produced LEGAL BYTES for A DIFFERENT INSTRUCTION, which
  is the worst kind of wrong: there is no trap to catch it
  and no length to be surprised by.
                

And one more that is not a bug but a fact nobody had written down: the operand map. In a three-operand instruction the fields are

$ ./vecdump | sed -n '/THE OPERAND MAP/,/R10 is that mistake/p'
  THE OPERAND MAP, which is not in any of the tables above and
  which this file established by assembling three distinct
  registers and reading which field each landed in:
      Intel 'vaddps DEST, SRC1, SRC2'
        ModRM.reg = DEST   vvvv = SRC1   ModRM.rm = SRC2
  A reader who assumes the GPR convention -- r/m is always the
  destination -- will mis-decode every three-operand instruction
  in the set.  R10 is that mistake, caught by the assembler.
                

That map is not in any specification table, because it is not a property of the encoding — it is a property of which register you named. So it cannot be looked up, and the only trustworthy way to learn it is to assemble three distinct registers and read which field each landed in, which is a five-line experiment. The assembly course’s map concept established the general form; this file re-derived it because a table you did not derive yourself is a table you cannot check.

Twenty-four retractions, sorted, and the one that took three attempts

Every retraction in the course is printed by the artifact and asserted as text by the harness, so a taken-back claim can be neither quietly dropped nor edited into being right. Sorted by what kind of mistake each one is:

$ ./vecdump | sed -n '/AND THE ONES THAT ARE NOT ABOUT/,/ends on\./p'
  AND THE ONES THAT ARE NOT ABOUT THE ARCHITECTURE AT ALL
  are R8, R11, R16, R17, R19, R21, R23 and R24, and they
  are the eight a reader should take away from this
  course: every one of them is a measurement that was
  WRONG about the machine and RIGHT about its own
  instrument.  Six of the twenty-four are mistakes about
  what a NUMBER is (R2, R4, R18, R19, R20 and R22),
  SEVEN are about what an INSTRUMENT is (R3, R8, R11,
  R16, R21, R23 and R24), three are about what an
  ENCODING is (R9, R10 and R15), and the rest are about
  what a BINARY contains or what a SPECIFICATION says.
  Not one of the twenty-four is a mistake about how a
  computer works, and that is the argument the course
  ends on.
                

Not one of the twenty-four is a mistake about how a computer works. Six are mistakes about what a number is (a lock dec reported non-atomic because the expectation was wrong, btc reported exact because the instrument could not read it). Seven are mistakes about what an instrument is — a probe the compiler deleted, a static array the compiler folded, a thread id that was never used, a section header counted as an instruction. Three are mistakes about what an encoding is. And the eight that are not about the architecture at all are the eight worth taking away, because every one of them is a measurement that was wrong about the machine and right about its own instrument.

Which brings us to the one that took three attempts, and it is the best story in the course because the tell was visible the whole time and the file printed it without objecting.

$ ./vecdump | sed -n '/R24\. /,/should have been SMALLER/p'
  R24. "The arm labelled 'store to my line, then load the
        peer's' is a two-thread ping-pong."  RETRACTED, and it
        took THREE attempts to fix, which is why it is here at
        that length.
        ONE.  The body took a THREAD ID and never used it
        TWO.  Indexing by id was not enough...  aligned(64)
        is not a promise about the elements; it is a promise
        about the object.
        THREE.  The fix is a STRIDE: a line is 64 bytes and a
        uint64_t is 8, so each thread gets a row of eight.
        THE TELL, and it is the part worth keeping: the
        store-only floor came out ABOVE the ping-pong in every
        run.  That is impossible for a floor, and this file
        PRINTED THE RATIO instead of treating it as a
        contradiction of its own vocabulary.  A row's NAME is a
        claim about what the row did, and a name is not
        evidence.
                

Three bugs, and the first two produced numbers that looked entirely reasonable. aligned(64) on a two-element array aligns the array, not each element, so the two threads’ words were still eight bytes apart in one cache line — and the experiment that was supposed to show that two separate lines are cheaper than one shared line was in fact measuring the shared line twice. The fix that worked was a stride: eight words per thread, because a line is 64 bytes and a word is 8.

And the tell. The store-only floor came out above the thing it was a floor for, in every single run. That is impossible — a floor is a lower bound by definition — and the file printed the ratio rather than treating it as a contradiction of its own vocabulary. The general form is the most useful thing on this page: a number that cannot have come out is the friendliest thing an experiment ever does, and the only way to deserve it is to hold a claim that says the number should have been smaller. A test that says “faster” passes when the instrument is broken; a test that says “slower” fails, and hands you the instrument.

Apply it

  1. Reproduce the whole thing.cd courses/x86simd/assets/samples && ./build_samples.sh. (Expect 266 checks, 30 rows with objdump agrees on every one, and a build that runs the artifact three times and cross-checks a fourth. The recorded vecdump.out ships with the course precisely so that the harness is runnable on a machine that never ran the benchmark — a course whose claims can only be checked by first rebuilding its own artifact is a course whose claims are only verifiable on the machine that wrote them.)
  2. Break the cross-check on purpose. This is the completion criterion. Delete the header-skip in load_dis() in vecmaps.c so objdump’s section header is counted as row 0 again. (Expect group I to report 28 disagreements out of 30 for an encoder that is entirely correct, and expect the two rows that still agree to be the two that both happen to be vaddps. Then restore it and watch it go back to 30. If your breakage produces all-agree instead, you have removed the wrong check — and that is worth noticing, because it is the other failure mode and it looks better.)
  3. Break the round trip, and watch it pass. Swap the R and X bits in the encoder so it writes them the right way up. (Expect the round-trip column to stay at 30 of 30, because the decoder has the same inversion. Then run objdump -D -b binary vecmaps.bin by hand and see the register names come out wrong. This is the cleanest demonstration in the collection of what a tautology looks like from the inside: every test you wrote passes and the program is broken.)
  4. Reproduce the floor tell. In vec5.c, change LINE_WORDS from 8 to 2 and rerun. (Expect the layout block to print “8 bytes apart (THE SAME LINE)” and the store floor to come back out above the ping-pong. Then let the harness run and watch group G fail on the ordering rather than on a number — which is the shape of a check that is about the claim and not about the digits. Then put it back.)
  5. Write your own second reader. Take any encoder you have written, and check it against something you did not write. (Expect the round trip to pass and expect at least one row to disagree, and expect the disagreement to be a field whose meaning you had silently assumed. The class of bug is narrow — a field that depends on another field, a bit that is inverted, a width that changed between extension and base — and it is invisible to every test that compares the encoder to itself.)

Connect

Backwards, everything. This concept is the account of the instrument that produced the other five, and the two things it is not are worth naming: it does not measure the hardware, and it does not measure the course. The assembly course’s map concept found the R/X/B inversion that this file re-found from the other direction; the third course’s last concept proved that CR4.OSXSAVE is unreadable from ring 3 and this course’s third concept infers it; and the SIMD course’s compiler concept is the same class of failure — a measurement that ran the wrong instruction — in a place where no disassembler is available to catch it.

Forwards, and the chain in this section is now complete. The x86-64 data path course was the fourth and last of the four, and it inherits from the first three: the encoding from x86asm, the calling convention from x86abi, the #GP as a signal number from x86sys. What it gives back is the one thing all three needed and none of them could supply: a second reader. A decoder that was not written from your table is the only instrument in this collection that has caught a real encoding bug, and it has now caught one in every course in the section that has one.

Outward. The transferable idea is not about x86 at all, and it is the one every neutral course in this collection is built on: a test that compares a thing to itself cannot fail in a way that means anything. Round trips, benchmarks that measure their own overhead, a compiler’s vectoriser checked against its own output, a lock-free queue checked against a lock, a course’s own diagram checked against its own prose. The second reader is the only defence, it costs one command, and it is skipped exactly when the code looks most finished.

render_lesson_js(&mut page)