Talk

The precise semantics of floating-point arithmetic programs depends on the execution platform, including the compiler and the target hardware. Platform dependencies are particularly pronounced for arithmetic-intensive scientific numeric programs and infringe on the highly desirable goal of software portability (which is in fact promised by heterogeneous computing frameworks like OpenCL): the same program run on the same inputs on different platforms can produce different results. So far so bad.

Serious doubts on the portability of numeric applications arise when these differences are behavioral, i.e. when they lead to changes in the control flow of a program. In this work I will present an algorithm that takes a numeric procedure and determines an input that is likely to lead to different decisions depending merely on how the arithmetic in the procedure is compiled. Our implementation of the algorithm requires minimal intervention by the user. I will illustrate its operation on examples characteristic of scientific numeric computing, where control flow divergence actually occurs across different execution platforms.

Time permitting, I will also sketch how to prove the /absence/ of inputs that may lead to control flow divergence, i.e. how to prove programs /stable/ (in one of the many senses of this word). This is ongoing work.

Thomas Wahl is an Assistant Professor at Northeastern University. This is joint work with Yijia Gu, Mahsa Bayati, and Miriam Leeser at Northeastern.

In the past few years, high-level programming languages have played a key role in several networking platforms, by providing abstractions that streamline application development. Unfortunately, current compilers can take tens of minutes to generate forwarding state for even relatively small networks. This forces programmers to either work around performance issues or revert to using lower-level APIs.

In this talk, we first present a new compiler for NetKAT (a network programming language) that is two orders of magnitude faster than existing systems. Our key insight is a new intermediate representation based on a variant of binary decision diagrams that can represent network programs compactly and supports fast, algebraic manipulation. We argue that our compiler scales to large networks using a diverse set of benchmarks.

In addition to speed, our new intermediate representation lets us build a powerful new abstraction for network programming. Existing languages provide constructs for programming individual switches, which forces programmers to specify whole-network behavior on a switch-by-switch basis. For the first time, we can compile programs that syntactically represent sets of end-to-end paths through the network.  To do so, our compiler automatically inserts stateful operations (e.g., VLAN tagging) to distinguish overlapping paths from each other.

Finally, we present a very general implementation of network virtualization that leverages our ability to compile end-to-end paths.  The key insight is to give packets two locations--physical and virtual--and synthesize a program that moves packets along physical paths to account for hops in the virtual network. We show that different synthesis strategies can be used to implement global requirements, such as shortest paths, load-balancing, and so on.

Arjun Guha is an assistant professor of Computer Science at UMass Amherst. He enjoys tackling problems in systems using the tools and principles of programming languages. Apart from network programming, he has worked on Web security and system configuration languages. He received a PhD in Computer Science from Brown University in 2012 and a BA in Computer Science from Grinnell College in 2006.

Programming Languages Seminar

Concurrent programming is the art of coordinating multiple processes into a single program, and is a pervasive part of practical programming.  It's also hard to do well, in part because good abstractions for concurrent programming are hard to come by.

This talk discusses Async, a concurrent programming library for OCaml, a statically typed functional language in the ML family. We'll discuss how Async compares to other approaches to concurrent programming, and how we leverage OCaml's type system to build high-quality abstractions for concurrency, without modification to the underlying language.

We'll also discuss how our approach to concurrent programming has   evolved over the last decade, and what aspects of the API have   turned out to be problematic.

In this talk I will discuss research advances that led to practical tools for automatically proving program termination and related properties, e.g. liveness. Practical applications include automatically proving device driver correctness, and pharmaceutical research. 

Byron Cook is Professor of Computer Science at University College London.  Byron is also a Senior Principal at Amazon.  See http://www0.cs.ucl.ac.uk/staff/b.cook/ for more information.

In this talk we give a survey of solutions -- and especially, discuss the underlying design principles -- that we developed in recent years to achieve extremely high packet processing rates in commodity operating systems, for both bare metal and virtual machines.

By using simple abstractions, and resisting the temptation to design systems around performant but constraining assumptions, we have been able to build a very flexible framework that addresses the speed and latency communication requirements of both bare metal and virtual machines up to the 100 Gbit/s range. Our goal is not to provide the fastest framework in the universe, but one that is easy to use and rich of features (and still, amazingly fast), to taking away concerns on the dataplane's speed from (reasonable) network applications.

Our NETMAP framework, opensource and BSD licensed, runs on 3 OSes (FreeBSD, Linux, Windows); provides access to NICs, host stack, virtual switches and point-to-point channels (netmap pipes), running between 20 and over 100Mpps on software ports, and saturating NICs with just a single core (reported up to 45 Mpps on recent 40G nics); achieves bare-metal speed on VMs thanks to a virtual passthrough mode (available for Qemu and bhyve); and can be used with no modifications by libpcap clients.

Luigi Rizzo is an associate professor at the Universita` di Pisa. He has worked on network emulation, high performance networking, packet scheduling, multicast and reliable multicast.  He is a long time contributor to FreeBSD, for which he has developed several subsystems including the dummynet network emulator, the ipfw firewall, and the netmap framework.  He has been program committe member for for sigcomm, conext, infocom, nsdi, Usenix ATC, ANCS and other conferences, as well as PC chair for Sigcomm 2009 and Conext 2014, ANCS 2016, and general chair for Sigcomm 2006. Luigi has been a frequent visiting researcher at various institutions including ICSI/UC Berkeley, Google Mountain View, Intel Research Cambridge, Intel Research Berkeley.

There is much interest recently in doing automated performance diagnosis on user laptops or desktops. One interesting aspect of performance diagnosis that has received little attention is the user perspective on performance. To conduct research on both end-host performance diagnosis and user perception of network and application performance, we designed an end-host data collection tool, called HostView. HostView not only collects network, application and machine level data, but also gathers feedback directly from users. User feedback is obtained via two mechanisms, a system-triggered questionnaire and a user-triggered feedback form, that for example asks users to rate the performance of their network and applications. This talk will describe our experience with the first deployment of HostView. Using data from 40 users, we articulate the challenges in this line of research, and report on initial findings in correlating user data to system-level data. We then describe our more recent efforts in conducting an in-depth study with twelve users in France to guide our design of the next version of HostView and of methods to infer user context and activities.

This is joint work with Diana Joumblatt, Jaideep Chandrashekar, Nina Taft, Anna-Kaisa Pietilainen, George Rosca, Peter Tolmie, Tom Rodden, Tom Lodge, Richard Motier. This work is funded in part by the EU FP7 User-Centric Networking project, Grant No. 611001.

Renata Teixeira received the Ph.D. degree in computer science from the University of California, San Diego, in 2005. During her Ph.D. studies, she worked on Internet routing at the AT&T Research. She was a researcher with the Centre National de la Recherche Scientifique (CNRS) at LIP6, UPMC Sorbonne Universites, Paris, France from 2006 to 2013. She joined Inria Paris-Rocquencourt as senior researcher in October 2013. She was a visiting scholar at UC Berkeyley/ICSI in 2011. Her research interests are in measurement, analysis, and management of data networks. She has authored more than 60 papers in this area. Renata is vice-chair of ACM SIGCOMM. She is a member of the steering committee of the ACM Internet Measurement Conference and has been active in the program committees of ACM SIGCOMM, ACM IMC, ACM CoNEXT, PAM, IEEE INFOCOM, among others.
 

Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code.  Further, mistakes are often hunted down using rudimentary tools such as Ping and Traceroute.

Taking our cue from other fields such as hardware design, we suggest fresh approaches.   Our first attempt was a geometric model of network forwarding called Header Space together with parsers that convert router configurations to header space representations.  Header Space ideas were used to build a static checker (Hassel) that can identify reachability bugs and a dynamic checker (ATPG) that can identify performance faults.  Unlike classical model checkers, Hassel does not have a notion of a specification language or a modeling language, which makes it difficult to write higher level specifications or deal with changing router behaviors.  Our attempt to remedy this was to teach an old dog (Datalog) new tricks to create what we call Network Optimized Datalog (NoD) followed by extensions to quantitative  and automatic verification.    

These results suggest that concepts from Electronic Design Automation (EDA) and program verification can be leveraged to create what might be termed Network Design Automation (NDA).   What might the equivalent of Layout Versus Schematic tools or Specification Mining be?  What are the differences in the domain that can be exploited? The second part of this talk will explore this vision, touching upon modular network semantics, language design, performance invariants, and interactive network debuggers.  This is joint work with collaborators at Berkeley, MSR, and Stanford.

George Varghese received his Ph.D. in 1992 from MIT.  From 1993-1999, he was a professor at Washington University, and at UCSD from 1999 to 2013. He was the Distinguished Visitor in the computer science department at Stanford University from 2010-2011.  He joined Microsoft Research in 2012.  

His book "Network Algorithmics" was published in December 2004 by Morgan-Kaufman. In May 2004, he co-founded NetSift, which was acquired by Cisco Systems in 2005. With colleagues, he has won best paper awards at SIGCOMM (2014), ANCS (2013), OSDI (2008), PODC (1996), and the IETF Applied Networking Prize (2013).  He won the Kobayashi Award and the SIGCOMM Lifetime Award, both in 2014, and the IIT Bombay Distinguished Alumni Award in 2015.

This talk aims to accessibly introduce a new theory of network architecture relevant to biology, medicine and technology (particularly SDN/NFV and cyberphysical systems), initially minimizing math details. Key ideas are motivated by familiar examples from neuroscience, including live demos using audience brains, and further illustrated with examples from technology and biology. The status of the necessary math will be sketched in as much detail as time permits. Background material is in online videos (accessible from website above) and a recent blog post: rigorandrelevance.wordpress.com/author/doyleatcaltech.  My research is aimed at developing a more “unified” theory for complex networks motivated by and drawing lessons from neuroscience[4], cell biology[3], medical physiology[9], technology (internet, smartgrid, sustainable infrastructure)[1][8], and multiscale physics [2],[5],[6]. This theory involves several elements: hard limits, tradeoffs, and constraints on achievable robust, efficient performance ( “laws”), the organizing principles that succeed or fail in achieving them (“architectures” and protocols), the resulting high variability data and “robust yet fragile” behavior observed in real systems and case studies (behavior, data, statistics), the processes by which systems adapt and evolve (variation, selection, design), and their unavoidable fragilities (hijacking, parasites, predation, zombies).  We will leverage a series of case studies with live demos from neuroscience, particularly vision and sensorimotor control, plus some hopefully familiar and simple insights from medicine, cell biology and modern computer and networking technology.  Zombies emerge throughout as a ubiquitous, strangely popular, and annoying system fragility, particularly in the form of zombie science.  In addition to the above mentioned blog and videos, papers [1] and [4] (and references therein) are the most accessible and broad introduction while the other papers give more domain specific details.  For math details the best place to start is Nikolai Matni’s website (cds.caltech.edu/~nmatni/).

Selected recent references:
[1]        Alderson DL, Doyle JC (2010) Contrasting views of complexity and their implications for network-centric infrastructures. IEEE Trans Systems Man Cybernetics—Part A: Syst Humans 40:839-852.
[2]        Sandberg H, Delvenne JC, Doyle JC. On Lossless Approximations, the Fluctuation-Dissipation Theorem, and Limitations of Measurements, IEEE Trans Auto Control, Feb 2011
[3]        Chandra F, Buzi G, Doyle JC (2011) Glycolytic oscillations and limits on robust efficiency. Science, Vol 333, pp 187-192.
[4]        Doyle JC, Csete ME(2011) Architecture, Constraints, and Behavior, P Natl Acad Sci USA, vol. 108, Sup 3 15624-15630
[5]        Gayme DF, McKeon BJ, Bamieh B, Papachristodoulou P, Doyle JC (2011) Amplification and Nonlinear Mechanisms in Plane Couette Flow, Physics of Fluids, V23, Issue 6, 065108
[6]        Page, M. T., D. Alderson, and J. Doyle (2011), The magnitude distribution of earthquakes near Southern California faults, J. Geophys. Res., 116, B12309, doi:10.1029/2010JB007933.
[7]        Namas R, Zamora R, An, G, Doyle, J et al, (2012) Sepsis: Something old, something new, and a systems view, Journal Of Critical Care  Volume: 27   Issue: 3
[8]        Chen, L; Ho, T; Chiang, M, Low S; Doyle J,(2012) Congestion Control for Multicast Flows With Network Coding, IEEE Trans On Information Theory  Volume: 58   Issue: 9   Pages: 5908-5921
[9]        Li, Cruz, Chien, Sojoudi, Recht, Stone, Csete, Bahmiller, Doyle (2014)   Robust efficiency

John Doyle is the Jean-Lou Chameau Professor of Control and Dynamical Systems, Electrical Engineer, and BioEngineering at Caltech (BS&MS EE, MIT (1977), PhD, Math, UC Berkeley (1984)). Research is on mathematical foundations for complex networks with applications in biology, technology, medicine, ecology, and neuroscience. Paper prizes include IEEE Baker and Automatic Control Transactions (twice), ACM Sigcomm, AACC American Control Conference. Individual awards include IEEE Power Hickernell, AACC Eckman, UCB Friedman, IEEE Centennial Outstanding Young Engineer, and IEEE Control Systems Field Award.  Best known for fabulous friends, colleagues, and students, plus national and world records and championships in various sports.  Extremely fragile.