On Tue, Dec 5, 2023 at 10:43 AM Andrii Nakryiko <andrii@xxxxxxxxxx> wrote:
>
> Instead of allocating and copying instruction history each time we
> enqueue child verifier state, switch to a model where we use one common
> dynamically sized array of instruction history entries across all states.
>
> The key observation for proving this is correct is that instruction
> history is only relevant while state is active, which means it either is
> a current state (and thus we are actively modifying instruction history
> and no other state can interfere with us) or we are checkpointed state
> with some children still active (either enqueued or being current).
>
> In the latter case our portion of instruction history is finalized and
> won't change or grow, so as long as we keep it immutable until the state
> is finalized, we are good.
>
> Now, when state is finalized and is put into state hash for potentially
> future pruning lookups, instruction history is not used anymore. This is
> because instruction history is only used by precision marking logic, and
> we never modify precision markings for finalized states.
>
> So, instead of each state having its own small instruction history, we
> keep a global dynamically-sized instruction history, where each state in
> current DFS path from root to active state remembers its portion of
> instruction history. Current state can append to this history, but
> cannot modify any of its parent histories.
>
> Because the insn_hist array can be grown through realloc, states don't
> keep pointers, they instead maintain two indices, [start, end), into
> global instruction history array. End is exclusive index, so
> `start == end` means there is no relevant instruction history.
>
> This eliminates a lot of allocations and minimizes overall memory usage.
I still think it's too dangerous to rely on DFS here.
The algo would certainly save allocs, but to save memory we can simply do:
@@ -16128,6 +16128,7 @@ static void clean_verifier_state(struct
bpf_verifier_env *env,
/* all regs in this state in all frames were already marked */
return;
+ clear_jmp_history(st);
for (i = 0; i <= st->curframe; i++)
clean_func_state(env, st->frame[i]);
}
to achieve the same effect (it seems to work fine in tests).
I'm not sure how much memory it actually saves
(both above hack and this algo).
We probably need to augment veristat with cgroup memory.peak numbers
the way benchs/bench_htab_mem.c does.
This will give us a clear signal whether we're saving any memory or not.
Reusing the jmp history array this way also has a negative effect on kasan.
When arrays are separate any UAF or out-of-bounds are easier to catch.
So I pushed the first 9 patches to bpf-next.
