On Wed, 2023-02-01 at 16:13 +0000, Edward Cree wrote: > On 01/02/2023 15:14, Eduard Zingerman wrote: > > I can update this remark as follows: > > > > ---- 8< --------------------------- > > > > Current +-------------------------------+ > > state | r0 | r1-r5 | r6-r9 | fp-8 ... | > > +-------------------------------+ > > \ > > r6 read mark is propagated via these links > > all the way up to checkpoint #1. > > The checkpoint #1 contains a write mark for r6 > > because of instruction (1), thus read propagation > > does not reach checkpoint #0 (see section below). > Yep, that's good. > > > TBH, I'm a bit hesitant to put such note on the diagram because > > liveness tracking algorithm is not yet discussed. I've updated the > > next section a bit to reflect this, please see below. > Yeah I didn't mean put that bit on the diagram. Just 'somewhere'. > > > I intentionally avoided description of this mechanics to keep some > > balance between clarity and level of details. Added a note that there > > is some additional logic. > Makes sense. > > > All in all here is updated start of the section: > > > > ---- 8< --------------------------- > > > > The principle of the algorithm is that read marks propagate back along the state > > parentage chain until they hit a write mark, which 'screens off' earlier states > > from the read. The information about reads is propagated by function > > ``mark_reg_read()`` which could be summarized as follows:: > Hmm, I think you want to still also have the bit about "For each > processed instruction..."; otherwise the reader seeing "The > principle of the algorithm" will wonder "*what* algorithm?" > Don't have an immediate suggestion of how to wordsmith the two > together though, sorry. How about the following? ---- 8< --------------------------- For each processed instruction, the verifier tracks read and written registers and stack slots. The main idea of the algorithm is that read marks propagate back along the state parentage chain until they hit a write mark, which 'screens off' earlier states from the read. The information about reads is propagated by function ``mark_reg_read()`` which could be summarized as follows:: ---- >8 --------------------------- > > > Notes: > > * The read marks are applied to the **parent** state while write marks are > > applied to the **current** state. The write mark on a register or stack slot > > means that it is updated by some instruction verified within current state. > "Within current state" is blurry and doesn't emphasise the key > point imho. How about: > The write mark on a register or stack slot means that it is > updated by some instruction in the straight-line code (/basic > block?) leading from the parent state to the current state. Sounds good, thank you. > > > * Details about REG_LIVE_READ32 are omitted. > > * Function ``propagate_liveness()`` (see section :ref:`Read marks propagation > > for cache hits`) might override the first parent link, please refer to the > > comments in the source code for further details. > "comments on that function's source code" perhaps, so they know > where to find it. If they have to look all the way through > verifier.c's 15,000 lines for a relevant comment it could take > them quite a while ;) Sounds good. > > > Thanks a lot for commenting! > > wdyt about my updates? > I think we're getting pretty close and I look forward to giving > you a Reviewed-by on v4 :) > (But make sure to Cc me as I'm not subscribed to bpf@vger.) Sure, will do.
