Keeping P4 switches fast and fault-free through automatic verification
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 requirem...
Elmentve itt :
| Szerzők: | |
|---|---|
| Testületi szerző: | |
| Dokumentumtípus: | Cikk |
| Megjelent: |
University of Szeged, Institute of Informatics
Szeged
2019
|
| Sorozat: | Acta cybernetica
24 No. 1 |
| Kulcsszavak: | Számítástechnika, Informatika |
| Tárgyszavak: | |
| doi: | 10.14232/actacyb.24.1.2019.6 |
| Online Access: | http://acta.bibl.u-szeged.hu/59228 |
| Tartalmi kivonat: | 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. |
|---|---|
| Terjedelem/Fizikai jellemzők: | 61-81 |
| ISSN: | 0324-721X |