An overview of the register tracking liveness algorithm.
Previous versions posted here: [1], [2], [3].
- Changes from RFC to v2 (suggested by Andrii Nakryiko):
- wording corrected to use term "stack slot" instead of "stack spill";
- parentage chain diagram updated to show nil links for frame #1;
- added example for non-BPF_DW writes behavior;
- explanation in "Read marks propagation for cache hits" is reworked.
- Changes from v2 to v3:
- lot's of grammatical / wording fixes as suggested by David Vernet;
- "Register parentage chains" section is fixed to reflect what
happens to r1-r5 when function call is processed (as suggested by David and Alexei);
- Example in "Liveness marks tracking" section updated to explain
why partial writes should not lead to REG_LIVE_WRITTEN marks
(suggested by David);
- "Read marks propagation for cache hits" section updates:
- Explanation updated to hint why read marks should be propagated
before jumping to example (suggested by David);
- Removed box around B/D in the diagram updated (suggested by Alexei).
- Changes from v3 to v4 (suggested by Edward Cree):
- register parentage chain diagram updated to explain why r6 mark is
not propagated;
- read mark propagation algorithm pseudo-code fixed to correctly
show "if state->live & REG_LIVE_WRITTEN" stop condition;
- general wording improvements in section "Liveness marks tracking".
[1] https://lore.kernel.org/bpf/20230124220343.2942203-1-eddyz87@xxxxxxxxx/
[2] https://lore.kernel.org/bpf/20230130182400.630997-1-eddyz87@xxxxxxxxx/
[3] https://lore.kernel.org/bpf/20230131181118.733845-1-eddyz87@xxxxxxxxx/
Eduard Zingerman (1):
docs/bpf: Add description of register liveness tracking algorithm
Documentation/bpf/verifier.rst | 295 +++++++++++++++++++++++++++++++++
1 file changed, 295 insertions(+)
--
2.39.0
