Synthesizing state machines for data planes

Abstract

The emergence of programmable switches such as the Intel Tofino has made it possible, in theory, to implement many network monitoring applications directly in the network data plane. In practice, however, such implementations are often more challenging than expected. A key difficulty is that such applications often depend, in part, on recognizing traffic patterns that are easy to specify as a deterministic finite state automaton (a DFA) but hard to implement thanks to stringent hardware constraints: to maximize throughput and avoid race conditions, state machine updates must be completed in a single Tofino pipeline stage, but the limited computational resources make finding an implementation a challenging puzzle. This paper presents a solution to such puzzles - -a general framework for synthesizing DFA implementations automatically. A key insight is that such a synthesis system is free to renumber state machine states and implement transitions using any available arithmetic or logical operations over that renumbering, provided the resulting implementation is semantically equivalent to the input specification. To produce such a synthesizer, we model the required state machine semantics and the available single-stage switch operations using SMT constraints. An off-the-shelf SMT solver finds a solution to the constraints, and this solution is then translated to P4 code. We evaluate the effectiveness of our methods by synthesizing state machines for a variety of useful applications, including those that monitor TCP handshakes and video conference streams.