Fix a claim in the ring buffer blueprint: the trace file does say how many

[tamnd]

What this fixes

A claim in trace-ring-buffer, merged in #69, that is wrong.

The blueprint said the trace file does not say that events were lost. It does. The header of that file carries entries-in-buffer/entries-written, and the second of those two numbers is not a counter the writer keeps: it is this processor's kept events plus its overrun, added up at the moment the header is printed. On the capture in section 5 it would read 273/44275.

What is actually true

Narrower, and more useful than what was there before. Neither way of reading a trace gives you both halves of the answer.

The trace file says how many, once, at the top, in a header a reader skips on the way to the lines. It marks nothing in the body, so the body reads exactly the same whether nothing was lost or almost everything was. The header is also a display option rather than part of the format, so echo 0 > options/context-info removes the one admission the file makes.

trace_pipe is the other way round. It prints CPU:0 [LOST 44002 EVENTS] at the position the loss happened, so it says where, and it has no header at all.

Two readers of the same buffer, each of which is missing a different half. That is a better sentence than the one it replaces, and it has the advantage of being true.

The project already knew

TraceLog in kxray/models/flat.py reads that banner into in_buffer and written, has a lost property that subtracts them, and its docstring says a trace where the two differ has holes in it that nothing in the body of the file admits to. The parser was right and the blueprint disagreed with it.

What changed

• Section 3 gains a step 22 for where the header number comes from, and the lead sentence now counts to 22.
• The opening, section 6 and section 9 are corrected.
• Invariant 11 is unchanged and still holds. The iterator's missed events flag really is never set on an ordinary buffer, and its consequence is that nothing marks the body, which is what the note under it now says.
• The diagram gains the header line as a box and a bottom band reading "each way of reading a trace tells you half of what was lost". Alt text updated to match.
• Three new citations, R76 to R78, confirmed against the pinned tree: the seq_printf that prints the header, the addition of ring_buffer_overrun_cpu into the total, and the CONTEXT_INFO test that can remove the header.

Gates

All of them, locally. bpc: 5 blueprint(s) clean, refcheck: paths clean, 210 citation(s), baseline: 41 artefact(s), 7968 line(s), 0 unparsed, lintprose: 41 file(s) clean.