BPF List
 help / color / mirror / Atom feed
* [PATCH bpf-next v1 00/10] bpf: replace path-sensitive with path-insensitive live stack analysis
@ 2025-09-11  1:04 Eduard Zingerman
  2025-09-11  1:04 ` [PATCH bpf-next v1 01/10] bpf: bpf_verifier_state->cleaned flag instead of REG_LIVE_DONE Eduard Zingerman
                   ` (10 more replies)
  0 siblings, 11 replies; 22+ messages in thread
From: Eduard Zingerman @ 2025-09-11  1:04 UTC (permalink / raw)
  To: bpf, ast, andrii; +Cc: daniel, martin.lau, kernel-team, yonghong.song, eddyz87

Consider the following program, assuming checkpoint is created for a
state at instruction (3):

  1: call bpf_get_prandom_u32()
  2: *(u64 *)(r10 - 8) = 42
  -- checkpoint #1 --
  3: if r0 != 0 goto +1
  4: exit;
  5: r0 = *(u64 *)(r10 - 8)
  6: exit

The verifier processes this program by exploring two paths:
 - 1 -> 2 -> 3 -> 4
 - 1 -> 2 -> 3 -> 5 -> 6

When instruction (5) is processed, the current liveness tracking
mechanism moves up the register parent links and records a "read" mark
for stack slot -8 at checkpoint #1, stopping because of the "write"
mark recorded at instruction (2).

This patch set replaces the existing liveness tracking mechanism with
a path-insensitive data flow analysis. The program above is processed
as follows:
 - a data structure representing live stack slots for
   instructions 1-6 in frame #0 is allocated;
 - when instruction (2) is processed, record that slot -8 is written at
   instruction (2) in frame #0;
 - when instruction (5) is processed, record that slot -8 is read at
   instruction (5) in frame #0;
 - when instruction (6) is processed, propagate read mark for slot -8
   up the control flow graph to instructions 3 and 2.

The key difference is that the new mechanism operates on a control
flow graph and associates read and write marks with pairs of (call
chain, instruction index). In contrast, the old mechanism operates on
verifier states and register parent links, associating read and write
marks with verifier states.

Motivation
==========

As it stands, this patch set makes liveness tracking slightly less
precise, as it no longer distinguishes individual program paths taken
by the verifier during symbolic execution.
See the "Impact on verification performance" section for details.

However, this change is intended as a stepping stone toward the
following goals:
 - Short term, integrate precision tracking into liveness analysis and
   remove the following code:
   - verifier backedge states accumulation in is_state_visited();
   - most of the logic for precision tracking;
   - jump history tracking.
 - Long term, help with more efficient loop verification handling.

 Why integrating precision tracking?
 -----------------------------------

In a sense, precision tracking is very similar to liveness tracking.
The data flow equations for liveness tracking look as follows:

  live_after =
    U [state[s].live_before for s in insn_successors(i)]

  state[i].live_before =
    (live_after / state[i].must_write) U state[i].may_read

While data flow equations for precision tracking look as follows:

  precise_after =
    U [state[s].precise_before for s in insn_successors(i)]

  // if some of the instruction outputs are precise,
  // assume its inputs to be precise
  induced_precise =
    ⎧ state[i].may_read   if (state[i].may_write ∩ precise_after) ≠ ∅
    ⎨
    ⎩ ∅                   otherwise

  state[i].precise_before =
    (precise_after / state[i].must_write) ∩ induced_precise

Where:
 - `may_read` set represents a union of all possibly read slots
   (any slot in `may_read` set might be by the instruction);
 - `must_write` set represents an intersection of all possibly written slots
   (any slot in `must_write` set is guaranteed to be written by the instruction).
 - `may_write` set represents a union of all possibly written slots
   (any slot in `may_write` set might be written by the instruction).

This means that precision tracking can be implemented as a logical
extension of liveness tracking:
 - track registers as well as stack slots;
 - add bit masks to represent `precise_before` and `may_write`;
 - add above equations for `precise_before` computation;
 - (linked registers require some additional consideration).

Such extension would allow removal of:
 - precision propagation logic in verifier.c:
   - backtrack_insn()
   - mark_chain_precision()
   - propagate_{precision,backedges}()
 - push_jmp_history() and related data structures, which are only used
   by precision tracking;
 - add_scc_backedge() and related backedge state accumulation in
   is_state_visited(), superseded by per-callchain function state
   accumulated by liveness analysis.

The hope here is that unifying liveness and precision tracking will
reduce overall amount of code and make it easier to reason about.

 How this helps with loops?
 --------------------------

As it stands, this patch set shares the same deficiency as the current
liveness tracking mechanism. Liveness marks on stack slots cannot be
used to prune states when processing iterator-based loops:
 - such states still have branches to be explored;
 - meaning that not all stack slot reads have been discovered.

For example:

  1: while(iter_next()) {
  2:   if (...)
  3:     r0 = *(u64 *)(r10 - 8)
  4:   if (...)
  5:     r0 = *(u64 *)(r10 - 16)
  6:   ...
  7: }

For any checkpoint state created at instruction (1), it is only
possible to rely on read marks for slots fp[-8] and fp[-16] once all
child states of (1) have been explored. Thus, when the verifier
transitions from (7) to (1), it cannot rely on read marks.

However, sacrificing path-sensitivity makes it possible to run
analysis defined in this patch set before main verification pass,
if estimates for value ranges are available.
E.g. for the following program:

  1: while(iter_next()) {
  2:   r0 = r10
  3:   r0 += r2
  4:   r0 = *(u64 *)(r2 + 0)
  5:   ...
  6: }

If an estimate for `r2` range is available before the main
verification pass, it can be used to populate read marks at
instruction (4) and run the liveness analysis. Thus making
conservative liveness information available during loops verification.

Such estimates can be provided by some form of value range analysis.
Value range analysis is also necessary to address loop verification
from another angle: computing boundaries for loop induction variables
and iteration counts.

The hope here is that the new liveness tracking mechanism will support
the broader goal of making loop verification more efficient.

Validation
==========

The change was tested on three program sets:
 - bpf selftests
 - sched_ext
 - Meta's internal set of programs

Commit [#8] enables a special mode where both the current and new
liveness analyses are enabled simultaneously. This mode signals an
error if the new algorithm considers a stack slot dead while the
current algorithm assumes it is alive. This mode was very useful for
debugging. At the time of posting, no such errors have been reported
for the above program sets.

[#8] "bpf: signal error if old liveness is more conservative than new"

Impact on memory consumption
============================

Debug patch [1] extends the kernel and veristat to count the amount of
memory allocated for storing analysis data. This patch is not included
in the submission. The maximal observed impact for the above program
sets is 2.6Mb.

Data below is shown in bytes.

For bpf selftests top 5 consumers look as follows:

  File                     Program           liveness mem
  -----------------------  ----------------  ------------
  pyperf180.bpf.o          on_event               2629740
  pyperf600.bpf.o          on_event               2287662
  pyperf100.bpf.o          on_event               1427022
  test_verif_scale3.bpf.o  balancer_ingress       1121283
  pyperf_subprogs.bpf.o    on_event                756900

For sched_ext top 5 consumers loog as follows:

  File       Program                          liveness mem
  ---------  -------------------------------  ------------
  bpf.bpf.o  lavd_enqueue                           164686
  bpf.bpf.o  lavd_select_cpu                        157393
  bpf.bpf.o  layered_enqueue                        154817
  bpf.bpf.o  lavd_init                              127865
  bpf.bpf.o  layered_dispatch                       110129

For Meta's internal set of programs top consumer is 1Mb.

[1] https://github.com/kernel-patches/bpf/commit/085588e787b7998a296eb320666897d80bca7c08

Impact on verification performance
==================================

Veristat results below are reported using
`-f insns_pct>1 -f !insns<500` filter and -t option
(BPF_F_TEST_STATE_FREQ flag).

 master vs patch-set, selftests (out of ~4K programs)
 ----------------------------------------------------

  File                              Program                                 Insns (A)  Insns (B)  Insns    (DIFF)
  --------------------------------  --------------------------------------  ---------  ---------  ---------------
  cpumask_success.bpf.o             test_global_mask_nested_deep_array_rcu       1622       1655     +33 (+2.03%)
  strobemeta_bpf_loop.bpf.o         on_event                                     2163       2684   +521 (+24.09%)
  test_cls_redirect.bpf.o           cls_redirect                                36001      42515  +6514 (+18.09%)
  test_cls_redirect_dynptr.bpf.o    cls_redirect                                 2299       2339     +40 (+1.74%)
  test_cls_redirect_subprogs.bpf.o  cls_redirect                                69545      78497  +8952 (+12.87%)
  test_l4lb_noinline.bpf.o          balancer_ingress                             2993       3084     +91 (+3.04%)
  test_xdp_noinline.bpf.o           balancer_ingress_v4                          3539       3616     +77 (+2.18%)
  test_xdp_noinline.bpf.o           balancer_ingress_v6                          3608       3685     +77 (+2.13%)

 master vs patch-set, sched_ext (out of 148 programs)
 ----------------------------------------------------

  File       Program           Insns (A)  Insns (B)  Insns    (DIFF)
  ---------  ----------------  ---------  ---------  ---------------
  bpf.bpf.o  chaos_dispatch         2257       2287     +30 (+1.33%)
  bpf.bpf.o  lavd_enqueue          20735      22101   +1366 (+6.59%)
  bpf.bpf.o  lavd_select_cpu       22100      24409  +2309 (+10.45%)
  bpf.bpf.o  layered_dispatch      25051      25606    +555 (+2.22%)
  bpf.bpf.o  p2dq_dispatch           961        990     +29 (+3.02%)
  bpf.bpf.o  rusty_quiescent         526        534      +8 (+1.52%)
  bpf.bpf.o  rusty_runnable          541        547      +6 (+1.11%)

Perf report
===========

In relative terms, the analysis does not consume much CPU time.
For example, here is a perf report collected for pyperf180 selftest:

 # Children      Self  Command   Shared Object         Symbol
 # ........  ........  ........  ....................  ........................................
        ...
      1.22%     1.22%  veristat  [kernel.kallsyms]     [k] bpf_update_live_stack
        ...

Eduard Zingerman (10):
  bpf: bpf_verifier_state->cleaned flag instead of REG_LIVE_DONE
  bpf: use compute_live_registers() info in clean_func_state
  bpf: remove redundant REG_LIVE_READ check in stacksafe()
  bpf: declare a few utility functions as internal api
  bpf: compute instructions postorder per subprogram
  bpf: callchain sensitive stack liveness tracking using CFG
  bpf: enable callchain sensitive stack liveness tracking
  bpf: signal error if old liveness is more conservative than new
  bpf: disable and remove registers chain based liveness
  bpf: table based bpf_insn_successors()

 Documentation/bpf/verifier.rst                | 264 -------
 include/linux/bpf_verifier.h                  |  52 +-
 kernel/bpf/Makefile                           |   2 +-
 kernel/bpf/liveness.c                         | 723 ++++++++++++++++++
 kernel/bpf/log.c                              |  28 +-
 kernel/bpf/verifier.c                         | 564 ++++----------
 .../testing/selftests/bpf/prog_tests/align.c  | 178 ++---
 .../selftests/bpf/prog_tests/spin_lock.c      |  12 +-
 .../selftests/bpf/prog_tests/test_veristat.c  |  44 +-
 .../selftests/bpf/progs/exceptions_assert.c   |  34 +-
 .../selftests/bpf/progs/iters_state_safety.c  |   4 +-
 .../selftests/bpf/progs/iters_testmod_seq.c   |   6 +-
 .../bpf/progs/mem_rdonly_untrusted.c          |   4 +-
 .../selftests/bpf/progs/verifier_bounds.c     |  38 +-
 .../bpf/progs/verifier_global_ptr_args.c      |   4 +-
 .../selftests/bpf/progs/verifier_ldsx.c       |   2 +-
 .../selftests/bpf/progs/verifier_precision.c  |  16 +-
 .../selftests/bpf/progs/verifier_scalar_ids.c |  10 +-
 .../selftests/bpf/progs/verifier_spill_fill.c |  40 +-
 .../bpf/progs/verifier_subprog_precision.c    |   6 +-
 .../selftests/bpf/verifier/bpf_st_mem.c       |   4 +-
 21 files changed, 1107 insertions(+), 928 deletions(-)
 create mode 100644 kernel/bpf/liveness.c

-- 
2.47.3


^ permalink raw reply	[flat|nested] 22+ messages in thread
end of thread, other threads:[~2025-09-12 16:48 UTC | newest]

Thread overview: 22+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2025-09-11  1:04 [PATCH bpf-next v1 00/10] bpf: replace path-sensitive with path-insensitive live stack analysis Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 01/10] bpf: bpf_verifier_state->cleaned flag instead of REG_LIVE_DONE Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 02/10] bpf: use compute_live_registers() info in clean_func_state Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 03/10] bpf: remove redundant REG_LIVE_READ check in stacksafe() Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 04/10] bpf: declare a few utility functions as internal api Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 05/10] bpf: compute instructions postorder per subprogram Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 06/10] bpf: callchain sensitive stack liveness tracking using CFG Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 07/10] bpf: enable callchain sensitive stack liveness tracking Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 08/10] bpf: signal error if old liveness is more conservative than new Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 09/10] bpf: disable and remove registers chain based liveness Eduard Zingerman
2025-09-11 14:19   ` kernel test robot
2025-09-11 21:26     ` Eduard Zingerman
2025-09-11 22:00       ` Alexei Starovoitov
2025-09-11 22:07         ` Eduard Zingerman
2025-09-12  8:17   ` Dan Carpenter
2025-09-12 16:48     ` Eduard Zingerman
2025-09-11  1:04 ` [PATCH bpf-next v1 10/10] bpf: table based bpf_insn_successors() Eduard Zingerman
2025-09-11  6:57 ` [syzbot ci] Re: bpf: replace path-sensitive with path-insensitive live stack analysis syzbot ci
2025-09-11 21:09   ` Eduard Zingerman
2025-09-11 21:58     ` Alexei Starovoitov
2025-09-11 22:06       ` Eduard Zingerman
2025-09-11 22:11         ` Alexei Starovoitov

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox