[PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Nandakumar Edamana]

This commit addresses a challenge explained in an open question ("How
can we incorporate correlation in unknown bits across partial
products?") left by Harishankar et al. in their paper:
https://arxiv.org/abs/2105.05398

When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
from which we could find two possible partial products and take a
union. Experiment shows that applying this technique in long
multiplication improves the precision in a significant number of cases
(at the cost of losing precision in a relatively lower number of
cases).

This commit also removes the value-mask decomposition technique
employed by Harishankar et al., as its direct incorporation did not
result in any improvements for the new algorithm.

Signed-off-by: Nandakumar Edamana <nandakumar@nandakumar.co.in>
---
 include/linux/tnum.h |  3 +++
 kernel/bpf/tnum.c    | 55 +++++++++++++++++++++++++++++++++-----------
 2 files changed, 45 insertions(+), 13 deletions(-)

diff --git a/include/linux/tnum.h b/include/linux/tnum.h
index 57ed3035cc30..68e9cdd0a2ab 100644
--- a/include/linux/tnum.h
+++ b/include/linux/tnum.h
@@ -54,6 +54,9 @@ struct tnum tnum_mul(struct tnum a, struct tnum b);
 /* Return a tnum representing numbers satisfying both @a and @b */
 struct tnum tnum_intersect(struct tnum a, struct tnum b);
 
+/* Returns a tnum representing numbers satisfying either @a or @b */
+struct tnum tnum_union(struct tnum t1, struct tnum t2);
+
 /* Return @a with all but the lowest @size bytes cleared */
 struct tnum tnum_cast(struct tnum a, u8 size);
 
diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index fa353c5d550f..c98aa148e666 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -116,31 +116,47 @@ struct tnum tnum_xor(struct tnum a, struct tnum b)
 	return TNUM(v & ~mu, mu);
 }
 
-/* Generate partial products by multiplying each bit in the multiplier (tnum a)
- * with the multiplicand (tnum b), and add the partial products after
- * appropriately bit-shifting them. Instead of directly performing tnum addition
- * on the generated partial products, equivalenty, decompose each partial
- * product into two tnums, consisting of the value-sum (acc_v) and the
- * mask-sum (acc_m) and then perform tnum addition on them. The following paper
- * explains the algorithm in more detail: https://arxiv.org/abs/2105.05398.
+/* Perform long multiplication, iterating through the trits in a:
+ * - if LSB(a) is a known 0, keep current accumulator
+ * - if LSB(a) is a known 1, add b to current accumulator
+ * - if LSB(a) is unknown, take a union of the above cases.
+ *
+ * For example:
+ *
+ *               acc_0:        acc_1:
+ *
+ *     11 *  ->      11 *  ->      11 *  -> union(0011, 1001) == x0x1
+ *     x1            01            11
+ * ------        ------        ------
+ *     11            11            11
+ *    xx            00            11
+ * ------        ------        ------
+ *   ????          0011          1001
  */
 struct tnum tnum_mul(struct tnum a, struct tnum b)
 {
-	u64 acc_v = a.value * b.value;
-	struct tnum acc_m = TNUM(0, 0);
+	struct tnum acc = TNUM(0, 0);
 
 	while (a.value || a.mask) {
 		/* LSB of tnum a is a certain 1 */
 		if (a.value & 1)
-			acc_m = tnum_add(acc_m, TNUM(0, b.mask));
+			acc = tnum_add(acc, b);
 		/* LSB of tnum a is uncertain */
-		else if (a.mask & 1)
-			acc_m = tnum_add(acc_m, TNUM(0, b.value | b.mask));
+		else if (a.mask & 1) {
+			/* acc = tnum_union(acc_0, acc_1), where acc_0 and
+			 * acc_1 are partial accumulators for cases
+			 * LSB(a) = certain 0 and LSB(a) = certain 1.
+			 * acc_0 = acc + 0 * b = acc.
+			 * acc_1 = acc + 1 * b = tnum_add(acc, b).
+			 */
+
+			acc = tnum_union(acc, tnum_add(acc, b));
+		}
 		/* Note: no case for LSB is certain 0 */
 		a = tnum_rshift(a, 1);
 		b = tnum_lshift(b, 1);
 	}
-	return tnum_add(TNUM(acc_v, 0), acc_m);
+	return acc;
 }
 
 /* Note that if a and b disagree - i.e. one has a 'known 1' where the other has
@@ -155,6 +171,19 @@ struct tnum tnum_intersect(struct tnum a, struct tnum b)
 	return TNUM(v & ~mu, mu);
 }
 
+/* Returns a tnum with the uncertainty from both a and b, and in addition, new
+ * uncertainty at any position that a and b disagree. This represents a
+ * superset of the union of the concrete sets of both a and b. Despite the
+ * overapproximation, it is optimal.
+ */
+struct tnum tnum_union(struct tnum a, struct tnum b)
+{
+	u64 v = a.value & b.value;
+	u64 mu = (a.value ^ b.value) | a.mask | b.mask;
+
+	return TNUM(v & ~mu, mu);
+}
+
 struct tnum tnum_cast(struct tnum a, u8 size)
 {
 	a.value &= (1ULL << (size * 8)) - 1;
-- 
2.39.5

[PATCH v5 bpf-next 2/2] bpf: add selftest to check the verifier's abstract multiplication

[Nandakumar Edamana]

This commit adds selftest to test the abstract multiplication
technique(s) used by the verifier, following the recent improvement in
tnum multiplication (tnum_mul). One of the newly added programs,
verifier_mul/mul_precise, results in a false positive with the old
tnum_mul, while the program passes with the latest one.

Signed-off-by: Nandakumar Edamana <nandakumar@nandakumar.co.in>
---
 .../selftests/bpf/prog_tests/verifier.c       |  2 +
 .../selftests/bpf/progs/verifier_mul.c        | 38 +++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 tools/testing/selftests/bpf/progs/verifier_mul.c

diff --git a/tools/testing/selftests/bpf/prog_tests/verifier.c b/tools/testing/selftests/bpf/prog_tests/verifier.c
index 77ec95d4ffaa..e35c216dbaf2 100644
--- a/tools/testing/selftests/bpf/prog_tests/verifier.c
+++ b/tools/testing/selftests/bpf/prog_tests/verifier.c
@@ -59,6 +59,7 @@
 #include "verifier_meta_access.skel.h"
 #include "verifier_movsx.skel.h"
 #include "verifier_mtu.skel.h"
+#include "verifier_mul.skel.h"
 #include "verifier_netfilter_ctx.skel.h"
 #include "verifier_netfilter_retcode.skel.h"
 #include "verifier_bpf_fastcall.skel.h"
@@ -194,6 +195,7 @@ void test_verifier_may_goto_1(void)           { RUN(verifier_may_goto_1); }
 void test_verifier_may_goto_2(void)           { RUN(verifier_may_goto_2); }
 void test_verifier_meta_access(void)          { RUN(verifier_meta_access); }
 void test_verifier_movsx(void)                 { RUN(verifier_movsx); }
+void test_verifier_mul(void)                  { RUN(verifier_mul); }
 void test_verifier_netfilter_ctx(void)        { RUN(verifier_netfilter_ctx); }
 void test_verifier_netfilter_retcode(void)    { RUN(verifier_netfilter_retcode); }
 void test_verifier_bpf_fastcall(void)         { RUN(verifier_bpf_fastcall); }
diff --git a/tools/testing/selftests/bpf/progs/verifier_mul.c b/tools/testing/selftests/bpf/progs/verifier_mul.c
new file mode 100644
index 000000000000..7145fe3351d5
--- /dev/null
+++ b/tools/testing/selftests/bpf/progs/verifier_mul.c
@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-2.0
+/* Copyright (c) 2025 Nandakumar Edamana */
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+#include <bpf/bpf_tracing.h>
+#include "bpf_misc.h"
+
+/* Intended to test the abstract multiplication technique(s) used by
+ * the verifier. Using assembly to avoid compiler optimizations.
+ */
+SEC("fentry/bpf_fentry_test1")
+void BPF_PROG(mul_precise, int x)
+{
+	/* First, force the verifier to be uncertain about the value:
+	 *     unsigned int a = (bpf_get_prandom_u32() & 0x2) | 0x1;
+	 *
+	 * Assuming the verifier is using tnum, a must be tnum{.v=0x1, .m=0x2}.
+	 * Then a * 0x3 would be m0m1 (m for uncertain). Added imprecision
+	 * would cause the following to fail, because the required return value
+	 * is 0:
+	 *     return (a * 0x3) & 0x4);
+	 */
+	asm volatile ("\
+	call %[bpf_get_prandom_u32];\
+	r0 &= 0x2;\
+	r0 |= 0x1;\
+	r0 *= 0x3;\
+	r0 &= 0x4;\
+	if r0 != 0 goto l0_%=;\
+	r0 = 0;\
+	goto l1_%=;\
+l0_%=:\
+	r0 = 1;\
+l1_%=:\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
-- 
2.39.5

Re: [PATCH v5 bpf-next 2/2] bpf: add selftest to check the verifier's abstract multiplication

[Eduard Zingerman]

On Mon, 2025-08-25 at 22:59 +0530, Nandakumar Edamana wrote:
> This commit adds selftest to test the abstract multiplication
> technique(s) used by the verifier, following the recent improvement in
> tnum multiplication (tnum_mul). One of the newly added programs,
> verifier_mul/mul_precise, results in a false positive with the old
> tnum_mul, while the program passes with the latest one.
> 
> Signed-off-by: Nandakumar Edamana <nandakumar@nandakumar.co.in>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Eduard Zingerman]

On Mon, 2025-08-25 at 22:59 +0530, Nandakumar Edamana wrote:
> This commit addresses a challenge explained in an open question ("How
> can we incorporate correlation in unknown bits across partial
> products?") left by Harishankar et al. in their paper:
> https://arxiv.org/abs/2105.05398
> 
> When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
> from which we could find two possible partial products and take a
> union. Experiment shows that applying this technique in long
> multiplication improves the precision in a significant number of cases
> (at the cost of losing precision in a relatively lower number of
> cases).
> 
> This commit also removes the value-mask decomposition technique
> employed by Harishankar et al., as its direct incorporation did not
> result in any improvements for the new algorithm.
> 
> Signed-off-by: Nandakumar Edamana <nandakumar@nandakumar.co.in>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Harishankar Vishwanathan]

On Mon, Aug 25, 2025 at 1:30 PM Nandakumar Edamana
<nandakumar@nandakumar.co.in> wrote:
>
> This commit addresses a challenge explained in an open question ("How
> can we incorporate correlation in unknown bits across partial
> products?") left by Harishankar et al. in their paper:
> https://arxiv.org/abs/2105.05398
>
> When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
> from which we could find two possible partial products and take a
> union. Experiment shows that applying this technique in long
> multiplication improves the precision in a significant number of cases
> (at the cost of losing precision in a relatively lower number of
> cases).
>
> This commit also removes the value-mask decomposition technique
> employed by Harishankar et al., as its direct incorporation did not
> result in any improvements for the new algorithm.
>
> Signed-off-by: Nandakumar Edamana <nandakumar@nandakumar.co.in>
> ---

Reviewed-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>

[...]

Re: [PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Alexei Starovoitov]

On Mon, Aug 25, 2025 at 10:30 AM Nandakumar Edamana
<nandakumar@nandakumar.co.in> wrote:
>
> This commit addresses a challenge explained in an open question ("How
> can we incorporate correlation in unknown bits across partial
> products?") left by Harishankar et al. in their paper:
> https://arxiv.org/abs/2105.05398

Either drop this paragraph or add the details inline.

> When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
> from which we could find two possible partial products and take a
> union. Experiment shows that applying this technique in long
> multiplication improves the precision in a significant number of cases
> (at the cost of losing precision in a relatively lower number of
> cases).
>
> This commit also removes the value-mask decomposition technique
> employed by Harishankar et al., as its direct incorporation did not
> result in any improvements for the new algorithm.

Please rewrite commit using imperative language.
Like what you use in the comment:

> +/* Perform long multiplication, iterating through the trits in a:

"trit" is not used anywhere in the code.
Use "ternary digit" instead.

Keep acks when respining.

pw-bot: cr

Re: [PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Nandakumar Edamana]

On 26/08/25 06:19, Alexei Starovoitov wrote:
> On Mon, Aug 25, 2025 at 10:30 AM Nandakumar Edamana
> <nandakumar@nandakumar.co.in> wrote:
>> This commit addresses a challenge explained in an open question ("How
>> can we incorporate correlation in unknown bits across partial
>> products?") left by Harishankar et al. in their paper:
>> https://arxiv.org/abs/2105.05398
> Either drop this paragraph or add the details inline.

Okay, I'll drop it from the commit message and add it to the code like 
this, since it's useful information:

diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index c98aa148e666..4c82f3ede74e 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -116,7 +116,7 @@ struct tnum tnum_xor(struct tnum a, struct tnum b)
         return TNUM(v & ~mu, mu);
  }

-/* Perform long multiplication, iterating through the trits in a:
+/* Perform long multiplication, iterating through the bits in a using 
rshift:
   * - if LSB(a) is a known 0, keep current accumulator
   * - if LSB(a) is a known 1, add b to current accumulator
   * - if LSB(a) is unknown, take a union of the above cases.
@@ -132,6 +132,11 @@ struct tnum tnum_xor(struct tnum a, struct tnum b)
   *    xx            00            11
   * ------        ------        ------
   *   ????          0011          1001
+ *
+ * Considering cases LSB(a) = known 0 and LSB(a) = known 1 separately and
+ * taking a union addresses a challenge explained in an open question ("How
+ * can we incorporate correlation in unknown bits across partial 
products?")
+ * left by Harishankar et al. in their paper: 
https://arxiv.org/abs/2105.05398
   */
  struct tnum tnum_mul(struct tnum a, struct tnum b)
  {

>> When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
>> from which we could find two possible partial products and take a
>> union. Experiment shows that applying this technique in long
>> multiplication improves the precision in a significant number of cases
>> (at the cost of losing precision in a relatively lower number of
>> cases).
>>
>> This commit also removes the value-mask decomposition technique
>> employed by Harishankar et al., as its direct incorporation did not
>> result in any improvements for the new algorithm.
> Please rewrite commit using imperative language.

This will be my new message:

   bpf: Improve the general precision of tnum_mul

   Drop the value-mask decomposition technique and adopt straightforward
   long-multiplication with a twist: when LSB(a) is uncertain, find the
   two partial products (for LSB(a) = known 0 and LSB(a) = known 1) and
   take a union.

   Experiment shows that applying this technique in long multiplication
   improves the precision in a significant number of cases (at the cost
   of losing precision in a relatively lower number of cases).

Using uppercase for the character after "bpf: " this time, just to be 
consistent with other commits.

Similar changes for PATCH 2/2.

> "trit" is not used anywhere in the code.
> Use "ternary digit" instead.

Changing it to "bits" since other comments in the file already use it to 
mean trit (also, "digit" could be confused for a decimal thing). With 
another clarification, "iterating through the trits in a" now becomes 
"iterating through the bits in a using rshift". Hope it's okay.

I'll send v6 after waiting for a while for further feedback, if any.

> Keep acks when respining.
Sorry, I didn't get this. Is this something I need to do?

-- 
Nandakumar

Re: [PATCH v5 bpf-next 1/2] bpf: improve the general precision of tnum_mul

[Alexei Starovoitov]

On Mon, Aug 25, 2025 at 7:05 PM Nandakumar Edamana
<nandakumar@nandakumar.co.in> wrote:
>
> On 26/08/25 06:19, Alexei Starovoitov wrote:
> > On Mon, Aug 25, 2025 at 10:30 AM Nandakumar Edamana
> > <nandakumar@nandakumar.co.in> wrote:
> >> This commit addresses a challenge explained in an open question ("How
> >> can we incorporate correlation in unknown bits across partial
> >> products?") left by Harishankar et al. in their paper:
> >> https://arxiv.org/abs/2105.05398
> > Either drop this paragraph or add the details inline.
>
> Okay, I'll drop it from the commit message and add it to the code like
> this, since it's useful information:
>
> diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
> index c98aa148e666..4c82f3ede74e 100644
> --- a/kernel/bpf/tnum.c
> +++ b/kernel/bpf/tnum.c
> @@ -116,7 +116,7 @@ struct tnum tnum_xor(struct tnum a, struct tnum b)
>          return TNUM(v & ~mu, mu);
>   }
>
> -/* Perform long multiplication, iterating through the trits in a:
> +/* Perform long multiplication, iterating through the bits in a using
> rshift:
>    * - if LSB(a) is a known 0, keep current accumulator
>    * - if LSB(a) is a known 1, add b to current accumulator
>    * - if LSB(a) is unknown, take a union of the above cases.
> @@ -132,6 +132,11 @@ struct tnum tnum_xor(struct tnum a, struct tnum b)
>    *    xx            00            11
>    * ------        ------        ------
>    *   ????          0011          1001
> + *
> + * Considering cases LSB(a) = known 0 and LSB(a) = known 1 separately and
> + * taking a union addresses a challenge explained in an open question ("How
> + * can we incorporate correlation in unknown bits across partial
> products?")
> + * left by Harishankar et al. in their paper:

No. This indirection is not helpful.
People should not be forced to click on some link and read the paper.
Just drop it.

> https://arxiv.org/abs/2105.05398
>    */
>   struct tnum tnum_mul(struct tnum a, struct tnum b)
>   {
>
> >> When LSB(a) is uncertain, we know for sure that it is either 0 or 1,
> >> from which we could find two possible partial products and take a
> >> union. Experiment shows that applying this technique in long
> >> multiplication improves the precision in a significant number of cases
> >> (at the cost of losing precision in a relatively lower number of
> >> cases).
> >>
> >> This commit also removes the value-mask decomposition technique
> >> employed by Harishankar et al., as its direct incorporation did not
> >> result in any improvements for the new algorithm.
> > Please rewrite commit using imperative language.
>
> This will be my new message:
>
>    bpf: Improve the general precision of tnum_mul
>
>    Drop the value-mask decomposition technique and adopt straightforward
>    long-multiplication with a twist: when LSB(a) is uncertain, find the
>    two partial products (for LSB(a) = known 0 and LSB(a) = known 1) and
>    take a union.
>
>    Experiment shows that applying this technique in long multiplication
>    improves the precision in a significant number of cases (at the cost
>    of losing precision in a relatively lower number of cases).

+1

> Using uppercase for the character after "bpf: " this time, just to be
> consistent with other commits.

+1

> Similar changes for PATCH 2/2.
>
> > "trit" is not used anywhere in the code.
> > Use "ternary digit" instead.
>
> Changing it to "bits" since other comments in the file already use it to
> mean trit (also, "digit" could be confused for a decimal thing). With
> another clarification, "iterating through the trits in a" now becomes
> "iterating through the bits in a using rshift". Hope it's okay.

Sounds good.

> I'll send v6 after waiting for a while for further feedback, if any.

Just respin it. The code itself looks good.

> > Keep acks when respining.
> Sorry, I didn't get this. Is this something I need to do?

When you respin apply the acks/review-by tags you received already.