SCIENCE CHINA Information Sciences, Volume 62 , Issue 6 : 062101(2019) https://doi.org/10.1007/s11432-018-9826-x

Predictive analysis for race detection in software-defined networks

More info
  • ReceivedJul 31, 2018
  • AcceptedFeb 18, 2019
  • PublishedMay 8, 2019



This work was partially supported by National Basic Research Program of China (973 Program) (Grant No. 2014CB340702), National Natural Science Foundation of China (Grant Nos. 91418202, 61472178, 91318301), and National Science Foundation for Young Scientists of China (Grant No. 61702256).


[1] Open Networking Foundation. OpenFlow Switch Specification. version 1.3.3. 2013. https://www.opennetworking.org/wp-content/uploads/2014/10/\\openflow-spec-v1.3.3.pdf. Google Scholar

[2] Deng D D, Jin G L, de Kruijf M. Fixing, preventing, and recovering from concurrency bugs. Sci China Inf Sci, 2015, 58: 1-18 CrossRef Google Scholar

[3] Wu Z, Lu K, Wang X. Surveying concurrency bug detectors based on types of detected bugs. Sci China Inf Sci, 2017, 60: 031101 CrossRef Google Scholar

[4] Xu L, Huang J, Hong S M, et al. Attacking the brain: races in the SDN control plane. In: Proceedings of the 26th USENIX Security Symposium, Vancouver, 2017. 451--468. Google Scholar

[5] Cai Y, Cao L W. Effective and precise dynamic detection of hidden races for Java programs. In: Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, Bergamo, 2015. 450--461. Google Scholar

[6] Huang J, Meredith P O, Rosu G. Maximal sound predictive race detection with control flow abstraction. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, Edinburgh, 2014. 337--348. Google Scholar

[7] Huang J, Zhou J, Zhang C. Scaling predictive analysis of concurrent programs by removing trace redundancy. ACM Trans Softw Eng Methodol, 2013, 22: 1-21 CrossRef Google Scholar

[8] Liu P, Tripp O, Zhang X Y. IPA: improving predictive analysis with pointer analysis. In: Proceedings of the 25th International Symposium on Software Testing and Analysis, Saarbrücken, 2016. 59--69. Google Scholar

[9] Wang C, Kundu S, Limaye R. Symbolic predictive analysis for concurrent programs. Form Asp Comp, 2011, 23: 781-805 CrossRef Google Scholar

[10] El-Hassany A, Miserez J, Bielik P, et al. SDNRacer: concurrency analysis for software-defined networks. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, Santa Barbara, 2016. 402--415. Google Scholar

[11] Zhang Z, Chen Z, Gao R. An empirical study on constraint optimization techniques for test generation. Sci China Inf Sci, 2017, 60: 012105 CrossRef Google Scholar

[12] Big Switch Networks, Inc. Floodlight learning switch. 2013. https://github.com/floodlight/floodlight/tree/v0.91/src/main\\/java/net/floodlightcontroller/learningswitch. Google Scholar

[13] McCauley J. POX EEL L2 learning switch. 2015. https://github.com/noxrepo/pox/blob/eel/pox/forwarding/\\l2_learning.py. Google Scholar

[14] Big Switch Networks, Inc. Floodlight forwarding application. 2013. https://github.com/floodlight/floodlight/blob/v0.91/src/\\main/java/net/floodlightcontroller/forwarding/Forwarding.java. Google Scholar

[15] McCauley J. POX angler forwarding application. 2012. https://github.com/noxrepo/pox/blob/angler/pox/forwarding/\\l2_multi.py. Google Scholar

[16] McCauley J. POX EEL forwarding application. 2015. https://github.com/noxrepo/pox/blob/eel/pox/forwarding/\\l2_multi.py. Google Scholar

[17] Open Networking Laboratory. ONOS: forwarding application. 2015. https://github.com/opennetworkinglab/onos/tree/onos-1.2/apps/fwd. Google Scholar

[18] Big Switch Networks, Inc. Floodlight circuit pusher application. 2013. https://github.com/floodlight/floodlight/tree/v0.91/\\apps/circuitpusher. Google Scholar

[19] Big Switch Networks, Inc. Floodlight firewall. 2013. https://github.com/floodlight/floodlight/tree/v0.91/src/main/java/net/\\floodlightcontroller/firewall. Google Scholar

[20] Big Switch Networks, Inc. Floodlight load-balancer application. 2013. https://github.com/floodlight/floodlight/tree/v0.91/\\src/main/java/net/floodlightcontroller/loadbalancer. Google Scholar

[21] Sun X S, Agarwal A, Ng T S E. Controlling Race Conditions in OpenFlow to Accelerate Application Verification and Packet Forwarding. IEEE Trans Netw Serv Manage, 2015, 12: 263-277 CrossRef Google Scholar

[22] Majumdar R, Tetali S D, Wang Z. Kuai: a model checker for software-defined networks. In: Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design, Portland, 2014. 163--170. Google Scholar

[23] Khurshid A, Zhou W, Caesar M. Veriflow: verifying network-wide invariants in real time. SIGCOMM Comput Commun Rev, 2012, 42: 467-472 CrossRef Google Scholar

[24] May R, EI-Hassany A, Vanbever L, et al. BigBug: practical concurrency analysis for SDN. In: Proceedings of the Symposium on SDN Research, Santa Clara, 2017. 88--94. Google Scholar

[25] Naik M, Aiken A, Whaley J. Effective static race detection for Java. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Ottawa, 2006. 308--319. Google Scholar

[26] Luo Z D, Hillis L, Das R, et al. Effective static analysis to find concurrency bugs in Java. In: Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation, Timisoara, 2010. 135--144. Google Scholar

[27] Pozniansky E, Schuster A. Efficient on-the-fly data race detection in multithreaded C+ programs. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Diego, 2003. 179--190. Google Scholar

[28] Serebryany K, Iskhodzhanov T. ThreadSanitizer: data race detection in practice. In: Proceedings of the Workshop on Binary Instrumentation and Applications, New York, 2009. 62--71. Google Scholar

[29] Xie X W, Xue J L. Acculock: accurate and efficient detection of data races. In: Proceedings of the 9th International Symposiumon Code Generation and Optimization, Nanjing, 2011. 201--212. Google Scholar

[30] Yu Y, Rodeheffer T, Chen W. RaceTrack: efficient detection of data race conditions via adaptive tracking. In: Proceedings of ACM Symposium on Operating Systems Principles, Brighton, 2005. 221--234. Google Scholar

[31] Yannis S, Jacob M E, Caitlin S, et al. Sound predictive race detection in polynomial time. In: Proceedings of the 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, 2012. 387--399. Google Scholar

[32] Dileep K, Umang M, Mahesh V. Dynamic race prediction in linear time. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, 2017. 157--170. Google Scholar

[33] Savage S, Burrows M, Nelson G. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst, 1997, 15: 391-411 CrossRef Google Scholar

[34] Flanagan C, Freund S N. FastTrack: efficient and precise dynamic race detection. In: Proceedings of the 30th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, Dublin, 2009. 121--133. Google Scholar

[35] Sen K. Race directed random testing of concurrent programs. In: Proceedings of the 29th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, Tucson, 2008. 11--21. Google Scholar

[36] Callahan R, Choi J D. Hybrid dynamic data race detection. In: Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, California, 2003. 167--178. Google Scholar

  • Figure 1

    (Color online) An example of a LearningSwitch application in Floodlight and a sequence of events (represented by numbers) which causes three race conditions.

  • Figure 2

    (Color online) A segment of event sequence in Figure 1 and two race conditions detected by SDN-predict.

  • Figure 3

    (Color online) Another segment of event sequence in Figure 1 and a race condition detected by SDN-predict.

  • Figure 4

    (Color online) The overview of SDN-predict.

  • Figure 5

    The constraint encoding for the trace in our example.

  • Figure 6

    (Color online) Race detection capability of the two detectors. LS: LearingSwitch, FO: Forwarding, CP: CircuitPusher, FW: FireWall, LB: LoadBalancer, S: Star, M: Mesh, B: BinTree, PE: Pox EEL, F: Floodlight, PA: Pox Angler, PEF: Pox EEL Fx, O: ONOS.

  • Figure 7

    (Color online) Analysis time for traces from Table 3.

  • Table 1   The events in each SDN device and their related messages and operations
    SwMsgHandlePACKET_OUT, FLOW_MODRead, add, modify, delete
    SwMsgSendPACKET_IN, FLOW_REMOVED$\emptyset$
    CtrlMsgSendPACKET_OUT, FLOW_MOD$\emptyset$
  • Table 2   The encoding rules for MHB constraints ($X_{e_1.{\rm~eid}}~<~X_{e_2.{\rm~eid}}$)
    CategoryRuleEvent 1Event 2
    pid_out $\rightarrow$ pid_in
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $e_2$ $\in$ SwPktSend
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $e_2$ $\in$ SwMsgHandle
    3$e_1$ $\in$ HostPktHandle$e_2$ $\in$ HostPktSend
    $e_1$ $\in$ SwPktSend $\cup$ HostPktSend
    $e_2$ $\in$ SwPktHandle $\cup$ HostPktHandle
    mid_out $\rightarrow$ mid_in
    $e_1$ $\in$ SwPktHandle $\cup$ SwMsgHandle
    $\cup$ SwFlowRemoved
    $e_2$ $\in$ SwMsgSend
    6$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ CtrlMsgSend
    7$e_1$ $\in$ SwMsgSend$e_2$ $\in$ CtrlMsgHandle
    8$e_1$ $\in$ CtrlMsgSend$e_2$ $\in$ SwMsgHandle
    ($e_2.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    9$e_1$ $\in$ SwMsgHandle$e_2$ $\in$ SwMsgHandle
    ($e_1.{\rm~msg\_type}$ =BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    10$e_1$ $\in$ SwMsgHandle$e_2$ $\in$ SwMsgHandle
    ($e_2.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    11$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ SwMsgHandle
    ($e_1.{\rm~msg\_type}$ = BARRIER
    $e_1.{\rm~sw}~=~e_2.{\rm~sw}$ $e_1~\prec_{\tau}~e_2$)
    12$e_1$ $\in$ CtrlMsgHandle$e_2$ $\in$ SwMsgHandle
    TIME1 ($e_2.t~-e_1.t~>~\delta$)
    $e_1~\in$ SwPktHandle
    $\cup$ SwMsgHandle
    $e_2~\in$ SwMsgHandle
    TIME2 ($e_2.t~-e_1.t~>~\delta$)
    14$e_1~\in$ SwMsgHandle
    $e_2~\in$ SwPktHandle $\cup$ SwMsgHandle
    15$e_1~\in$ SwMsgHandle
    $e_2~\in$ AsyncFlowExpiry
  • Table 3   Reported races for different traces with applying time filter using $\delta~=2$ s$^{\rm~a)}$
    Num. of eventsSDN-predictSDNRacer
    cmidrule11-14 App.TopologyControllerTotalWRRDRacesComm.TimeRemain.RacesComm.TimeRemain.
    2*StarPox EEL19374230925574102942186610
    2*MeshPox EEL27416665704031432453238712124
    2*BinTreePox EEL40334876636408662571144966620666133766465
    5*StarPox Angler10641668352586133217
    Pox EEL145819180135351010984241
    Pox EEL Fx1848292601955312189145422
    5*MeshPox Angler24813483451252002032311619116
    For-Pox EEL3062050590348217254052351597
    wardingPox EEL Fx30316514643489719276206628
    5*BinTreePox Angler21062863592093513397723030820447131796988280
    Pox EEL436250445351918402031137833734385279566201228
    Pox EEL Fx428346741344297429771199121125091223824229
    Total racestext–7187text–6014