On Mon, 2023-11-20 at 16:22 -0800, Andrii Nakryiko 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. > > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx> > --- Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> [...]
