research-article

Meissa: scalable network testing for programmable data planes

Authors:

Hongqiang Harry Liu,

Xin JinAuthors Info & Claims

SIGCOMM '22: Proceedings of the ACM SIGCOMM 2022 Conference

Pages 350 - 364

https://doi.org/10.1145/3544216.3544247

Published: 22 August 2022 Publication History

Abstract

Ensuring the correctness of programmable data planes is important. Testing offers comprehensive correctness checking, including detecting both code bugs and non-code bugs. However, scalability is a key challenge for testing production-scale data planes to achieve high coverage. This paper presents Meissa, a scalable network testing system for programmable data planes with full path coverage. The core of Meissa is a domain-specific code summary technique that simplifies the control flow graph of a data plane program for scalable testing without sacrificing coverage. Code summary decomposes a data plane program into individual pipelines, and summarizes each pipeline with a succinct representation. We formally prove that Meissa with code summary achieves 100% path coverage. We use both open-source and production-scale data plane programs to evaluate Meissa. The evaluation shows that (i) Meissa is able to test production-scale data plane programs that cannot be supported by state-of-the-art efforts, and (ii) besides P4 code bugs, Meissa is able to not only identify known non-code bugs, but also detect previously-unknown non-code bugs. We also share in this paper several real cases tested by Meissa in a production programmable data plane.

Supplementary Material

PDF File (p350-zheng-supp.pdf)

Supplemental material.

Download
62.62 KB

References

[1]

2020. bf-p4c backend bug 1 detected by Gauntlet. https://github.com/p4gauntlet/gauntlet/blob/master/bugs/tofino/semantic/semantic_bug1.p4.

[2]

2020. bf-p4c backend bug 3 detected by Gauntlet. https://github.com/p4gauntlet/gauntlet/blob/master/bugs/tofino/semantic/semantic_bug3.p4.

[3]

2020. bf-p4c backend bug 6 detected by Gauntlet. https://github.com/p4gauntlet/gauntlet/blob/master/bugs/tofino/semantic/semantic_bug6.p4.

[4]

2020. P4c issue 2147. https://github.com/p4lang/p4c/issues/2147.

[5]

2020. P4c issue 2343. https://github.com/p4lang/p4c/issues/2343.

[6]

2021. Data Plane Development Kit. https://www.dpdk.org.

[7]

2021. Open Tofino. https://github.com/barefootnetworks/Open-Tofino.

[8]

2021. PTF: Packet testing framework. https://github.com/p4lang/ptf.

[9]

Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast multilayer network verification. In USENIX NSDI.

[10]

Paul Ammann and Jeff Offutt. 2016. Introduction to software testing. Cambridge University Press.

[11]

Venkat Arun, Mina Tahmasbi Arashloo, Ahmed Saeed, Mohammad Alizadeh, and Hari Balakrishnan. 2021. Toward formally verifying congestion control behavior. In ACM SIGCOMM.

[12]

Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. Cvc4. In International Conference on Computer Aided Verification.

[13]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A general approach to network configuration verification. In ACM SIGCOMM.

[14]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2016. Don't mind the gap: Bridging network-wide objectives and device-level configurations. In ACM SIGCOMM.

[15]

Ran Ben Basat, Sivaramakrishnan Ramanathan, Yuliang Li, Gianni Antichi, Minian Yu, and Michael Mitzenmacher. 2020. Pint: Probabilistic in-band network telemetry. In ACM SIGCOMM.

Digital Library

[16]

Rudiger Birkner, Tobias Brodmann, Petar Tsankov, Laurent Vanbever, and Martin T Vechev. 2021. Metha: Network Verifiers Need To Be Correct Too!. In USENIX NSDI.

[17]

Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. 2014. P4: Programming protocol-independent packet processors. ACM SIGCOMM Computer Communication Review (2014).

Digital Library

[18]

Pietro Bressana, Noa Zilberman, and Robert Soule. 2020. Finding hard-to-find data plane bugs with a PTA. In ACM CoNEXT.

[19]

Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX OSDI.

Digital Library

[20]

Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later. Commun. ACM (2013).

Digital Library

[21]

Eric Hayden Campbell, William T Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soule, and Nate Foster. 2021. Avenir: Managing Data Plane Diversity with Control Plane Synthesis. In USENIX NSDI.

[22]

Yiyang Chang, Chuan Jiang, Ashish Chandra, Sanjay Rao, and Mohit Tawarmalani. 2019. Lancet: Better network resilience by designing for pruned failure sets. Proceedings of the ACM on Measurement and Analysis of Computing Systems (2019).

Digital Library

[23]

Yiyang Chang, Sanjay Rao, and Mohit Tawarmalani. 2017. Robust validation of network designs under uncertain demands and failures. In USENIX NSDI.

[24]

Junjie Chen, Wenxiang Hu, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang, and Bing Xie. 2016. An empirical comparison of compiler testing techniques. In International Conference on Software Engineering.

[25]

Xiaoqi Chen, Shir Landau-Feibish, Mark Braverman, and Jennifer Rexford. 2020. Beaucoup: Answering many network traffic queries, one memory update at a time. In ACM SIGCOMM.

Digital Library

[26]

Leonardo De Moura and Nikolaj Bjorner. 2008. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

[27]

Dragos Dumitrescu, Radu Stoenescu, Lorina Negreanu, and Costin Raiciu. 2020. bf4: towards bug-free P4 programs. In ACM SIGCOMM.

[28]

Dragos Dumitrescu, Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2019. Dataplane equivalence and its applications. In USENIX NSDI.

[29]

Tomer Eliyahu, Yafim Kazak, Guy Katz, and Michael Schapira. 2021. Verifying learning-augmented systems. In ACM SIGCOMM.

[30]

Tiago Ferreira, Harrison Brewton, Loris D'Antoni, and Alexandra Silva. 2021. Prognosis: closed-box analysis of network protocol implementations. In ACM SIGCOMM.

[31]

Lucas Freire, Miguel Neves, Lucas Leal, Kirill Levchenko, Alberto Schaeffer-Filho, and Marinho Barcellos. 2018. Uncovering bugs in p4 programs with assertion-based verification. In Symposium on SDN Research.

Digital Library

[32]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast control plane analysis using an abstract representation. In ACM SIGCOMM.

[33]

Patrice Godefroid. 2007. Compositional Dynamic Test Generation. SIGPLAN Not. (2007).

[34]

Alex Horn, Ali Kheradmand, and Mukul Prasad. 2017. Delta-net: Real-time network verification using atoms. In USENIX NSDI.

[35]

Qun Huang, Siyuan Sheng, Xiang Chen, Yungang Bao, Rui Zhang, Yanwei Xu, and Gong Zhang. 2021. Toward nearly-zero-error sketching via compressive sensing. In USENIX NSDI.

[36]

Qun Huang, Haifeng Sun, Patrick PC Lee, Wei Bai, Feng Zhu, and Yungang Bao. 2020. Omnimon: Re-architecting network telemetry with resource efficiency and full accuracy. In ACM SIGCOMM.

[37]

Karthick Jayaraman, Nikolaj Bjorner, Geoff Outhred, and Charlie Kaufman. 2014. Automated analysis and debugging of network connectivity policies. Microsoft Research (2014).

[38]

Karthick Jayaraman, Nikolaj Bjorner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. 2019. Validating datacenters at scale. In ACM SIGCOMM.

[39]

Chuan Jiang, Sanjay Rao, and Mohit Tawarmalani. 2020. PCF: provably resilient flexible routing. In ACM SIGCOMM.

[40]

Xin Jin, Xiaozhou Li, Haoyu Zhang, Robert Soule, Jeongkeun Lee, Nate Foster, Changhoon Kim, and Ion Stoica. 2017. Netcache: Balancing key-value stores with fast in-network caching. In ACM SOSP.

Digital Library

[41]

Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In ACM SIGCOMM.

[42]

Siva Kesava Reddy Kakarla, Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, Yuval Tamir, and George Varghese. 2020. Finding network misconfigurations by automatic template inference. In USENIX NSDI.

[43]

Qiao Kang, Jiarong Xing, Yiming Qiu, and Ang Chen. 2021. Probabilistic profiling of stateful data planes for adversarial testing. In ACM ASPLOS.

[44]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header space analysis: Static checking for networks. In USENIX NSDI.

[45]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2013. Veriflow: Verifying network-wide invariants in real time. In USENIX NSDI.

[46]

Changhoon Kim, Anirudh Sivaraman, Naga Katta, Antonin Bas, Advait Dixit, and Lawrence J Wobker. 2015. In-band network telemetry via programmable dataplanes. In ACM SIGCOMM.

[47]

Daehyeok Kim, Zaoxing Liu, Yibo Zhu, Changhoon Kim, Jeongkeun Lee, Vyas Sekar, and Srinivasan Seshan. 2020. Tea: Enabling state-intensive network functions on programmable switches. In ACM SIGCOMM.

[48]

Daehyeok Kim, Jacob Nelson, Dan RK Ports, Vyas Sekar, and Srinivasan Seshan. 2021. Redplane: Enabling fault-tolerant stateful in-switch applications. In ACM SIGCOMM.

[49]

Hyojoon Kim, Joshua Reich, Arpit Gupta, Muhammad Shahbaz, Nick Feamster, and Russ Clark. 2015. Kinetic: Verifiable dynamic network control. In USENIX NSDI.

[50]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM (1976).

[51]

Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. 2012. Efficient state merging in symbolic execution. ACM SIGPLAN Notices (2012).

[52]

ChonLam Lao, Yanfang Le, Kshiteej Mahajan, Yixi Chen, Wenfei Wu, Aditya Akella, and Michael M Swift. 2021. ATP: In-network Aggregation for Multi-tenant Learning. In USENIX NSDI. 741--761.

[53]

Vu Le, Chengnian Sun, and Zhendong Su. 2015. Finding deep compiler bugs via guided stochastic program mutation. ACM SIGPLAN Notices (2015).

[54]

Jialin Li, Jacob Nelson, Ellis Michael, Xin Jin, and Dan RK Ports. 2020. Pegasus: Tolerating skewed workloads in distributed storage with in-network coherence directories. In USENIX OSDI.

[55]

Yuliang Li, Rui Miao, Hongqiang Harry Liu, Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, and Minlan Yu. 2019. HPCC: High precision congestion control. In ACM SIGCOMM.

[56]

Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soule, Han Wang, Cualin Cacscaval, Nick McKeown, and Nate Foster. 2018. P4v: Practical verification for programmable data planes. In ACM SIGCOMM.

[57]

Zaoxing Liu, Hun Namkung, Georgios Nikolaidis, Jeongkeun Lee, Changhoon Kim, Xin Jin, Vladimir Braverman, Minlan Yu, and Vyas Sekar. 2021. Jaqen: A high-performance switch-native approach for detecting and mitigating volumetric ddos attacks with programmable switches. In USENIX Security Symposium.

[58]

Nuno P Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking beliefs in dynamic networks. In USENIX NSDI.

[59]

Rui Miao, Hongyi Zeng, Changhoon Kim, Jeongkeun Lee, and Minlan Yu. 2017. Silkroad: Making stateful layer-4 load balancing fast and cheap using switching asics. In ACM SIGCOMM.

Digital Library

[60]

Miguel Neves, Lucas Freire, Alberto Schaeffer-Filho, and Marinho Barcellos. 2018. Verification of p4 programs in feasible time using assertions. In ACM CoNEXT.

[61]

Andres Notzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas. 2018. P4pktgen: Automated test case generation for p4 programs. In Symposium on SDN Research.

Digital Library

[62]

Tian Pan, Nianbing Yu, Chenhao Jia, Jianwen Pi, Liang Xu, Yisong Qiao, Zhiguo Li, Kun Liu, Jie Lu, Jianyuan Lu, Enge Song, Jiao Zhang, Tao Huang, and Shunmin Zhu. 2021. Sailfish: Accelerating cloud-scale multi-tenant multi-service gateways with programmable switches. In ACM SIGCOMM.

Digital Library

[63]

Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, and Scott Shenker. 2015. New directions for network verification. In Summit on Advances in Programming Languages.

[64]

Aurojit Panda, Ori Lahav, Katerina Argyraki, Mooly Sagiv, and Scott Shenker. 2017. Verifying reachability in networks with mutable datapaths. In USENIX NSDI.

[65]

Van-Thuan Pham, Marcel Bohme, and Abhik Roychoudhury. 2020. AFLNet: a greybox fuzzer for network protocols. In International Conference on Software Testing, Validation and Verification.

[66]

Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. In USENIX NSDI.

Digital Library

[67]

Jose Miguel Rojas and Corina S Pasareanu. 2013. Compositional symbolic execution through program specialization. BYTECODE'13 (ETAPS) (2013).

[68]

Fabian Ruffy, Tao Wang, and Anirudh Sivaraman. 2020. Gauntlet: Finding bugs in compilers for programmable packet processing. In USENIX OSDI.

[69]

Leonid Ryzhyk, Nikolaj Bjorner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B Terry, and George Varghese. 2017. Correct by construction networks using stepwise refinement. In USENIX NSDI.

[70]

Amedeo Sapio, Marco Canini, Chen-Yu Ho, Jacob Nelson, Panos Kalnis, Changhoon Kim, Arvind Krishnamurthy, Masoud Moshref, Dan RK Ports, and Peter Richtarik. 2019. Scaling distributed machine learning with in-network aggregation. arXiv preprint arXiv:1903.06701 (2019).

[71]

Tibor Schneider, Rudiger Birkner, and Laurent Vanbever. 2021. Snowcap: synthesizing network-wide configuration updates. In ACM SIGCOMM.

[72]

Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing engine for C. ACM SIGSOFT Software Engineering Notes (2005).

[73]

Jinghao Shi, Shuvendu K Lahiri, Ranveer Chandra, and Geoffrey Challen. 2018. Wireless protocol validation under uncertainty. Formal methods in system design (2018).

[74]

Samuel Steffen, Timon Gehr, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2020. Probabilistic verification of network configurations. In ACM SIGCOMM.

[75]

Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting fuzzing through selective symbolic execution. In ISOC Network and Distributed System Security Symposium.

[76]

Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2018. Debugging P4 programs with Vera. In ACM SIGCOMM.

[77]

Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2016. Symnet: Scalable symbolic execution for modern networks. In ACM SIGCOMM.

Digital Library

[78]

Alan Tang, Siva Kesava Reddy Kakarla, Ryan Beckett, Ennan Zhai, Matt Brown, Todd Millstein, Yuval Tamir, and George Varghese. 2021. Campion: debugging router configuration differences. In ACM SIGCOMM.

[79]

Bingchuan Tian, Jiaqi Gao, Mengqi Liu, Ennan Zhai, Yanqing Chen, Yu Zhou, Li Dai, Feng Yan, Mengjing Ma, Ming Tang, Jie Lu, Xionglie Wei, Hongqiang Harry Liu, Ming Zhang, Chen Tian, and Minlan Yu. 2021. Aquila: a practically usable verification system for production-scale programmable data planes. In ACM SIGCOMM.

[80]

Bingchuan Tian, Xinyi Zhang, Ennan Zhai, Hongqiang Harry Liu, Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, Da Yu, Chen Tian, Haitao Zheng, and Ben Y. Zhao. 2019. Safely and automatically updating in-network acl configurations with intent language. In ACM SIGCOMM.

[81]

Nikolai Tillmann and Jonathan De Halleux. 2008. Pex-white box test generation for. net. In International Conference on Tests and Proofs.

[82]

Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, and Sharon Shoham. 2016. Some complexity results for stateful network verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[83]

Xusheng Xiao, Sihan Li, Tao Xie, and Nikolai Tillmann. 2013. Characteristic studies of loop problems for structural test generation via symbolic execution. In International Conference on Automated Software Engineering.

Digital Library

[84]

Tao Xie, Nikolai Tillmann, Jonathan De Halleux, and Wolfram Schulte. 2009. Fitness-guided path exploration in dynamic symbolic execution. In IEEE/IFIP International Conference on Dependable Systems and Networks.

[85]

Qiongwen Xu, Michael D. Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman. 2021. Synthesizing Safe and Efficient Kernel Extensions for Packet Processing. In ACM SIGCOMM.

[86]

Xieyang Xu, Ryan Beckett, Karthick Jayaraman, Ratul Mahajan, and David Walker. 2021. Test coverage metrics for the network. In ACM SIGCOMM.

[87]

Wei Yang, Mukul R Prasad, and Tao Xie. 2013. A grey-box approach for automated GUI-model generation of mobile applications. In International Conference on Fundamental Approaches to Software Engineering.

Digital Library

[88]

Nofel Yaseen, Behnaz Arzani, Ryan Beckett, Selim Ciraci, and Vincent Liu. 2020. Aragog: Scalable Runtime Verification of Shardable Networked Systems. In USENIX OSDI.

[89]

Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. 2020. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In ACM SIGCOMM.

[90]

Farnaz Yousefi, Anubhavnidhi Abhashkumar, Kausik Subramanian, Kartik Hans, Soudeh Ghorbani, and Aditya Akella. 2020. Liveness verification of stateful network functions. In USENIX NSDI.

[91]

Liangcheng Yu, John Sonchack, and Vincent Liu. 2020. Mantis: Reactive programmable switches. In ACM SIGCOMM.

Digital Library

[92]

Zhuolong Yu, Chuheng Hu, Jingfeng Wu, Xiao Sun, Vladimir Braverman, Mosharaf Chowdhury, Zhenhua Liu, and Xin Jin. 2021. Programmable packet scheduling with a single queue. In ACM SIGCOMM.

[93]

Yifei Yuan, Soo-Jin Moon, Sahil Uppal, Limin Jia, and Vyas Sekar. 2020. NetSMC: A custom symbolic model checker for stateful network verification. In USENIX NSDI.

[94]

Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. 2019. Verifying software network functions with no verification expertise. In ACM SOSP.

[95]

Chaoliang Zeng, Layong Luo, Teng Zhang, Zilong Wang, Luyang Li, Wenchen Han, Nan Chen, Lebing Wan, Lichao Liu, Zhipeng Ding, Xiongfei Geng, Tao Feng, Feng Ning, Kai Chen, and Chuanxiong Guo. 2022. Tiara: A Scalable and Efficient Hardware Acceleration Architecture for Stateful Layer-4 Load Balancing. In USENIX NSDI.

[96]

Hongyi Zeng, Shidong Zhang, Fei Ye, Vimalkumar Jeyakumar, Mickey Ju, Junda Liu, Nick McKeown, and Amin Vahdat. 2014. Libra: Divide and conquer to verify forwarding tables in huge networks. In USENIX NSDI.

[97]

Ennan Zhai, Ang Chen, Ruzica Piskac, Mahesh Balakrishnan, Bingchuan Tian, Bo Song, and Haoliang Zhang. 2020. Check before you change: Preventing correlated failures in service updates. In USENIX NSDI.

[98]

Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. 2020. Automated verification of customizable middlebox properties with gravel. In USENIX NSDI.

[99]

Yinda Zhang, Zaoxing Liu, Ruixin Wang, Tong Yang, Jizhou Li, Ruijie Miao, Peng Liu, Ruwen Zhang, and Junchen Jiang. 2021. CocoSketch: high-performance sketch-based measurement over arbitrary partial key query. In ACM SIGCOMM.

[100]

Yikai Zhao, Kaicheng Yang, Zirui Liu, Tong Yang, Li Chen, Shiyi Liu, Naiqian Zheng, Ruixin Wang, Hanbo Wu, Yi Wang, and Nicholas Zhang. 2021. Light-Guardian: A Full-Visibility, Lightweight, In-band Telemetry System Using Sketchlets. In USENIX NSDI.

[101]

Yu Zhou, Chen Sun, Hongqiang Harry Liu, Rui Miao, Shi Bai, Bo Li, Zhilong Zheng, Lingjun Zhu, Zhen Shen, Yongqing Xi, Pengcheng Zhang, Dennis Cai, Ming Zhang, and Mingwei Xu. 2020. Flow event telemetry on programmable data plane. In ACM SIGCOMM.

[102]

Hang Zhu, Kostis Kaffes, Zixu Chen, Zhenming Liu, Christos Kozyrakis, Ion Stoica, and Xin Jin. 2020. Racksched: A microsecond-scale scheduler for rack-scale computers. In USENIX OSDI.

Cited By

Yao YCui ZTian LLi MPan FHu Y(2024)Scaver: A Scalable Verification System for Programmable NetworkProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673887(14-19)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673887
Li RYuan YYe FLiu MYang RYu YGuo TMa QZeng XXu CCai DZhai ESekar VYu MSeneviratne AVeitch D(2024)A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k FailuresProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672246(228-243)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672246
Wan YFeng CWu KWang J(2024)Towards Easy-to-Monitor Networks: Network Design and Measurement Path ConstructionIEEE Transactions on Network Science and Engineering10.1109/TNSE.2024.341878111:5(4397-4412)Online publication date: Sep-2024
https://doi.org/10.1109/TNSE.2024.3418781
Show More Cited By

Index Terms

Meissa: scalable network testing for programmable data planes
1. Networks
  1. Network services
    1. Programmable networks
2. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions

Recommendations

Aquila: a practically usable verification system for production-scale programmable data planes
SIGCOMM '21: Proceedings of the 2021 ACM SIGCOMM 2021 Conference

This paper presents Aquila, the first practically usable verification system for Alibaba's production-scale programmable data planes. Aquila addresses four challenges in building a practically usable verification: (1) specification complexity; (2) ...
A Hybrid Testing System on P4 Cloud Gateway
FMANO '24: Proceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation

P4 gateway is the hub of cloud network, and with the growth of cloud traffic scale, the reliability of a cloud gateway must be guaranteed by testing. The existing cloud gateway testing solutions, such as symbolic execution and fuzzing, perform either ...
Relating counterexamples to test cases in CTL model checking specifications
A-MOST '07: Proceedings of the 3rd international workshop on Advances in model-based testing

Counterexamples produced by model checkers are frequently exploited for the purpose of testing. Counterexamples and test cases are generally treated as essentially the same thing, while in fact they can differ significantly. For example, it might take ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '22: Proceedings of the ACM SIGCOMM 2022 Conference

August 2022

858 pages

ISBN:9781450394208

DOI:10.1145/3544216

General Chairs:
Fernando Kuipers
Delft University of Technology
,
Ariel Orda
Technion Israel Institute of Technology

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 August 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

SIGCOMM '22

Sponsor:

SIGCOMM

SIGCOMM '22: ACM SIGCOMM 2022 Conference

August 22 - 26, 2022

Amsterdam, Netherlands

Acceptance Rates

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
1,039
Total Downloads

Downloads (Last 12 months)166
Downloads (Last 6 weeks)18

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yao YCui ZTian LLi MPan FHu Y(2024)Scaver: A Scalable Verification System for Programmable NetworkProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673887(14-19)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673887
Li RYuan YYe FLiu MYang RYu YGuo TMa QZeng XXu CCai DZhai ESekar VYu MSeneviratne AVeitch D(2024)A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k FailuresProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672246(228-243)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672246
Wan YFeng CWu KWang J(2024)Towards Easy-to-Monitor Networks: Network Design and Measurement Path ConstructionIEEE Transactions on Network Science and Engineering10.1109/TNSE.2024.341878111:5(4397-4412)Online publication date: Sep-2024
https://doi.org/10.1109/TNSE.2024.3418781
Liu HChen XHuang QSun GWang PZhang DWu CLiu XYang Q(2024)Toward Resource-Efficient and High- Performance Program Deployment in Programmable NetworksIEEE/ACM Transactions on Networking10.1109/TNET.2024.341338832:5(4270-4285)Online publication date: Oct-2024
https://doi.org/10.1109/TNET.2024.3413388
Rieger SLux LSchmitt JStiemerling M(2024)DigSiNet: Using Multiple Digital Twins to Provide Rhythmic Network ConsistencyNOMS 2024-2024 IEEE Network Operations and Management Symposium10.1109/NOMS59830.2024.10575632(1-5)Online publication date: 6-May-2024
https://doi.org/10.1109/NOMS59830.2024.10575632
Yang MYang XXu LHou YXie LWang Y(2024)Towards Better QoS and Lower Costs of P4 EIP Gateway at the Edge2024 IEEE 24th International Symposium on Cluster, Cloud and Internet Computing (CCGrid)10.1109/CCGrid59990.2024.00016(57-66)Online publication date: 6-May-2024
https://doi.org/10.1109/CCGrid59990.2024.00016
Liu XGu DChen ZWen JZhang ZMa YWang HJin X(2023)Rise of Distributed Deep Learning Training in the Big Model Era: From a Software Engineering PerspectiveACM Transactions on Software Engineering and Methodology10.1145/359720432:6(1-26)Online publication date: 29-Sep-2023
https://dl.acm.org/doi/10.1145/3597204
Cesen FVogt FCastro ARothenberg C(2023)Towards Multiple Pipelines Network Emulation with P72023 IEEE 9th International Conference on Network Softwarization (NetSoft)10.1109/NetSoft57336.2023.10175488(290-292)Online publication date: 19-Jun-2023
https://doi.org/10.1109/NetSoft57336.2023.10175488
Chen XWu CLiu XHuang QZhang DZhou HYang QKhan M(2023)Empowering Network Security With Programmable Switches: A Comprehensive SurveyIEEE Communications Surveys & Tutorials10.1109/COMST.2023.326598425:3(1653-1704)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1109/COMST.2023.3265984

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents