Multiple systems have explored how to use programmable switch ASICs to improve the performance of distributed systems. However, they focus on accelerating read operations and perform poorly under write-intensive workloads. In this paper, we present Gecko, a system that accelerates write operations in distributed key-value store systems using switch ASICs. The core idea of Gecko is to offload the client-side chasing mechanism, a technique deployed by production storage networks, to the programmable switch to simultaneously reduce the perceived and actual write-tail latency in distributed key-value stores. The perceived latency is the interval between the user sending a write request and the user receiving the write success, and there may be replicas that have not yet completed the write, but the actual latency requires all replicas to be successfully written. Gecko not only reduces the perceived write tail latency by deploying the chasing mechanism, but the actual write tail latency is also reduced by utilizing the capabilities of programmable switches. Specifically, Gecko’s in-network chasing design caches a write request at the switch data plane and reports success to the client when only m out of n (usually set to 2 and 3 in production networks, respectively) replicas have been successfully written to the server, and retries the cached write request if the remaining n − m replicas are not successfully written. In addition to caching the write request, Gecko also introduces novel designs to fully implement the chasing controller and a corresponding timer controller in the switch data plane, minimizing the interaction overhead between the switch control and data plane. Extensive experiments on a testbed of Barefoot Tofino switch and commodity servers show that Gecko not only substantially reduces the write tail latency by more than 2.16x caused by transient glitches at servers, but also maintains the same level of reliability as the classic three-replica write operation in distributed key-value stores.

People have been leveraging the capabilities of programmable switches, which are programmable in the data plane and process packets at the line rate, to improve the performance of distributed systems. However, few have explored whether programmable switches can speed up problem-solving. In this paper, we select the SAT problem, one of the most fundamental problems in computer science, as a case study to first explore the feasibility and benefits of this line of research. Our intuition is that by exploiting the parallel lookup capability of programmable switches, we can substantially speed up the process of checking whether an assignment is a solution to a SAT problem. Consequently, we design conflict tables using TCAM to quickly check assignment satisfiability. Building on the conflict tables, we propose two SAT solvers, P4-DPLL and Antler. Specifically, P4-DPLL is based on the classical DPLL algorithm and implements a stack data structure using registers and SRAM to efficiently make variable search decisions in the data plane, while Antler utilizes the mirroring capability of the programmable switch to further accelerate the SAT solving, which improves the non-parallel depth-first search-based P4-DPLL into a parallel breadth-first search-based SAT solver. We implement the prototypes of P4-DPLL and Antler on the Tofino switch, and evaluate their performance extensively. Results show that P4-DPLL and Antler improve the solving time by 2x and 169x on 90% quantile of test cases, compared to a CPU-based DPLL implementation. Besides, compared with the most popular SAT solvers, MathSAT and Z3, Antler improves the solving time by 42x and 35x, respectively.

Centralized data plane verification (DPV) faces significant scalability issues in large networks (i.e., the verifier being a performance bottleneck and single point of failure and requiring a reliable management network). We tackle this scalability challenge by introducing Tulkun, a distributed, on-device DPV framework. Our key insight is that DPV can be transformed into a counting problem on a directed acyclic graph, which can be naturally decomposed into lightweight tasks executed at network devices, enabling fast data plane checking in networks of various scales and types. With this insight, Tulkun consists of (1) a declarative invariant specification language, (2) a planner that employs a novel data structure DPVNet to systematically decompose global verification into on-device counting tasks, (3) a distributed verification messaging (DVM) protocol that specifies how on-device verifiers efficiently communicate task results to jointly verify the invariants, and (4) a mechanism to verify invariant fault-tolerance with minimal involvement of the planner. Extensive experiments with real-world datasets (WAN/LAN/DC) show that Tulkun verifies a real, large DC in 41 seconds while others tools need minutes or up to tens of hours, and shows an up to 2355× speed up on 80% quantile of incremental verification with small overhead on commodity network devices.