Keeping P4 switches fast and fault-free through automatic verification

Lukács Dániel and Tejfel Máté and Pongrácz Gergely: Keeping P4 switches fast and fault-free through automatic verification. In: Acta cybernetica, (24) 1. pp. 61-81. (2019)

[thumbnail of actacyb_24_1_2019_061_081.pdf]
Cikk, tanulmány, mű

Download (854kB) | Preview


The networking dataplane is going through a paradigm shift as softwarization of switches sees an increased pull from the market. Yet, software tooling to support development with these new technologies is still in its infancy. In this work, we introduce a framework for verifying performance requirement conformance of data plane protocols defined in the P4 language . We present a framework that transforms a P4 program in a versatile symbolic formula which can be utilized to answer various performance queries. We represented the system using denotational semantics and it can be easily extended with low-level target-dependent information. We demonstrate the operation of this system on a toy specification.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2019
Volume: 24
Number: 1
ISSN: 0324-721X
Page Range: pp. 61-81
Language: English
Publisher: University of Szeged, Institute of Informatics
Place of Publication: Szeged
Event Title: Conference of PhD students in computer science (11.) (2018) (Szeged)
Related URLs:
DOI: 10.14232/actacyb.24.1.2019.6
Uncontrolled Keywords: Számítástechnika, Informatika
Additional Information: Bibliogr.: p. 80-81. ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2019. Jul. 17. 13:18
Last Modified: 2022. Jun. 21. 09:07

Actions (login required)

View Item View Item