A team of Cornell computer science researchers—including associate professor Nate Foster; Eric Hayden Campbell, a fourth-year Ph.D. student and 2019 NSF Graduate Research Fellow; and Hossein Hojjat, a former postdoctoral student with Foster—presented new research on Avenir, a synthesis engine for software defined networks (SDNs), at USENIX NSDI ’21, the Symposium on Networked Systems Design and Implementation. Their paper—“Avenir: Managing Data Plane Diversity with Control Plane Synthesis”—is the result of a collaboration with Infosys, in particular, Vignesh Ramamurthy and Kalicharan Vuppala.
CS News reached out to the researchers for further details on their findings, including what motivated the research, the project description, how the academic/industry collaboration was achieved, and applications of the findings. Eric Hayden Campbell, the paper’s lead author, represented the Cornell group, while Vignesh Ramamurthy reflected on how Infosys became involved.
CS News: Let’s start with some basics. You describe Avenir as “an engine for automatically managing switch diversity in a software defined network.” Can you say more about how an SDN functions?
Eric Hayden Campbell for the Avenir Team: Sure thing. In a software defined network (SDN), a network operating system manages network resources much like a traditional operating system manages computing resources. Critically, network OSes have to support many hardware devices (switches, routers, etc), which means writing new code to manage each new kind of hardware; these programs are called drivers. The main difference between drivers in a traditional OS (say to manage a fancy GPU) and SDN drivers is that the network engineers (rather than the hardware vendors) have to write the drivers themselves (imagine having to write a Java program before using your new gaming keyboard!). This isn’t an easy task even for well-trained professional software engineers; it has taken up to two years to develop these drivers for new hardware!
CS News: And this is the point where Avenir makes its debut?
Campbell: Precisely. Avenir essentially eliminates the need to write drivers. Using a powerful formal methods technique called program synthesis, Avenir automatically computes switch configurations from an abstract representation. As an added bonus, Avenir automatically verifies the correctness of the switch configuration using an automated solver. In fact, this verification is part of Avenir’s core algorithm, which continually tweaks its solution until the solver certifies its correctness.
CS News: What, then, are some specific uses for Avenir, or, at least, ones you’ve identified thus far?
Campbell: Avenir is particularly suited to networks whose switches are programmed using the P4 programming language, because it computes the logical formulae necessary to certify correctness directly from the program itself, using classic techniques developed by Dijkstra in the 1970s. It’s true that for non-programmable (i.e. fixed-function) switches engineers would need to write down an imperative specification of the switch’s pipeline in a language like P4, which is certainly not a trivial task. Using Avenir in this setting is less automatic, but still provides the clear benefit of formal verification.
CS News: We’d like to learn more about the timeline of your research and some specifics about your successful collaboration. The research team from Cornell worked closely with Vignesh Ramamurthy and Kalicharan Vuppala at Infosys. How did this collaboration come about?
Campbell: Our collaboration with Infosys started in the spring of 2019, when we had many back-and forth conversations with Vignesh and Kalicharan to understand the nature of the problems they were having with ONOS. They were using a large segment-routing abstraction supported by Trellis and wanted to translate this logic across various hardware switches. These conversations were essential to situate our academic research problem in a real industrial context. After a few months, we had developed a prototype that translated between segment-routing schemes and destination-based routing schemes.
CS News: Yet, you mentioned there were constraints that needed to be addressed?
Campbell: Yes, that’s right. Pretty soon it became clear that ONOS needed more flexibility, it needed to support many different kinds of switches, and ideally it would support many kinds of internal abstractions. Later, when Hossein Hojjat came to Cornell for a visiting appointment in the summer of 2019, he observed that our techniques were a special case of counterexample-guided inductive synthesis, and we worked quickly to generate a prototype implementation that worked on small examples. This shifted our problem formulation slightly: now we were automatically translating operations from an abstract switch to a target switch, which meant that engineers could write code against the abstract switch without worrying about the targets.
CS News: By this point—the winter of 2019 and into 2020—you were poised to run Avenir on real world data. How did you find a way to do this?
Campbell: We reached out to Infosys and their partner, the ONF, who provided us with real-world P4 programs and configurations from their testbed that we used to benchmark Avenir. With the help of these programs, after a few months, Avenir could perform efficiently on industrial-grade switch programs.
CS News: Aside from the excellent news of presenting your research at USENIX NSDI ’21, what’s the latest on the project?
Campbell: Currently, I am working with Andy Zhu, a Cornell M.Eng. student, to measure Avenir’s performance on some additional data from Infosys that will help us to even better understand the feasibility of integrating Avenir into ONOS.
CS News: Now, we’d like to turn to Vignesh Ramamurthy and Kalicharan Vuppala at Infosys for a few words. Vignesh, can you share a few notes from your perspective on the project and the collaboration with Cornell researchers?
Vignesh Ramamurthy of Infosys: Certainly. To start with, I believe that we are addressing a very critical problem that the Networking industry is facing. A consistent way of managing diversity of device types and merchant Silicon ASICs in Telecom networks is very essential today.
SDN and Network virtualization is a reality today across Communication Service Provider, Enterprise, and Cloud Networks. We have designed and built a carrier-grade Switching fabric based on Whitebox switches with merchant Silicon from Broadcom. The solution used a remote Network Operating System with a cluster of SDN controllers. One of the significant challenges was really understanding the mapping of the higher layers (like Broadcom OFDPA) to the underlying physical switching pipelines. This is critical for supporting new protocols and device types. The Avenir POC has demonstrated a novel way of developing and verifying these translations. As we move into a more hybrid Telecom Networks with a mix of traditional and SDN-driven solutions like Avenir are valuable for the industry.
It was a great experience collaborating with Nate, Eric, and the team where we brought in a number of real-life scenarios to shape the Avenir tool for industrial purposes. We believe that the tool has the potential to be integrated into mainstream SDN controller solutions.
CS News: Thank you all for generously sharing some of your research with the Cornell CS community.
- Eric Hayden Campbell, Cornell PhD Candidate, lead author of Avenir
- Nate Foster, associate professor of computer science
- Hossein Hojjat, professor at Tehran and TeIAS; Foster’s former postdoc
- Priya Srikumar, Cornell undergrad, worked on writing code for Avenir
- Andy Zhu, Cornell M.Eng. student working on applying Avenir
- Vignesh Ramamurthy
- Kalicharan Vuppala
- Andy Fingerhut, William T. Hallahan, Jed Liu, Ruzica Piskac, Robert Soulé, the Yale-Barefoot team working on P4 implementability
- Carmelo Cascone, Brian O’Connor, Charles Chan, Pier Luigi Ventre, engineers at the ONF who have been essential in positioning Avenir, and providing data to evaluate Avenir, and understanding the engineering considerations to integrate Avenir with ONOS