From f379a2645c585ba0dc191514f159d722c475aebc Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Wed, 10 Jun 2026 04:00:55 -0700 Subject: [PATCH] [NetKAT] Add scale benchmark with realistically large inputs. The existing benchmarks compile small fixed policies, so they mostly measure constant overheads and cannot detect asymptotic problems (or improvements) in the backend. This benchmark compiles inputs modeled on real networking workloads - wide forwarding tables, multi-field ACLs, and ring-network reachability via Iterate - parameterized by size, so scaling behavior is visible directly in the output. It immediately demonstrates its value: forwarding table compilation scales super-quadratically at head (8x entries -> 66-100x time; 4096 entries take 3.5 seconds), quantifying the known lack of operation memoization (b/382379263) and giving future optimizations a measurable target. Co-Authored-By: Claude Fable 5 --- netkat/BUILD.bazel | 13 +++ netkat/scale_benchmark.cc | 191 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 204 insertions(+) create mode 100644 netkat/scale_benchmark.cc diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel index 9121fef..9534d7f 100644 --- a/netkat/BUILD.bazel +++ b/netkat/BUILD.bazel @@ -433,6 +433,19 @@ cc_binary( ], ) +cc_binary( + name = "scale_benchmark", + testonly = True, + srcs = ["scale_benchmark.cc"], + deps = [ + ":frontend", + ":netkat_cc_proto", + ":packet_set", + ":packet_transformer", + "@com_google_benchmark//:benchmark_main", + ], +) + # go/golden-test-with-coverage cc_test( name = "packet_transformer_test_runner", diff --git a/netkat/scale_benchmark.cc b/netkat/scale_benchmark.cc new file mode 100644 index 0000000..1c82799 --- /dev/null +++ b/netkat/scale_benchmark.cc @@ -0,0 +1,191 @@ +// Copyright 2026 The NetKAT authors +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +// ----------------------------------------------------------------------------- +// File: scale_benchmark.cc +// ----------------------------------------------------------------------------- +// +// Benchmarks the NetKAT backend on realistically *large* inputs, complementing +// the micro-benchmarks in `packet_set_benchmark.cc` and +// `packet_transformer_benchmark.cc` (which compile small, fixed policies and +// thus mostly measure constant overheads). +// +// The benchmarks are parameterized by input size, so their output also shows +// how the backend *scales*: compare the per-size timings to see whether an +// operation behaves linearly, quadratically, or worse in practice. +// +// Three families of inputs are modeled on common networking workloads: +// * Forwarding tables: many rules matching a single field (wide decision +// nodes with one branch per value). +// * ACLs: rules matching several fields each (deeper decision graphs over +// multiple fields). +// * Network reachability: a ring of switches with per-switch forwarding +// tables, composed with `Iterate` to a fixed point - the workload at the +// heart of symbolic network verification. + +#include +#include +#include + +#include "benchmark/benchmark.h" +#include "netkat/frontend.h" +#include "netkat/netkat.pb.h" +#include "netkat/packet_set.h" +#include "netkat/packet_transformer.h" + +namespace netkat { +namespace { + +// Deterministically scrambles `i` into a value in [0, 2^16), so that matched +// values are spread out rather than consecutive. (Knuth's multiplicative +// hash; any fixed bijective-ish scramble would do.) +int ScrambledValue(uint32_t i) { + return static_cast((i * 2654435761u) >> 16) % (1 << 16); +} + +// -- Forwarding tables -------------------------------------------------------- + +// A forwarding table with `num_entries` exact-match rules on dst_ip, each +// forwarding to one of `num_ports` ports. +Policy ForwardingTable(int num_entries, int num_ports = 32) { + std::vector rules; + rules.reserve(num_entries); + for (int i = 0; i < num_entries; ++i) { + rules.push_back(Sequence(Filter(Match("dst_ip", ScrambledValue(i))), + Modify("out_port", i % num_ports))); + } + return Union(std::move(rules)); +} + +void BM_CompileForwardingTable(benchmark::State& state) { + const int num_entries = state.range(0); + PolicyProto policy = ForwardingTable(num_entries).ToProto(); + for (auto s : state) { + PacketTransformerManager manager; + benchmark::DoNotOptimize(manager.Compile(policy)); + } + state.SetItemsProcessed(state.iterations() * num_entries); +} +BENCHMARK(BM_CompileForwardingTable)->Arg(64)->Arg(512)->Arg(4096); + +// -- ACLs ---------------------------------------------------------------------- + +// An ACL with `num_rules` rules, each a conjunction over 4 of 5 header fields +// with scrambled values. Models a multi-field classifier; unlike forwarding +// tables, the compiled decision graph branches on several fields per path. +Predicate AclRule(int rule) { + return Match("src_ip", ScrambledValue(2 * rule)) && + Match("dst_ip", ScrambledValue(2 * rule + 1)) && + Match("ip_proto", rule % 3) && + Match(rule % 2 == 0 ? "dst_port" : "src_port", rule % 1024); +} + +Predicate Acl(int num_rules) { + Predicate acl = Predicate::False(); + for (int i = 0; i < num_rules; ++i) { + acl = std::move(acl) || AclRule(i); + } + return acl; +} + +void BM_CompileAclAsPacketSet(benchmark::State& state) { + const int num_rules = state.range(0); + PredicateProto acl = Acl(num_rules).ToProto(); + for (auto s : state) { + PacketSetManager manager; + benchmark::DoNotOptimize(manager.Compile(acl)); + } + state.SetItemsProcessed(state.iterations() * num_rules); +} +BENCHMARK(BM_CompileAclAsPacketSet)->Arg(16)->Arg(64)->Arg(256); + +// Compiling `permitted && !denied` exercises Not/And on large packet sets. +void BM_CompileAclDifference(benchmark::State& state) { + const int num_rules = state.range(0); + // Two ACLs with 50% overlap. + Predicate permitted = Acl(num_rules); + Predicate denied = Predicate::False(); + for (int i = num_rules / 2; i < num_rules + num_rules / 2; ++i) { + denied = std::move(denied) || AclRule(i); + } + PredicateProto policy = (std::move(permitted) && !std::move(denied)).ToProto(); + for (auto s : state) { + PacketSetManager manager; + benchmark::DoNotOptimize(manager.Compile(policy)); + } + state.SetItemsProcessed(state.iterations() * num_rules); +} +BENCHMARK(BM_CompileAclDifference)->Arg(16)->Arg(64)->Arg(256); + +// -- Network reachability ------------------------------------------------------- + +// A ring network of `num_switches` switches. Each switch delivers packets +// addressed to it and forwards all other (known) packets clockwise to its +// neighbor. One "step" of the network is the union of all per-switch tables. +Policy RingNetworkStep(int num_switches) { + std::vector switch_policies; + switch_policies.reserve(num_switches); + for (int sw = 0; sw < num_switches; ++sw) { + std::vector rules; + rules.reserve(num_switches); + for (int dst = 0; dst < num_switches; ++dst) { + if (dst == sw) { + // Deliver locally. + rules.push_back( + Sequence(Filter(Match("dst_sw", dst)), Modify("delivered", 1))); + } else { + // Forward clockwise. + rules.push_back(Sequence(Filter(Match("dst_sw", dst)), + Modify("sw", (sw + 1) % num_switches))); + } + } + switch_policies.push_back(Sequence( + Filter(Match("sw", sw) && Match("delivered", 0)), + Union(std::move(rules)))); + } + return Union(std::move(switch_policies)); +} + +// Compiles the reachability transformer of the ring network: all forwarding +// paths of any length, via Iterate. The ring has diameter num_switches - 1, +// so the fixed-point computation must traverse the entire ring. +void BM_CompileRingReachability(benchmark::State& state) { + const int num_switches = state.range(0); + PolicyProto reachability = + Iterate(RingNetworkStep(num_switches)).ToProto(); + for (auto s : state) { + PacketTransformerManager manager; + benchmark::DoNotOptimize(manager.Compile(reachability)); + } + state.SetItemsProcessed(state.iterations() * num_switches); +} +BENCHMARK(BM_CompileRingReachability)->Arg(2)->Arg(4)->Arg(8)->Arg(16)->Arg(32); + +// Full end-to-end verification question: "which packets can every switch +// deliver?" Computes the output packet set of the reachability transformer. +void BM_RingReachableOutputs(benchmark::State& state) { + const int num_switches = state.range(0); + PolicyProto reachability = + Iterate(RingNetworkStep(num_switches)).ToProto(); + for (auto s : state) { + PacketTransformerManager manager; + PacketTransformerHandle transformer = manager.Compile(reachability); + benchmark::DoNotOptimize(manager.GetAllPossibleOutputPackets(transformer)); + } + state.SetItemsProcessed(state.iterations() * num_switches); +} +BENCHMARK(BM_RingReachableOutputs)->Arg(2)->Arg(4)->Arg(8)->Arg(16)->Arg(32); + +} // namespace +} // namespace netkat