1st ACM SIGCOMM Workshop on Formal Methods Aided Network Operation (FMANO)

Brighten Godfrey is a Professor in the Department of Computer Science at the University of Illinois Urbana-Champaign. He co-founded and served as CTO of network verification pioneer Veriflow through its 2019 acquisition by VMware (now Broadcom), where he serves as a Technical Director. He received his Ph.D. at UC Berkeley in 2009, and his B.S. at Carnegie Mellon University in 2002. His research interests lie in the design of networked systems and algorithms. He has served as co-chair of ACM SIGCOMM 2022, SOSR 2016 and ACM HotNets 2014, and currently serves on the ACM SIGCOMM Steering Committee. He is a winner of the ACM SIGCOMM Rising Star Award, the Sloan Research Fellowship, and the National Science Foundation CAREER Award.

Abstract:

The field of network verification has achieved significant success in improving correctness of deployed networks. This success is due in part to the focused scope of network data and control planes, making the problem tractable. However, modern cloud infrastructure is evolving and broadening. Above the physical network, a rich ecosystem of virtual infrastructure helps support so-called “cloud native” applications, including cluster orchestrators, containers and microservices, service meshes, and their associated virtual network control and data planes. In this talk, we’ll explore new opportunities for formal methods to help the operations of these “networks above the network” — and how this domain presents new challenges characterized by dynamic closed-loop control, complex custom software elements, and closer association with applications.

Xiaoliang Wang a Professor at Fudan University. Before that, he was a visiting scholar of Microsoft Research and worked at the Tencent network platform department. He published multiple papers at SIGCOMM, NSDI, OSDI. His research focuses on distributed systems and cloud networks.

Abstract:

Corporations worldwide are investing heavily in the infrastructure for training large AI models. However, the service providers have met great challenges in the planning, construction, operation, and optimization of the ultra-large-scale AI clusters. In this talk, we report a performance model that organizes key elements of the LLM, and optimizes the deployment and operation of AI clusters. The performance model, called Astral-GOA (Tencent Astral AI Large Model Global Optimization Analysis System), has been applied in Tencent AI clusters for years to support large AI model training and inference. We provide case studies of Astral-GOA to verify its effectiveness for planning, problem localization, and optimization. We further demonstrate the operational experience and discuss the difference to the current modeling tools like NVIDIA Calculon, Astra-sim, etc. The overall design of Astral-GOA is useful to the community and raises new research problems. We hope to attract more practitioners and researchers to discuss and improve the tool together.

Ratul Mahajan is an Associate Professor at the University of Washington's Paul G. Allen School of Computer Science. He is also the co-director of UW FOCI (Future of Cloud Infrastructure) and an Amazon Scholar. In earlier lives, he was a Co-founder and CEO of Intentionet, a company that pioneered network verification, and a Principal Researcher at Microsoft Research. Ratul is a computer systems researcher with a networking focus and has worked on a broad range of topics, including network verification, connected homes, optical networks, Internet routing and measurements, and mobile systems. Many of the technologies that he has helped develop are part of real-world systems at Microsoft and other companies. Ratul has been recognized as an ACM Distinguished Scientist, an ACM SIGCOMM Rising Star, and a Microsoft Research Graduate Fellow. His papers have won the ACM SIGCOMM Test-of-Time Award, the IEEE William R. Bennett Prize, the ACM SIGCOMM Best Paper Awards (twice), the HVC Best Paper Award, and the IETF Applied Networking Research Prize.

Abstract:

In this talk, I will argue that methods to simplify network operations, be they based on synthesis, verification, or testing, must account for network evolution. Otherwise, the abstractions upon which these methods are built can go stale over time and even leave the network in a worse state than not having those abstractions in the first place. Using examples from my recent work, evolution-friendliness is not something that can be layered atop basic techniques, but it can require a ground up thinking that leads to methods of a different kind.