| Message ID | 20230131181118.733845-2-eddyz87@gmail.com (mailing list archive) |
|---|---|
| State | Superseded |
| Delegated to: | BPF |
| Headers | show |
| Series | docs/bpf: Add description of register liveness tracking algorithm | expand |
On 31/01/2023 18:11, Eduard Zingerman wrote: > This is a followup for [1], adds an overview for the register liveness > tracking, covers the following points: > - why register liveness tracking is useful; > - how register parentage chains are constructed; > - how liveness marks are applied using the parentage chains. > > [1] https://lore.kernel.org/bpf/CAADnVQKs2i1iuZ5SUGuJtxWVfGYR9kDgYKhq3rNV+kBLQCu7rA@mail.gmail.com/ > > Signed-off-by: Eduard Zingerman <eddyz87@gmail.com> > --- > Documentation/bpf/verifier.rst | 280 +++++++++++++++++++++++++++++++++ > 1 file changed, 280 insertions(+) ... > + Current +-------------------------------+ > + state | r0 | r1-r5 | r6-r9 | fp-8 ... | > + +-------------------------------+ > + \ > + r6 read mark is propagated via > + these links all the way up to > + checkpoint #1. Perhaps explicitly mention here that the reason it doesn't propagate to checkpoint #0 (despite the arrow) is that there's a write mark on c1[r6]. Also worth mentioning somewhere that write marks are really a property of the arrow, not the state — a write mark in c#1 tells us that the straight-line code from c#0 to c#1 contains a write (thus 'breaking' that arrow for read mark propagation); it lives in c#1's data structures because it's c#1 that needs to 'know' about it, whereas c#0 (and its parents) need to 'know' about any *reads* in the straight-line code from c#0 to c#1 (but these are of no interest to c#1). I sometimes summarise this with the phrase "read up, write down", though idk how useful that is to anyone outside of my head ;) > +Liveness marks tracking > +======================= > + > +For each processed instruction, the verifier propagates information about reads > +up the parentage chain and saves information about writes in the current state. > +The information about reads is propagated by function ``mark_reg_read()`` which > +could be summarized as follows:: > + > + mark_reg_read(struct bpf_reg_state *state): > + parent = state->parent > + while parent: > + if parent->live & REG_LIVE_WRITTEN: > + break This isn't correct; we look at `state->live` here, because if in the straight-line code since the last checkpoint (parent) there's a write to this register, then reads should not propagate to `parent`. Then there's the complication of the `writes` variable in mark_reg_read(); that's explained by the comment on propagate_liveness(), which AFAICT you don't cover in your doc section about that. (And note that `writes` is only ever false for the first iteration through the mark_reg_read() loop). > + if parent->live & REG_LIVE_READ64: > + break > + parent->live |= REG_LIVE_READ64 > + state = parent > + parent = state->parent > + > +Note: details about REG_LIVE_READ32 are omitted. > + > +Also note: the read marks are applied to the **parent** state while write marks > +are applied to the **current** state. May be worth stating that the principle of the algorithm is that read marks propagate back along the chain until they hit a write mark, which 'screens off' earlier states from the read. Your doc implies this but afaict never states it explicitly, and I think it makes the algo easier to understand for someone who doesn't already know what it's all about. Apart from that, this is great. I particularly like your diagram of the parentage chains. -ed
On Wed, 2023-02-01 at 11:00 +0000, Edward Cree wrote: > On 31/01/2023 18:11, Eduard Zingerman wrote: > > This is a followup for [1], adds an overview for the register liveness > > tracking, covers the following points: > > - why register liveness tracking is useful; > > - how register parentage chains are constructed; > > - how liveness marks are applied using the parentage chains. > > > > [1] https://lore.kernel.org/bpf/CAADnVQKs2i1iuZ5SUGuJtxWVfGYR9kDgYKhq3rNV+kBLQCu7rA@mail.gmail.com/ > > > > Signed-off-by: Eduard Zingerman <eddyz87@gmail.com> > > --- > > Documentation/bpf/verifier.rst | 280 +++++++++++++++++++++++++++++++++ > > 1 file changed, 280 insertions(+) > ... > > + Current +-------------------------------+ > > + state | r0 | r1-r5 | r6-r9 | fp-8 ... | > > + +-------------------------------+ > > + \ > > + r6 read mark is propagated via > > + these links all the way up to > > + checkpoint #1. Hi Edward, could you please review the updates below? > Perhaps explicitly mention here that the reason it doesn't > propagate to checkpoint #0 (despite the arrow) is that there's > a write mark on c1[r6]. 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). --------------------------- >8 ---- > > Also worth mentioning somewhere that write marks are really a > property of the arrow, not the state — a write mark in c#1 tells > us that the straight-line code from c#0 to c#1 contains a write > (thus 'breaking' that arrow for read mark propagation); it lives > in c#1's data structures because it's c#1 that needs to 'know' > about it, whereas c#0 (and its parents) need to 'know' about any > *reads* in the straight-line code from c#0 to c#1 (but these are > of no interest to c#1). > I sometimes summarise this with the phrase "read up, write down", > though idk how useful that is to anyone outside of my head ;) 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. > > > +Liveness marks tracking > > +======================= > > + > > +For each processed instruction, the verifier propagates information about reads > > +up the parentage chain and saves information about writes in the current state. > > +The information about reads is propagated by function ``mark_reg_read()`` which > > +could be summarized as follows:: > > + > > + mark_reg_read(struct bpf_reg_state *state): > > + parent = state->parent > > + while parent: > > + if parent->live & REG_LIVE_WRITTEN: > > + break > This isn't correct; we look at `state->live` here, because if in > the straight-line code since the last checkpoint (parent) > there's a write to this register, then reads should not > propagate to `parent`. You are correct, thank you for catching it (:big facepalm image:). > Then there's the complication of the `writes` variable in > mark_reg_read(); that's explained by the comment on > propagate_liveness(), which AFAICT you don't cover in your > doc section about that. (And note that `writes` is only ever > false for the first iteration through the mark_reg_read() loop). 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. > > > + if parent->live & REG_LIVE_READ64: > > + break > > + parent->live |= REG_LIVE_READ64 > > + state = parent > > + parent = state->parent > > + > > +Note: details about REG_LIVE_READ32 are omitted. > > + > > +Also note: the read marks are applied to the **parent** state while write marks > > +are applied to the **current** state. > May be worth stating that the principle of the algorithm is that > read marks propagate back along the chain until they hit a write > mark, which 'screens off' earlier states from the read. > Your doc implies this but afaict never states it explicitly, and > I think it makes the algo easier to understand for someone who > doesn't already know what it's all about. 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:: mark_reg_read(struct bpf_reg_state *state, ...): parent = state->parent while parent: if state->live & REG_LIVE_WRITTEN: break if parent->live & REG_LIVE_READ64: break parent->live |= REG_LIVE_READ64 state = parent parent = state->parent 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. * 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. --------------------------- >8 ---- > > Apart from that, this is great. I particularly like your diagram > of the parentage chains. Thanks a lot for commenting! wdyt about my updates?
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. > 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. > * 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 ;) > 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.) -ed
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.
On 01/02/2023 18:28, Eduard Zingerman wrote: > 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 --------------------------- SGTM.
diff --git a/Documentation/bpf/verifier.rst b/Documentation/bpf/verifier.rst index 3afa548ec28c..34093d60fe87 100644 --- a/Documentation/bpf/verifier.rst +++ b/Documentation/bpf/verifier.rst @@ -316,6 +316,286 @@ Pruning considers not only the registers but also the stack (and any spilled registers it may hold). They must all be safe for the branch to be pruned. This is implemented in states_equal(). +Some technical details about state pruning implementation could be found below. + +Register liveness tracking +========================== + +In order to make state pruning effective, liveness state is tracked for each +register and stack slot. The basic idea is to track which registers and stack +slots are actually used during subseqeuent execution of the program, until +program exit is reached. Registers and stack slots that were never used could be +removed from the cached state thus making more states equivalent to a cached +state. This could be illustrated by the following program:: + + 0: call bpf_get_prandom_u32() + 1: r1 = 0 + 2: if r0 == 0 goto +1 + 3: r0 = 1 + --- checkpoint --- + 4: r0 = r1 + 5: exit + +Suppose that a state cache entry is created at instruction #4 (such entries are +also called "checkpoints" in the text below). The verifier could reach the +instruction with one of two possible register states: + +* r0 = 1, r1 = 0 +* r0 = 0, r1 = 0 + +However, only the value of register ``r1`` is important to successfully finish +verification. The goal of the liveness tracking algorithm is to spot this fact +and figure out that both states are actually equivalent. + +Data structures +=============== + +Liveness is tracked using the following data structures:: + + enum bpf_reg_liveness { + REG_LIVE_NONE = 0, + REG_LIVE_READ32 = 0x1, + REG_LIVE_READ64 = 0x2, + REG_LIVE_READ = REG_LIVE_READ32 | REG_LIVE_READ64, + REG_LIVE_WRITTEN = 0x4, + REG_LIVE_DONE = 0x8, + }; + + struct bpf_reg_state { + ... + struct bpf_reg_state *parent; + ... + enum bpf_reg_liveness live; + ... + }; + + struct bpf_stack_state { + struct bpf_reg_state spilled_ptr; + ... + }; + + struct bpf_func_state { + struct bpf_reg_state regs[MAX_BPF_REG]; + ... + struct bpf_stack_state *stack; + } + + struct bpf_verifier_state { + struct bpf_func_state *frame[MAX_CALL_FRAMES]; + struct bpf_verifier_state *parent; + ... + } + +* ``REG_LIVE_NONE`` is an initial value assigned to ``->live`` fields upon new + verifier state creation; + +* ``REG_LIVE_WRITTEN`` means that the value of the register (or stack slot) is + defined by some instruction "executed" within verifier state; + +* ``REG_LIVE_READ{32,64}`` means that the value of the register (or stack slot) + is read by some instruction "executed" within verifier state; + +* ``REG_LIVE_DONE`` is a marker used by ``clean_verifier_state()`` to avoid + processing same verifier state multiple times and for some sanity checks; + +* ``->live`` field values are formed by combining ``enum bpf_reg_liveness`` + values using bitwise or. + +Register parentage chains +========================= + +In order to propagate information between parent and child states, a *register +parentage chain* is established. Each register or stack slot is linked to a +corresponding register or stack slot in its parent state via a ``->parent`` +pointer. This link is established upon state creation in ``is_state_visited()`` +and might be modified by ``set_callee_state()`` called from +``__check_func_call()``. + +The rules for correspondence between registers / stack slots are as follows: + +* For the current stack frame, registers and stack slots of the new state are + linked to the registers and stack slots of the parent state with the same + indices. + +* For the outer stack frames, only caller saved registers (r6-r9) and stack + slots are linked to the registers and stack slots of the parent state with the + same indices. + +* When function call is processed a new ``struct bpf_func_state`` instance is + allocated, it encapsulates a new set of registers and stack slots. For this + new frame, parent links for r6-r9 and stack slots are set to nil, parent links + for r1-r5 are set to match caller r1-r5 parent links. + +This could be illustrated by the following diagram (arrows stand for +``->parent`` pointers):: + + ... ; Frame #0, some instructions + --- checkpoint #0 --- + 1 : r6 = 42 ; Frame #0 + --- checkpoint #1 --- + 2 : call foo() ; Frame #0 + ... ; Frame #1, instructions from foo() + --- checkpoint #2 --- + ... ; Frame #1, instructions from foo() + --- checkpoint #3 --- + exit ; Frame #1, return from foo() + 3 : r1 = r6 ; Frame #0 <- current state + + +-------------------------------+-------------------------------+ + | Frame #0 | Frame #1 | + Checkpoint +-------------------------------+-------------------------------+ + #0 | r0 | r1-r5 | r6-r9 | fp-8 ... | + +-------------------------------+ + ^ ^ ^ ^ + | | | | + Checkpoint +-------------------------------+ + #1 | r0 | r1-r5 | r6-r9 | fp-8 ... | + +-------------------------------+ + ^ ^ ^ + |_______|_______|_______________ + | | | + nil nil | | | nil nil + | | | | | | | + Checkpoint +-------------------------------+-------------------------------+ + #2 | r0 | r1-r5 | r6-r9 | fp-8 ... | r0 | r1-r5 | r6-r9 | fp-8 ... | + +-------------------------------+-------------------------------+ + ^ ^ ^ ^ ^ + nil nil | | | | | + | | | | | | | + Checkpoint +-------------------------------+-------------------------------+ + #3 | r0 | r1-r5 | r6-r9 | fp-8 ... | r0 | r1-r5 | r6-r9 | fp-8 ... | + +-------------------------------+-------------------------------+ + ^ ^ + nil nil | | + | | | | + Current +-------------------------------+ + state | r0 | r1-r5 | r6-r9 | fp-8 ... | + +-------------------------------+ + \ + r6 read mark is propagated via + these links all the way up to + checkpoint #1. + +Liveness marks tracking +======================= + +For each processed instruction, the verifier propagates information about reads +up the parentage chain and saves information about writes in the current state. +The information about reads is propagated by function ``mark_reg_read()`` which +could be summarized as follows:: + + mark_reg_read(struct bpf_reg_state *state): + parent = state->parent + while parent: + if parent->live & REG_LIVE_WRITTEN: + break + if parent->live & REG_LIVE_READ64: + break + parent->live |= REG_LIVE_READ64 + state = parent + parent = state->parent + +Note: details about REG_LIVE_READ32 are omitted. + +Also note: the read marks are applied to the **parent** state while write marks +are applied to the **current** state. + +Because stack writes could have different sizes ``REG_LIVE_WRITTEN`` marks are +applied conservatively: stack slots are marked as written only if write size +corresponds to the size of the register, e.g. see function ``save_register_state()``. + +Consider the following example:: + + 0: (*u64)(r10 - 8) = 0 ; define 8 bytes of fp-8 + --- checkpoint #0 --- + 1: (*u32)(r10 - 8) = 1 ; redefine lower 4 bytes + 2: r1 = (*u32)(r10 - 8) ; read lower 4 bytes defined at (1) + 3: r2 = (*u32)(r10 - 4) ; read upper 4 bytes defined at (0) + +As stated above, the write at (1) does not count as ``REG_LIVE_WRITTEN``. Should +it be otherwise, the algorithm above wouldn't be able to propagate the read mark +from (3) to checkpoint #0. + +Once the ``BPF_EXIT`` instruction is reached ``update_branch_counts()`` is +called to update the ``->branches`` counter for each verifier state in a chain +of parent verifier states. When the ``->branches`` counter reaches zero the +verifier state becomes a valid entry in a set of cached verifier states. + +Each entry of the verifier states cache is post-processed by a function +``clean_live_states()``. This function marks all registers and stack slots +without ``REG_LIVE_READ{32,64}`` marks as ``NOT_INIT`` or ``STACK_INVALID``. +Registers/stack slots marked in this way are ignored in function ``stacksafe()`` +called from ``states_equal()`` when a state cache entry is considered for +equivalence with a current state. + +Now it is possible to explain how the example from the beginning of the section +works:: + + 0: call bpf_get_prandom_u32() + 1: r1 = 0 + 2: if r0 == 0 goto +1 + 3: r0 = 1 + --- checkpoint[0] --- + 4: r0 = r1 + 5: exit + +* At instruction #2 branching point is reached and state ``{ r0 == 0, r1 == 0, pc == 4 }`` + is pushed to states processing queue (pc stands for program counter). + +* At instruction #4: + + * ``checkpoint[0]`` states cache entry is created: ``{ r0 == 1, r1 == 0, pc == 4 }``; + * ``checkpoint[0].r0`` is marked as written; + * ``checkpoint[0].r1`` is marked as read; + +* At instruction #5 exit is reached and ``checkpoint[0]`` can now be processed + by ``clean_live_states()``. After this processing ``checkpoint[0].r0`` has a + read mark and all other registers and stack slots are marked as ``NOT_INIT`` + or ``STACK_INVALID`` + +* The state ``{ r0 == 0, r1 == 0, pc == 4 }`` is popped from the states queue + and is compared against a cached state ``{ r1 == 0, pc == 4 }``, the states + are considered equivalent. + +Read marks propagation for cache hits +===================================== + +Another point is the handling of read marks when a previously verified state is +found in the states cache. Upon cache hit verifier must behave in the same way +as if the current state was verified to the program exit. This means that all +read marks, present on registers and stack slots of the cached state, must be +propagated over the parentage chain of the current state. Example below shows +why this is important. Function ``propagate_liveness()`` handles this case. + +Consider the following state parentage chain (S is a starting state, A-E are +derived states, -> arrows show which state is derived from which):: + + r1 read + <------------- A[r1] == 0 + C[r1] == 0 + S ---> A ---> B ---> exit E[r1] == 1 + | + ` ---> C ---> D + | + ` ---> E ^ + |___ suppose all these + ^ states are at insn #Y + | + suppose all these + states are at insn #X + +* Chain of states ``S -> A -> B -> exit`` is verified first. + +* While ``B -> exit`` is verified, register ``r1`` is read and this read mark is + propagated up to state ``A``. + +* When chain of states ``C -> D`` is verified the state ``D`` turns out to be + equivalent to state ``B``. + +* The read mark for ``r1`` has to be propagated to state ``C``, otherwise state + ``C`` might get mistakenly marked as equivalent to state ``E`` even though + values for register ``r1`` differ between ``C`` and ``E``. + Understanding eBPF verifier messages ====================================
This is a followup for [1], adds an overview for the register liveness tracking, covers the following points: - why register liveness tracking is useful; - how register parentage chains are constructed; - how liveness marks are applied using the parentage chains. [1] https://lore.kernel.org/bpf/CAADnVQKs2i1iuZ5SUGuJtxWVfGYR9kDgYKhq3rNV+kBLQCu7rA@mail.gmail.com/ Signed-off-by: Eduard Zingerman <eddyz87@gmail.com> --- Documentation/bpf/verifier.rst | 280 +++++++++++++++++++++++++++++++++ 1 file changed, 280 insertions(+)