research-article

Detecting network load violations for distributed control planes

Authors:

Kausik Subramanian,

Anubhavnidhi Abhashkumar,

Loris D'Antoni,

Aditya AkellaAuthors Info & Claims

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 974 - 988

https://doi.org/10.1145/3385412.3385976

Published: 11 June 2020 Publication History

Abstract

One of the major challenges faced by network operators pertains to whether their network can meet input traffic demand, avoid overload, and satisfy service-level agreements. Automatically verifying if no network links are overloaded is complicated---requires modeling frequent network failures, complex routing and load-balancing technologies, and evolving traffic requirements. We present QARC, a distributed control plane abstraction that can automatically verify whether a control plane may cause link-load violations under failures. QARC is fully automatic and can help operators program networks that are more resilient to failures and upgrade the network to avoid violations. We apply QARC to real datacenter and ISP networks and find interesting cases of load violations. QARC can detect violations in under an hour.

References

[1]

2018. Batfish. https://github.com/batfish/batfish. 2019. ARC. http://bitbucket.org/uw-madison-networking-research/ arc. 2019. Cisco IOS Configuration Fundamentals Command Reference. http://cisco.com/c/en/us/td/docs/ios/fundamentals/command/ reference/cf b ook.html.

[2]

Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 201–219. https: //www.usenix.org/conference/nsdi20/presentation/abhashkumar

[3]

Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. 2008. A scalable, commodity data center network architecture. In ACM SIGCOMM Computer Communication Review, Vol. 38. ACM, 63–74.

Digital Library

[4]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication (Los Angeles, CA, USA) (SIGCOMM ’17). ACM, New York, NY, USA, 155–168.

Digital Library

[5]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, and David Walker. 2016. Don’t Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations. In Proceedings of the ACM SIGCOMM 2016 Conference on SIGCOMM (SIGCOMM ’16).

Digital Library

[6]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2017. Network configuration synthesis with abstract topologies. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 437–451.

Digital Library

[7]

Theophilus Benson, Aditya Akella, and David Maltz. 2009. Unraveling the Complexity of Network Management. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (Boston, Massachusetts) (NSDI’09). USENIX Association, Berkeley, CA, USA, 335–348. http://dl.acm.org/citation.cfm?id=1558977.1559000

Digital Library

[8]

Theophilus Benson, Aditya Akella, and Aman Shaikh. 2011. Demystifying Configuration Challenges and Trade-offs in Network-based ISP Services. In Proceedings of the ACM SIGCOMM 2011 Conference (Toronto, Ontario, Canada) (SIGCOMM ’11). ACM, New York, NY, USA, 302–313.

Digital Library

[9]

Yiyang Chang, Sanjay Rao, and Mohit Tawarmalani. 2017. Robust Validation of Network Designs under Uncertain Demands and Failures. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 347– 362. https://www.usenix.org/conference/nsdi17/technical-sessions/ presentation/chang

[10]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 14th International Conference. 337–340. 2 4

[11]

Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2017. Network-wide Configuration Synthesis. In 29th International Conference on Computer Aided Verification, Heidelberg, Germany, 2017 (CAV’17).

[12]

Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2018. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). USENIX Association, Renton, WA, 579–594. https://www.usenix.org/conference/ nsdi18/presentation/el-hassany

[13]

Seyed K Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. 2016. Efficient Network Reachability Analysis using a Succinct Control Plane Representation. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, 217–232.

Digital Library

[14]

Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). 469–483.

[15]

Bernard Fortz and Mikkel Thorup. 2000. Internet traffic engineering by optimizing OSPF weights. In INFOCOM 2000. Nineteenth annual joint conference of the IEEE computer and communications societies. Proceedings. IEEE, Vol. 2. IEEE, 519–528.

[16]

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic netkat. In European Symposium on Programming Languages and Systems. Springer, 282–309.

Digital Library

[17]

Aaron Gember-Jacobson, Aditya Akella, Ratul Mahajan, and Hongqiang Harry Liu. 2017. Automatically repairing network control planes using an abstract representation. In Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 359–373.

Digital Library

[18]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In Proceedings of the 2016 ACM SIGCOMM Conference (Florianopolis, Brazil) (SIGCOMM ’16). ACM, New York, NY, USA, 300–313.

Digital Library

[19]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. Technical Report. University of Wisconsin-Madison.

[20]

Aaron Gember-Jacobson, Wenfei Wu, Xiujun Li, Aditya Akella, and Ratul Mahajan. 2015. Management Plane Analytics. In Proceedings of the 2015 Internet Measurement Conference (Tokyo, Japan) (IMC ’15). ACM, New York, NY, USA, 395–408. 2815675.2815684

Digital Library

[21]

Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker. 2020. NV: An Intermediate Language for Verification of Network Control Planes. In PLDI. ACM.

[22]

Phillipa Gill, Navendu Jain, and Nachiappan Nagappan. 2011. Understanding Network Failures in Data Centers: Measurement, Analysis, and Implications. In Proceedings of the ACM SIGCOMM 2011 Conference (Toronto, Ontario, Canada) (SIGCOMM ’11). ACM, New York, NY, USA, 350–361.

Digital Library

[23]

Albert Greenberg, James R. Hamilton, Navendu Jain, Srikanth Kandula, Changhoon Kim, Parantap Lahiri, David A. Maltz, Parveen Patel, and Sudipta Sengupta. 2009. VL2: A Scalable and Flexible Data Center Network. In Proceedings of the ACM SIGCOMM 2009 Conference on Data Communication (Barcelona, Spain) (SIGCOMM ’09). ACM, New York, NY, USA, 51–62.

Digital Library

[24]

Chi-Yao Hong, Srikanth Kandula, Ratul Mahajan, Ming Zhang, Vijay Gill, Mohan Nanduri, and Roger Wattenhofer. 2013. Achieving High Utilization with Software-driven WAN. In Proceedings of the ACM SIGCOMM 2013 Conference on SIGCOMM (Hong Kong, China) (SIGCOMM ’13). ACM, New York, NY, USA, 15–26. 10.1145/2486001.2486012

Digital Library

[25]

C. Hopps. 2000. Analysis of an Equal-Cost Multi-Path Algorithm.

[26]

S. Knight, H.X. Nguyen, N. Falkner, R. Bowden, and M. Roughan. 2011. The Internet Topology Zoo. Selected Areas in Communications, IEEE Journal on 29, 9 (october 2011), 1765 –1775.

[27]

JSAC.2011.111002

[28]

Alok Kumar, Sushant Jain, Uday Naik, Anand Raghuraman, Nikhil Kasinadhuni, Enrique Cauich Zermeno, C. Stephen Gunn, Jing Ai, Björn Carlin, Mihai Amarandei-Stavila, Mathieu Robin, Aspi Siganporia, Stephen Stuart, and Amin Vahdat. 2015. BwE: Flexible, Hierarchical Bandwidth Allocation for WAN Distributed Computing. In Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication (London, United Kingdom) (SIGCOMM ’15). ACM, New York, NY, USA, 1–14.

Digital Library

[29]

Praveen Kumar, Yang Yuan, Chris Yu, Nate Foster, Robert Kleinberg, Petr Lapukhov, Chiun Lin Lim, and Robert Soulé. 2018. Semi-Oblivious Detecting Network Load Violations for Distributed Control Planes PLDI ’20, June 15–20, 2020, London, UK Traffic Engineering: The Road Not Taken. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). USENIX Association, Renton, WA, 157–170. https://www.usenix.org/ conference/nsdi18/presentation/kumar

Digital Library

[30]

Dave Lenrow. 2015. Intent: What. Not How. http: //opennetworking.org/?p=1633&option=com w ordpress&Itemid=471.

[31]

Hongqiang Harry Liu, Srikanth Kandula, Ratul Mahajan, Ming Zhang, and David Gelernter. 2014. Traffic Engineering with Forward Fault Correction. In Proceedings of the 2014 ACM Conference on SIGCOMM (Chicago, Illinois, USA) (SIGCOMM ’14). ACM, New York, NY, USA, 527–538.

Digital Library

[32]

Gary Scott Malkin. 1998. RIP Version 2. STD 56. RFC Editor. http: //www.rfc-editor.org/rfc/rfc2453.txt http://www.rfc-editor.org/rfc/ rfc2453.txt.

[33]

David A. Maltz, Geoffrey Xie, Jibin Zhan, Hui Zhang, Gísli Hjálmtýsson, and Albert Greenberg. 2004. Routing Design in Operational Networks: A Look from the Inside. In Proceedings of the 2004 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (Portland, Oregon, USA) (SIGCOMM ’04). ACM, New York, NY, USA, 27–40.

Digital Library

[34]

Athina Markopoulou, Gianluca Iannaccone, Supratik Bhattacharyya, Chen-Nee Chuah, Yashar Ganjali, and Christophe Diot. 2008. Characterization of failures in an operational IP backbone network. IEEE/ACM Transactions on Networking (TON) 16, 4 (2008), 749–762.

Digital Library

[35]

John Moy. 1998. OSPF Version 2. STD 54. RFC Editor. http://www.rfceditor.org/rfc/rfc2328.txt http://www.rfc-editor.org/rfc/rfc2328.txt.

[36]

Gurobi Optimization. 2019. Gurobi. http://www.gurobi.com/.

[37]

Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese. 2016. Scaling Network Verification Using Symmetry and Surgery. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL ’16). ACM, New York, NY, USA, 69–83.

Digital Library

[38]

Yakov Rekhter, Tony Li, and Susan Hares. 2005. A border gateway protocol 4 (BGP-4). Technical Report.

[39]

Matthew Roughan, Albert Greenberg, Charles Kalmanek, Michael Rumsewicz, Jennifer Yates, and Yin Zhang. 2002. Experience in Measuring Backbone Traffic Variability: Models, Metrics, Measurements and Meaning. In Proceedings of the 2Nd ACM SIGCOMM Workshop on Internet Measurment (Marseille, France) (IMW ’02). ACM, New York, NY, USA, 91–92.

Digital Library

[40]

Arjun Roy, Hongyi Zeng, Jasmeet Bagga, George Porter, and Alex C. Snoeren. 2015. Inside the Social Network’s (Datacenter) Network. In Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication (London, United Kingdom) (SIGCOMM ’15). ACM, New York, NY, USA, 123–137. 2785956.2787472

Digital Library

[41]

Rachee Singh, Manya Ghobadi, Klaus-Tycho Foerster, Mark Filer, and Phillipa Gill. 2018. RADWAN: Rate Adaptive Wide Area Network. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (Budapest, Hungary) (SIGCOMM ’18). ACM, New York, NY, USA, 547–560.

Digital Library

[42]

Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. 2017. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL 2017). ACM, New York, NY, USA, 557–571. 3009837.3009843

Digital Library

[43]

Kausik Subramanian, Loris D’Antoni, and Aditya Akella. 2018. Synthesis of Fault-Tolerant Distributed Router Configurations. Proc. ACM Meas. Anal. Comput. Syst. 2, 1, Article 22 (April 2018), 26 pages.

Digital Library

[44]

Kausik Subramanian, Loris DâĂŹAntoni, and Aditya Akella. 2017. Genesis: Synthesizing Forwarding Tables in Multi-Tenant Networks. SIGPLAN Not. 52, 1 (Jan. 2017), 572âĂŞ585. 3093333.3009845

Digital Library

[45]

Yu-Wei Eric Sung, Xiaozheng Tie, Starsky HY Wong, and Hongyi Zeng. 2016. Robotron: Top-down network management at facebook scale. In Proceedings of the 2016 ACM SIGCOMM Conference. ACM, 426–439.

Digital Library

[46]

Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. 2012. FSR: Formal Analysis and Implementation Toolkit for Safe Interdomain Routing. IEEE/ACM Trans. Netw. 20, 6 (Dec. 2012), 1814– 1827.

Digital Library

[47]

Hao Wang, Haiyong Xie, Lili Qiu, Yang Richard Yang, Yin Zhang, and Albert Greenberg. 2006.

[48]

COPE: Traffic Engineering in Dynamic Networks. In Proceedings of the 2006 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (Pisa, Italy) (SIGCOMM ’06). ACM, New York, NY, USA, 99–110.

Digital Library

[49]

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Amsterdam, Netherlands) (OOPSLA 2016). ACM, New York, NY, USA, 765–780.

Digital Library

[50]

Junlan Zhou, Malveeka Tewari, Min Zhu, Abdul Kabbani, Leon Poutievski, Arjun Singh, and Amin Vahdat. 2014. WCMP: Weighted Cost Multipathing for Improved Fairness in Data Centers. In Proceedings of the Ninth European Conference on Computer Systems (Amsterdam, The Netherlands) (EuroSys ’14). ACM, New York, NY, USA, Article 5, 14 pages.

Digital Library

Cited By

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
Wang YLi ZJiang CQiu XRao S(2023)Comparative Synthesis: Learning Near-Optimal Network Designs by QueryProceedings of the ACM on Programming Languages10.1145/35711977:POPL(91-120)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571197
Jiang CLi ZRao STawarmalani MBianchi GMei A(2022)FlexileProceedings of the 18th International Conference on emerging Networking EXperiments and Technologies10.1145/3555050.3569119(110-125)Online publication date: 30-Nov-2022
https://dl.acm.org/doi/10.1145/3555050.3569119
Show More Cited By

Index Terms

Detecting network load violations for distributed control planes
1. Networks
  1. Network properties
    1. Network reliability
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Fast Control Plane Analysis Using an Abstract Representation
SIGCOMM '16: Proceedings of the 2016 ACM SIGCOMM Conference

Networks employ complex, and hence error-prone, routing control plane configurations. In many cases, the impact of errors manifests only under failures and leads to devastating effects. Thus, it is important to proactively verify control plane behavior ...
Fail-in-place network design: interaction between topology, routing algorithm and failures
SC '14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis

The growing system size of high performance computers results in a steady decrease of the mean time between failures. Exchanging network components often requires whole system downtime which increases the cost of failures. In this work, we study a fail-...
Application-driven TCP recovery and non-stop BGP
DSN '13: Proceedings of the 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

Some network protocols tie application state to underlying TCP connections, leading to unacceptable service outages when an endpoint loses TCP state during fail-over or migration. For example, BGP ties forwarding tables to its control plane connections ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2020

1174 pages

ISBN:9781450376136

DOI:10.1145/3385412

General Chair:
Alastair F. Donaldson
Imperial College London, UK
,
Program Chair:
Emina Torlak
University of Washington, USA

Copyright © 2020 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 the author(s) 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional / v1.1

Author Tags

Qualifiers

Research-article

Conference

PLDI '20

Sponsor:

SIGPLAN

PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 15 - 20, 2020

London, UK

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
224
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)4

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Wang YLi ZJiang CQiu XRao S(2023)Comparative Synthesis: Learning Near-Optimal Network Designs by QueryProceedings of the ACM on Programming Languages10.1145/35711977:POPL(91-120)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571197
Jiang CLi ZRao STawarmalani MBianchi GMei A(2022)FlexileProceedings of the 18th International Conference on emerging Networking EXperiments and Technologies10.1145/3555050.3569119(110-125)Online publication date: 30-Nov-2022
https://dl.acm.org/doi/10.1145/3555050.3569119
Grewal KD'Antoni LHsu JJhala RDillig I(2022)P4BID: information flow control in p4Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523717(46-60)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523717
Zhang YXu HXue CKuo T(2022)Probabilistic Analysis of Network Availability2022 IEEE 30th International Conference on Network Protocols (ICNP)10.1109/ICNP55882.2022.9940438(1-11)Online publication date: 30-Oct-2022
https://doi.org/10.1109/ICNP55882.2022.9940438
Kang QXing JQiu YChen ASherwood TBerger EKozyrakis C(2021)Probabilistic profiling of stateful data planes for adversarial testingProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446764(286-301)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446764
Liu BKheradmand ACaesar MGodfrey PZhao BZheng HMadhyastha HPadmanabhan V(2020)Towards Verified Self-Driving InfrastructureProceedings of the 19th ACM Workshop on Hot Topics in Networks10.1145/3422604.3425949(96-102)Online publication date: 4-Nov-2020
https://dl.acm.org/doi/10.1145/3422604.3425949

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