On Tue, Nov 7, 2023 at 9:46 PM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote: > > This patchset is a proof of concept for previously discussed concept[1] > of unifying smin/smax with umin/uax for both the 32-bit and 64-bit > range[2] within bpf_reg_state. This will allow the verifier to track > both signed and unsiged ranges using just two u32 (for 32-bit range) or > u64 (for 64-bit range), instead four as we currently do. > > The size reduction we gain from this probably isn't very significant. > The main benefit is in lowering of code _complexity_. The verifier > currently employs 5 value tracking mechanisms, two for 64-bit range, two > for 32-bit range, and one tnum that tracks individual bits. Exchanging > knowledge between all the bound tracking mechanisms requires a > (theoretical) 20-way synchronization[3]; with signed and unsigned > unification the verifier will only need 3 value tracking mechanism, > cutting this down to a 6-way synchronization. > > The unification is possible from a theoretical standpoint[4] and there > exists implementation[5]. The challenge lies in implementing it inside > the verifier and making sure it fits well with all the logic we have in > place. > > To lower the difficulty, the unified min/max tracking is implemented in > isolation, and have it correctness checked using model checking. The > model checking code can be found in this patchset as well, but is not > meant to be merged since a better method already exists[6]. > > So far I've managed to implement add/sub/mul operations for unified > min/max tracking, the next steps are: > - implement operation that can be used gain knowledge from conditional > jump, e.g wrange32_intersect, wrange32_diff > - implement wrange32_from_min_max and wrange32_to_min_max so we can > check whether this PoC works using current selftests > - implement operations for wrange64, the 64-bit counterpart of wrange32 > - come up with how to exchange knowledge between wrange64 and wrange32 > (this is likely the most difficult part) > - think about how to integrate this work in a manageable manner Thanks for taking a stab at it. The biggest question is how to integrate it without breaking anything. I suspect you might need to implement all alu and branch logic just to be able to run the tests. It's difficult to see a path for partial/incremental addition. The concern is that at the end this approach might hit an issue which will make it infeasible. So it's a big bet. Might be nice correctness and memory saving or nothing. Certainly exciting, but proceed with caution.
