In 30 seconds
Nate Foster, an EPFL professor and Jane Street visiting researcher, joins Ron Minsky to discuss the intersection of programming languages and networking. They trace the promise and limits of software-defined networks, programmable hardware, multicast, and new pressures from machine-learning workloads. Foster describes Butane, Jane Street’s system for compiling high-level network policies to distributed BGP configurations, and explains how models support testing, exploration and capacity planning.
- 1A network-wide programSoftware-defined networking replaces individual device configuration with higher-level descriptions that can be composed and analyzed.
- 2NetKAT and mathematical structureA forwarding language connects networking to Kleene algebra with tests, supporting compilers and verification.
- 3Why multicast still mattersTrading networks use multicast to distribute market data efficiently to many consumers, despite uneven support in cloud environments.
- 4Machine learning changes the workloadRegular training communication may make scheduled switching attractive, while idle GPUs make network delays costly.
- 5Butane and BGPA reviewed high-level policy compiles into BGP configurations, combining centralized intent with distributed responses.
- 6Models for explorationModels of policies and BGP can predict changes and support capacity planning; automated search for new configurations remains research.
Takeaways
- A network-wide program can express policies, support software review and help engineers reason about behavior before deployment.
- Mathematical models such as NetKAT provide tools for reasoning about forwarding, but real networks also contain failures and interactions beyond any single snapshot.
- Programmable hardware creates opportunities for in-network computing while raising questions about which functions belong in the network.
- Multicast remains useful for trading workloads even though its support has diminished relative to other network capabilities.
- A centralized policy can compile to distributed BGP configurations that react quickly to network changes.
- Formal models can enable exploration and capacity planning as well as detect errors, provided they faithfully represent real implementations.
- Simple abstractions that map clearly to router configurations can make operational behavior easier to understand.
Read the edited text by chapter
From physics to programming languages
Foster recounts his path through Java generics and bidirectional lenses. A postdoctoral move brought him into networking.
Ron Minsky introduces Nate Foster, an EPFL professor and Jane Street visiting researcher whose work connects programming languages and networking. Foster spends a day a week with the networking team.
Foster began college studying physics but found himself increasingly drawn to computer science. He liked seeing how a program could be followed through a compiler, instruction set and chip down to logic gates, and appreciated that computing abstractions such as lambda calculus are human creations constrained by mathematics and physical implementation.
His first research experience came from a summer project on a Java compiler with Kim Bruce. Java had brought garbage collection and a largely sound static type system into widespread use; the project explored adding polymorphism, before Java had generics.
Bruce's proposal was one of several competing designs. The generics eventually adopted grew out of GJ, by Philip Wadler and Martin Odersky. Foster notes that type systems can look simple while hiding subtle soundness or performance problems, so drawing on the research community was valuable.
After time in England, Foster pursued a PhD at Penn with Benjamin Pierce. He expected to work on type systems or semantics, but Pierce suggested a data synchronization project related to the OCaml file synchronizer Unison. Foster was initially disappointed that it sounded like a systems problem.
The project contained an elegant programming-languages problem: synchronizing different representations, such as calendar data in iCal and XML, requires conversions in both directions. Those functions are closely related, so the researchers developed a single abstraction, the lens, from which both directions could be derived.
Lenses had predecessors in database and functional programming research, but Pierce and Alan Schmitt's formulation attracted attention for its clarity. Foster studied variants, their expressiveness, and laws ensuring that changes propagated between representations accurately. Later Haskell work generalized the idea to other structures.
After his PhD, Foster accepted a faculty position at Cornell but first spent a year at Princeton with David Walker and Jennifer Rexford. He wanted a new problem after six years on lenses, and the group took a chance on a programming-languages researcher with little networking background.
The network as a program
Software-defined networking offers higher-level composition, isolation and reasoning across a network. NetKAT connects forwarding behavior to established mathematical theory.
Foster has since spent roughly 15 years at the intersection of programming languages and networks. Software-defined networking emerged as large technology companies needed more freedom to change their networks and struggled with the complexity of protocols and control algorithms across enormous data centers.
The idea is to describe network behavior in software at a higher level than individual hardware permits. A language can help engineers compose functions, isolate parts that must not interact, and reason about the possible behaviors of the whole network.
Minsky contrasts that with configuring each individual switch after designing and wiring a network. A network-wide program can enable faster iteration and make it easier to predict whether properties hold. Physical design still matters, and network programs have special constraints: allocating memory for every packet at every hop would be impractical.
Networks also require isolation between components and often distributed control among different teams. Minsky compares the problem to hardware synthesis: both need languages for a large graph-like system, but the domain places strong limits on what the generated implementation can do.
Foster's group developed NetKAT, a language for describing packet forwarding, not end-host behavior, TCP, or the control plane that selects routes. They discovered that their designs aligned with Kleene algebra with tests, an existing mathematical framework for imperative programs associated with Dexter Kozen.
That connection links seemingly peculiar network operations to familiar ideas such as finite automata and state machines. Minsky observes that a simple mathematical foundation can make language features generalize and compose more naturally. For Foster, it also supplied constructions for compilers and verification tools.
The group extended NetKAT with probabilities to reason about uncertain traffic, failures and randomized load balancing. Working out the semantics was subtle; Foster says the existing algebraic structure helped prevent the extended language from becoming incoherent.
Foster's slogan is that the network should be treated as another program. Historically, new capabilities often depended on a hardware vendor adding features or a standards body agreeing on a protocol. He wants the freedom to deploy new behavior on networking hardware more like writing a new program on a processor.
Minsky notes that this freedom is easier inside a large network controlled by one organization than across independent networks. Foster agrees: standards and vendors made the Internet interoperable across tens of thousands of autonomous systems, while a large private network can pursue its own objectives within its boundaries.
Applying the same approach to the open Internet is difficult because its success makes it hard to change. There is no practical day on which every autonomous system can be switched to a new protocol. Researchers have long explored architectures that would make the Internet more extensible and evolvable.
Software practices and verification
The vision has influenced practice without all of its original predictions coming true. Version control, testing and formal analysis help engineers manage changes and their consequences.
Foster thinks the network-as-program idea has become commonplace. A vision paper he wrote with collaborators was rejected partly because reviewers considered its premise already established. But particular predictions did not all come true: fully centralized control and completely programmable routers have not been adopted in the original form.
Minsky adds that software culture itself is valuable: version control, code review and testing can be applied to networking when configuration has a central representation. Foster agrees that this is broader than formal verification and notes that large ISPs were already exploring centralized specifications in the 1990s.
A representation of network configuration can also be tested or verified before deployment. For instance, an engineer can check whether a proposed route change breaks connectivity elsewhere. These checks matter because unexpected effects of configuration changes have caused major outages.
Verification is not finished, Foster cautions. Networks are distributed systems with failures, interacting control loops and components that may not be represented accurately in a model. A check over a snapshot does not capture every dynamic interaction or eliminate human error.
One practical success is reasoning about a forwarding-plane snapshot using model checkers, SAT solvers or tools such as NetKAT. Engineers can check whether two hosts remain connected or whether systems meant to be isolated have an unwanted path. Such tools catch errors and can give engineers confidence to make changes.
Rejecting a change that violates a property is not always sufficient. If a controller proposed it in response to a failure, rejecting it without a better alternative can leave the original failure unresolved. The challenge is to reason about both the desired property and the control system's response.
Programmable hardware and in-network computing
Foster describes P4, Barefoot Networks and the opportunities and controversy around computation in switches. Minsky explains why multicast matters for trading.
Foster values the networking research community's close mix of academics, cloud operators and switch vendors. People who study theory and people who build large backbones exchange ideas, sometimes moving research into practice quickly. Programming-language advances have often taken much longer, though connections are growing there too.
He helped develop P4, a language for specifying the behavior of switches and network interfaces. OpenFlow had modeled a router roughly as one large lookup table; real high-speed devices have complex pipelines of specialized units. P4 exposed more of that pipeline structure while allowing its behavior to be customized.
During a Cornell sabbatical, Foster joined Barefoot Networks, which was developing programmable switches. He wanted to understand routers and hardware at a deeper level. Working with chip-design experts taught him how many specialties, from circuit design to physical layout and fabrication, go into a device.
At Barefoot, colleague Chang Kim saw that a programmable router chip could act as a specialized processor with limited memory and state but very high throughput. A packet crossing a data center might encounter several such processors. That led to work on what computation could be placed inside the network.
The harder and more controversial question is what computation should be there. The end-to-end principle cautions against putting functions in the network that benefit only some users while imposing costs on everyone. Foster nevertheless sees uses for in-network computing, including observation, caching and certain consensus-related functions, depending on context.
Minsky says Jane Street also accelerates selected operations at network choke points for monitoring, filtering and traffic shaping. One especially important workload is multicast, which exchanges use to distribute market data to many recipients.
Multicast copies packets along a distribution tree, but it did not become the general video-delivery mechanism once anticipated. Minsky argues that bandwidth became cheap while control-plane state for many separate trees remained expensive. A trading network has relatively few channels that must reach many consumers, making the technique more useful there.
Cloud services may offer multicast-like interfaces primarily for legacy applications, he says, without the performance characteristics trading workloads need. Foster welcomes the opportunity to revisit predictions that did not work out: research communities need room to try ideas that may never become the prevailing design.
Research bets and finance-specific networks
The pair discuss learning from ideas that do not catch on and the distinctive latency and multicast requirements of financial infrastructure.
Foster points to the Nines networking conference, which encourages new ideas, and to Scott Shenker's reflection on what he got wrong about quality of service. Principles such as end-to-end design are useful, but treating them as rules that can never be revisited risks stagnation.
Minsky says Jane Street's growth has allowed it to make longer-term bets alongside incremental improvements. Academic research can take that even further, exploring ideas that may take decades to bear fruit. Foster had known Jane Street through functional programming and was attracted by its technical ambition and openness to new approaches.
Jane Street's network had grown large enough to benefit from top-down specification and tools for making changes with confidence. Foster was also curious about finance-specific constraints: multicast and very low latency can lead to different solutions from those designed for hyperscalers.
Minsky observes that research can be shaped by the dominant industrial problem of the moment. He gives garbage collection as an example: for years Java's assumptions influenced much of the literature, even though other languages and workloads call for different tuning choices.
Foster describes a paper on multicast in trading networks. Commodity routers have gained bandwidth and features, but more elaborate pipelines can add latency, while multicast support has not necessarily grown at the same pace. The paper explores alternatives such as optical networks and circuit switching, including trade-offs between broad delivery and filtering.
Minsky wonders whether multicast is underused elsewhere, for example in distributing streams of updates or implementing state-machine replication. Within a system it can act as an efficient bus; exchanges also use it to distribute market data fairly across organizational boundaries.
Packet switching and machine learning
Regular training workloads could benefit from scheduled or hybrid network designs. GPU synchronization raises the cost of communication delays.
Foster considers whether packet switching should always be the default. It efficiently shares resources among unpredictable flows, but routers must contend with simultaneous requests for the same output. That dynamic arbitration adds complexity to the high-speed switching fabric.
A paper by Nick McKeown and Sundar examines regular machine-learning training workloads. If communication schedules and permutations are predictable, a scheduled switch might be simpler, cheaper and faster than a general packet switch. Foster sees a possible future for hybrid designs, while acknowledging the efficiency and flexibility packet switching provides.
Minsky notes that training synchronizes expensive GPUs: uncovered communication time can leave them idle. The resulting demand for throughput and low latency, along with different scale-up and scale-out networks, creates an opportunity to rethink designs. Foster sees active experimentation in transport protocols, collective operations and co-optimization with GPU code.
BGP and Butane
BGP distributes routing knowledge and reacts to changes. Butane compiles reviewed network-wide policies into router configurations and supports analysis of their effects.
The conversation turns to BGP, the Border Gateway Protocol. Jane Street's growing wide-area network was still expressed through configurations for individual routers. BGP was designed to connect autonomous systems on the Internet, with each system deciding how to route traffic and sharing selected reachability information with neighbors.
A router can advertise that it knows a path to a destination, along with attributes such as cost or tags. Recipients compare advertisements and make local choices. The protocol is distributed, but those local choices collectively produce routes across the network.
Why does this decentralized system often converge? Foster points to work by Lixin Gao and Jennifer Rexford showing that properties of Internet business relationships and routing preferences help explain its stability. BGP can also be used within an organization, where routers must learn internal and external paths and respond to failures.
BGP is expressive, widely supported and familiar to network engineers. Foster says a weakness of an early SDN vision was assuming that a single high-level objective must yield a centralized implementation. Distributed protocols can react quickly to failures without requiring global coordination.
Jane Street's system, Butane, combines these ideas. Engineers maintain a high-level specification in a repository, review changes as software, and compile it into BGP configuration for each router. The routers then exchange messages and collectively arrive at forwarding behavior.
The policy distinguishes traffic that needs the fastest available path from traffic that merely needs to arrive. It also reflects the firm's network structure, sites and traffic classifications. Engineers can change a concise policy rather than manually edit configurations across several routers.
Foster says the value is not a single spectacular algorithm but a software-oriented workflow. The compiler generates BGP configuration, tools validate and visualize changes, and the result is deployed. Network engineers have particularly appreciated the ability to see the expected consequences before making a change.
A model using historical measurements and the semantics of Butane and BGP can estimate changes such as latency between sites. The team is exploring more powerful what-if questions: what happens if links fail, or what configuration changes would relieve a hotspot while minimizing disruption?
Foster emphasizes that automatically finding such changes remains research. It resembles program synthesis or solver-based exploration of configurations. Confidence depends on a model that has been checked mathematically and against actual vendor hardware, whose implementation must match the assumed BGP semantics.
Models, rollout and future research
Formal models support exploration and capacity planning, while production rollout demands substantial operational work. Foster closes with research into composable routing algebras.
Formal methods do more than act as a seat belt against mistakes, Foster argues. A trusted model can let engineers explore larger changes and compare their consequences. Minsky describes this as a kind of observability into possible network designs, subject to the accuracy of the model.
The team has also begun using the model for capacity planning: given traffic demand, historical workloads and available fiber, engineers can consider which future links to buy. The same model can help with both today's routes and tomorrow's network expansion.
Butane drew on academic work, including a formal semantics for BGP by researchers including Zachary Tatlock. The team chose relatively simple policy abstractions that compile straightforwardly to vendor configurations, rather than a more expressive language that would hide more of the mapping.
Foster initially found the modest design less exciting, but now thinks it was right for the context. Engineers can peel back the abstraction and see how it maps to BGP. Minsky agrees that straightforward compilation makes behavior easier to understand even when more sophisticated optimization could be valuable.
As a visiting researcher, Foster has usually spent one day a week at Jane Street, working alongside network engineers and tooling specialists to design and prototype the system. He values the speed and expertise of the engineers and the feedback that comes from working on a real operational problem.
Production rollout required much more than a working prototype. The team tested repeatedly, including in a lab and on new infrastructure not yet carrying production use, before a broader rollout. Operations work included router firmware upgrades and integration with the firm's deployment workflows.
Jane Street's homegrown tools gave the team access to the engineers building its deployment infrastructure. Foster says this made it possible to add capabilities needed by the project. Minsky notes that the firm's distinctive software ecosystem creates both pain points and considerable control over the stack.
Foster enjoys the visiting role partly because it gives him time to write code alongside his academic responsibilities. The work has also informed his lab: the original Butane and BGP semantics used an operational simulator, while his students are exploring a more algebraic model of routing.
Tim Griffin's work on metarouting proposes general building blocks for policy languages. Organizations differ in how they choose paths and what information they share, so a single policy language may not fit everyone. BGP could serve as a lower-level target for several different policy languages.
A routing algebra abstracts information exchanged with peers and choices made among received routes. Algebras concerned with latency and bandwidth, for example, can be composed into a richer policy with a defined preference between them. This provides a way to construct domain-specific languages from reusable pieces.
The theory also asks when a routing system converges. BGP configurations can oscillate as one party's preferred path causes another to change its choice; algebraic conditions can help characterize when a stable solution is guaranteed. Foster's lab is revisiting these ideas.
The broader ambition is a high-level network program implemented through a distributed protocol such as BGP. Foster suggests routing algebras might eventually help Jane Street reason about richer Butane policies, although the existing policy abstraction deliberately began with modest goals.
More from this channel
1:34:29EN
15:48EN
1:20:57EN
1:12:58EN
58:47EN
3:13EN