Show simple item record

dc.contributor.authorLong, Xiang
dc.date.accessioned2021-09-09T17:40:53Z
dc.date.available2021-09-09T17:40:53Z
dc.date.issued2021-05
dc.identifier.otherLong_cornellgrad_0058F_12482
dc.identifier.otherhttp://dissertations.umi.com/cornellgrad:12482
dc.identifier.urihttps://hdl.handle.net/1813/109772
dc.description166 pages
dc.description.abstractThe match-action paradigm has remained a popular low-level programming model for specifying packet forwarding behavior in network switches. There are efficient hardware implementations of match-action, and it is a simple model accepted by network programmers. Nevertheless, high-level domain specific languages (DSLs) such as NetKAT and P4 are available to provide abstractions for network policies that can then be compiled down to match-action tables in the target switch. Despite much theoretical work surrounding these DSLs, there has been comparatively little investigation towards putting match-action itself on a firm theoretical foundation. The aim of this dissertation is to understand existing practice surrounding match-action using theory. In the first part of our work, considering how match tables are implemented currently, we attempt to formally model their computational power. We argue that even the apparently low-level primitives of match-action: building blocks such as tables, rules, match patterns, etc., are open to formalization. We take both complexity-theoretic and language-theoretic approaches. On the one hand, we give a circuit complexity model for match-action, and we relate the complexity class AC0 to match tables of various sizes. Further, we give a multimatch extension to traditional match-action, and discover the complexity class that characterizes its expressivity. On the other hand, we describe an algebraic language for match-action called MatchKAT. Although closely related to NetKAT, it shows the same type of language-theoretic techniques can still be applied at match-action's lower abstraction level. In particular, we consider MatchKAT's equational theory, and hence program equivalence between match tables expressing the same forwarding policy. The second part considers mutable global state. Traditionally, NetKAT regards the packet forwarding plane, and hence match tables, to be stateless. We present Stateful NetKAT, a natural extension to NetKAT by adding state that can be modified during packet processing, and we show that subtle interplay between packet and state data now occurs. The last part of this dissertation considers the VPP software switch. VPP exposes a set of low-level interfaces on the underlying hardware that compilers of networking DSLs can potentially target. We give performance benchmarks of a network program compiled to VPP from P4, in order to make the case that exposing more low-level interfaces is beneficial as more optimizations can be made. This work is presented in order to give some evidence to our claim that further study into low-level packet forwarding constructs, such as match-action, can lead to more informed compilation from above.
dc.language.isoen
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subjectCircuit complexity
dc.subjectDenotational semantics
dc.subjectKleene algebra
dc.subjectMatch-action
dc.subjectNetKAT
dc.subjectSoftware-Defined Networking
dc.titlePrimitives for Match-Action in Theory and Practice
dc.typedissertation or thesis
thesis.degree.disciplineComputer Science
thesis.degree.grantorCornell University
thesis.degree.levelDoctor of Philosophy
thesis.degree.namePh. D., Computer Science
dc.contributor.chairKozen, Dexter
dc.contributor.committeeMemberFoster, Nate
dc.contributor.committeeMemberGrimmelmann, James
dcterms.licensehttps://hdl.handle.net/1813/59810
dc.identifier.doihttp://doi.org/10.7298/9vbw-4d54


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Except where otherwise noted, this item's license is described as Attribution 4.0 International

Statistics