TY - GEN

T1 - Synthesizing state machines for data planes

AU - Chen, Xiaoqi

AU - Johnson, Andrew

AU - Pan, Mengying

AU - Walker, David

N1 - Publisher Copyright:
© 2022 ACM.

PY - 2022/10/19

Y1 - 2022/10/19

N2 - 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.

AB - 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.

KW - DFA

KW - P4

KW - SMT

KW - programmable data plane

KW - state machine

UR - http://www.scopus.com/inward/record.url?scp=85141094359&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85141094359&partnerID=8YFLogxK

U2 - 10.1145/3563647.3563650

DO - 10.1145/3563647.3563650

M3 - Conference contribution

AN - SCOPUS:85141094359

T3 - SOSR 2022 - Proceedings of the 2022 Symposium on SDN Research

SP - 81

EP - 88

BT - SOSR 2022 - Proceedings of the 2022 Symposium on SDN Research

PB - Association for Computing Machinery, Inc

T2 - 2002 ACM SIGCOMM Symposium on SDN Research, SOSR 2022

Y2 - 20 October 2022

ER -