I received my Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign where I worked with Brighten Godfrey. I have also worked as a research collaborator, a research associate, and an intern at Microsoft Research, Princeton University, UW-Madison, and Max Planck Institute.
I design and build reliable networked systems with provable guarantees, drawing techniques from formal methods, distributed systems, and control theory. My research has been awarded the VMware Fellowship (one of the three winners worldwide, 2015), the HotSDN best paper award, the Feng Chen Memorial Award, the Gottlieb Fellowship, and the Wolfond Fellowship.
I have joined the Johns Hopkins University as an assistant professor and I'm looking for students!
Microbursts, the main culprit of packet loss in datacenters, last for a few microseconds -- a time period orders of magnitude shorter than the control loop of fastest existing load balancers.
We design DRILL, a datacenter fabric that performs micro load balancing to distribute load despite microbursts via employing per-packet decisions based on queue occupancies and randomized algorithms.
Our design addresses the resulting key challenges of packet reordering and topological asymmetry. DRILL outperforms the state of the art load balancers especially for bursty workloads, e.g., it results in 2.1x improvement in the average flow completion time in an incast scenario compared to CONGA.
Naively scaling networks can cause incorrect behaviors, e.g., we show that scaled-out firewalls erroneously and permanently block hosts. We design and build COCONUT, a system that leverages vector clocks for efficient seamless network scale-out of networks.
We show that the state distribution techniques in existing network virtualization systems can cause incorrect application-level behavior. We also show that that the incorrect behaviors occur while the pervasive correctness invariants are preserved throughout, and that the techniques designed to preserve such invariants can themselves occasionally break the otherwise correct behavior.
Modern networks rely on a variety of stateful network functions to implement rich policies. Correct operation of such networks relies on ensuring that they support a diverse set of properties including liveness properties. Unfortunately, despite exciting recent work on network verification, no existing approach is practical for, or applicable to, validating liveness.
We develop novel encodings of the behavior of network programs under dynamic events such as network state changes using Boolean formulas that can capture rich semantics such as packet counters. We prove that our encodings are equivalent to the program and show experimentally that they can succinctly express a variety of network functions and are orders of magnitude more scalable to verify than naive encodings.