The first tool that we will talk about is this tool called Nice. The goal of Nice is can we build a tool for systematically testing data center applications, especially from the networking perspective. A huge scalability challenge is in building a tool like that. First of all, you look at the data plane. There's a huge space of possible packets. So in any given application running on a number of such servers, there are several different flows that are going on even within a single application, and across applications. Every application is generating these packets, and all of these packets represent a huge space. Then if you look at the control plane, there's a huge space of event ordering in the network. So these are two different aspects of it which makes it quite involved in terms of thinking about how to build a scalable tool for analyzing the network traffic, and figuring out in terms of testing and debugging them. But the good news is there's equivalence class of data packets. Now, what do I mean by that? Well, suppose I have a source here, and I have a destination here, and I'm sending network packet from here to here, it is probably following a particular flow. So if I startup a TCP/IP connection, then I'm sending a whole bunch of packets. You can say at some level, all of these packets are equivalent to one another, because the content will be different, but it is going from one source to the destination. So there's the equivalence classes of data packets. In fact, this is exactly the premise behind SDN in the first place. The fact that you're essentially setting things up is because the fact that you're going to amortize over the flow of packets. So that's one thing. The second thing is that you can use application knowledge to do the event ordering, and navigate this space. So those are some of the underlying principles in Nice, and it's a pun on words, is there no bugs and controller execution, that's the acronym for Nice. It is a tool for automatically testing open-flow applications. What we want to do is have a systematic way of testing behavior of the application, and detect bugs in the program from the point of view of networking. So as I said, there is a possibility of state space explosion because of the combinatorial explosion. If you simply use a brute force approach, that will result in a combinatorial explosion because you have a huge space of data packets, a huge space of control events, and so the magic sauce that makes Nice work is the fact that first of all, they are doing the state-space exploration using model checking. That's one aspect of it. More importantly, they're using symbolic execution. This is where they bring in the application knowledge in order to do symbolic execution with the model checking so that you can prevent the explosion of state-space. So the input to this Nice tool is going to be your unmodified open flow program. Because that gives you the ability to do symbolic execution in the context of anything that you want to study, and the network topology that is assumed, and the correctness properties that you assume with respect to this particular program on the flow of packets. So using all of these three inputs, we can actually reduce the state-space that you want to search for. Otherwise, it's going to be a state space explosion. But the fact that you can use the equivalence class of packets and the control events that happened in the program, that is guided by the knowledge about the application behavior, all of this helps in reducing the state-space. So from this reduced state-space, then you can apply this correction properties and ask the question, "Are there any violation of the correctness properties that we have set for this particular program?" When we talk about system state, what are the things we're talking about, what is the state of the switch, and what is the routing rules that are being applied, what are the end hosts that are communicating, and what are the communication channels, TCP/IP channels, and UDP channels and so on? What are the communication channels that have been used in that particular application? All of this together is what a system state is, and that system state combinatorial explosion is being reduced by taking advantage of the application properties so that you can do symbolic execution, and the network topology where you can reduce the number of network events that you want to search on, and apply the correctness properties to know what kind of violations may come aboard. So that's sort of the tool that's available as an open source tool, which you can use if that is something that would help in analyzing your application behavior. Correctness properties could be first-in-first, first-out, if you have a flow and you say that this particular flow precedes another flow. These are correctness properties that you may have, already we have multiple agents working on something. You can say that this particular set of network packets should arrive before this, at a switch, and so on. So these are things that you can have as correctness properties, and sort of axions that you can use in order to explore whether the state space applied to state-space and ask the question, "Are any of these correctness properties being violated?" That violation can be the output of the Nice tool.
