propane.tex

\documentclass[sigconf]{acmart}

% Disable / remove copyright boxes
\setcopyright{none}
\settopmatter{printacmref=false}
\renewcommand\footnotetextcopyrightpermission[1]{}

% Increase margin between text and footer
\setlength{\footskip}{20pt}

% Add CCR footer
\usepackage{fancyhdr}
\fancypagestyle{plain}{%
   \fancyhf{} %
   \fancyfoot[L]{ACM SIGCOMM Computer Communication Review}%
   \fancyfoot[R]{Volume 49 Issue 5, October 2019}%
}
\pagestyle{plain}

% Add CCR footer on first page
\fancypagestyle{firstpagestyle}{%
   \fancyhf{} %
   \fancyfoot[L]{ACM SIGCOMM Computer Communication Review}%
   \fancyfoot[R]{Volume 49 Issue 5, October 2019}%
}

% Add editorial note
\begin{teaserfigure}
	\parbox{\textwidth}{\centering\normalsize
		This article is an editorial note submitted to CCR. It has NOT been peer reviewed.\\
		The authors take full responsibility for this article's
		technical content. Comments can be posted through CCR Online.
	}
	\vspace{10pt}
\end{teaserfigure}


\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{url}
\usepackage{times}
\usepackage{xspace}
\usepackage{listings}
\usepackage{code}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,positioning}
\let\proof\relax
\let\endproof\relax
\usepackage{amsthm}
\usepackage{subcaption}
%\usepackage{geometry}

\usepackage{balance}

\usepackage{mathptmx}


% fix from https://latex.org/forum/viewtopic.php?t=27680
\newcommand*{\origrightarrow}{}
\let\oldarrow\textrightarrow
\renewcommand*{\textrightarrow}{\fontfamily{cmr}\selectfont\origrightarrow}


\definecolor{princetonorange}{RGB}{255,143,0}
\definecolor{tmlblue}{RGB}{0,58,120}  % tmlblue == Toronto Maple Leafs Blue!

\newcommand{\todo}[1]{\textcolor{red}{[TODO: #1]}}
\newcommand{\ratul}[1]{\textcolor{blue}{[ratul: #1]}}
\newcommand{\ryan}[1]{\textcolor{green}{[ryan: #1]}}
\newcommand{\dpw}[1]{\textcolor{tmlblue}{[dpw: #1]}}
\newcommand{\todd}[1]{\textcolor{princetonorange}{[todd: #1]}}

\newcommand{\EG}{\emph{e.g.}}
\newcommand{\IE}{\emph{i.e.}}
\newcommand{\ETC}{\emph{etc.}}
\newcommand{\ETAL}{\emph{et al.}}

\newcommand{\sysname}{{\small \sf Propane}\xspace}

\newcommand{\para}[1]{\paragraph*{\textbf{#1}}}

\newcommand{\set}[1]{\ensuremath{\{ #1 \} }}
\newcommand{\abs}[1]{\ensuremath{ \lvert #1 \rvert }}

\newcommand{\CD}[1]{\texttt{\small #1}}  % code font
\newcommand{\KW}[1]{\texttt{\small\bfseries{#1}}}
%\newcommand{\KW}[1]{\texttt{#1}}
\newcommand{\True}{\CD{true}}
\newcommand{\Define}{\KW{define}}
\newcommand{\Prefer}{\texttt{>>}}
\newcommand{\Path}{\texttt{=>}}
\newcommand{\Link}{\texttt{->}}
\newcommand{\Agg}{\KW{agg}}
\newcommand{\Any}{\KW{any}}
\newcommand{\None}{\KW{drop}}
\newcommand{\In}{\KW{in}}
\newcommand{\Out}{\KW{out}}
\newcommand{\AND}{\texttt{\&}}
\newcommand{\OR}{\texttt{|}}
\newcommand{\NOT}{\texttt{!}}
\newcommand{\Intersect}{\ensuremath{\cap}}
\newcommand{\Union}{\ensuremath{\cup}}

\newcommand{\Exit}{\KW{exit}}
\newcommand{\End}{\KW{end}}
\newcommand{\Start}{\KW{start}}
\newcommand{\Enter}{\KW{enter}}
\newcommand{\Later}{\KW{later}}
\newcommand{\Before}{\KW{before}}
\newcommand{\Internal}{\KW{internal}}
\newcommand{\Never}{\KW{never}}
\newcommand{\Only}{\KW{only}}
\newcommand{\Through}{\KW{through}}
\newcommand{\LinkKW}{\KW{link}}
\newcommand{\PathKW}{\KW{path}}
\newcommand{\Novalley}{\KW{novalley}}

%\let\Url\url
%\renewcommand*{\LaTeX}{\oldLaTeX\space}
\renewcommand{\path}[2]{ #1 \mapsto \ensuremath{#2} }



\begin{document}


%\special{papersize=8.5in,11in}
%\setlength{\pdfpageheight}{\paperheight}
%\setlength{\pdfpagewidth}{\paperwidth}

\title{Don't Mind the Gap:  Bridging Network-wide Objectives and
  Device-level Configurations}

\subtitle{
  (Brief Reflections on Abstractions
  for Network Programming)
  }

%\author{Paper \#324, 14 pages}


\author{Ryan Beckett}
\affiliation{\institution{Microsoft}}
\email{Ryan.Beckett@microsoft.com}

\author{Ratul Mahajan}
\affiliation{\institution{University of Washington} and \institution{Intentionet}}
\email{ratul@cs.washington.edu}

\author{Todd Millstein}
  \affiliation{\institution{UCLA} and \institution{Intentionet}}
\email{todd@cs.ucla.edu}

\author{Jitendra Padhye}
\affiliation{\institution{Microsoft}}
\email{padhye@microsoft.com}
\author{David Walker}
\affiliation{\institution{Princeton University}}
\email{dpw@cs.princeton.edu}

\begin{abstract}
We reflect on the historical context that lead to 
\sysname,
a high-level language and compiler to help network operators
bridge the gap between network-wide routing objectives and low-level configurations of devices that run complex, distributed protocols.
We also highlight the primary contributions that Propane made to the
networking literature and describe ongoing challenges.
We conclude with an important lesson learned from the experience.
\end{abstract}

%\textbf{CCS Concepts}\\
%$\bullet$ Networks $\rightarrow$ {\em Network control algorithms; Network relia%bility; Network management;} 
%\bullet$ Software and its engineering $\rightarrow$ {\em Automated static analy%sis; Domain specific languages}

\keywords{Propane; Domain-specific Language, BGP, Synthesis, Compilation, Fault Tolerance, Distributed Systems}

\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003033</concept_id>
<concept_desc>Networks</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003033.10003068.10003073.10003075</concept_id>
<concept_desc>Networks~Network control algorithms</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003033.10003083.10003095</concept_id>
<concept_desc>Networks~Network reliability</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003033.10003099.10003104</concept_id>
<concept_desc>Networks~Network management</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007</concept_id>
<concept_desc>Software and its engineering</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10010940.10010992.10010998.10011000</concept_id>
<concept_desc>Software and its engineering~Automated static analysis</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011050.10011017</concept_id>
<concept_desc>Software and its engineering~Domain specific languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Networks}
\ccsdesc[500]{Networks~Network control algorithms}
\ccsdesc[500]{Networks~Network reliability}
\ccsdesc[500]{Networks~Network management}
\ccsdesc[500]{Software and its engineering}
\ccsdesc[500]{Software and its engineering~Automated static analysis}
\ccsdesc[500]{Software and its engineering~Domain specific languages}
% \section{Outline}

% \begin{itemize}
% \item highlight the differences between openflow and
%   \item interdomain setting  difference .  same abstraction both
%     inside and outside.
% \end{itemize}

\maketitle




\section{Historical context}

When Software-Defined Networking (SDN) burst onto the scene around 2008,
it offered a new means to control packet forwarding  from a single
centralized vantage point.  Neither network engineers nor 
researchers would be bound to the slowly-evolving technology provided by
traditional routers.  Instead, for many in the networking
community, SDN opened up the opportunity to program new
algorithms that use network-wide data to optimize performance.
The decisions made by these new algorithms could then be realized by
pushing specific packet-processing rules out to a distributed
collection of  OpenFlow-enabled switches.

While many networking researchers examined \emph{what} new algorithms
could be implementing using SDN, a few, in collaboration
with programming languages researchers, began to explore \emph{how}
best to express these algorithms.  With a plethora of new algorithms
and much new infrastructure being developed, there are were bound to
be many bugs, which in the short term at least, might make such network
services less reliable.  Hence, it made sense to consider
whether there might be new programming paradigms that, through their
design, might be able to cut down on certain classes of software
errors.

Frenetic was the first language that provided programmers with
a higher-level interface to OpenFlow switches~\cite{frenetic}.  It responded to control
events from switches, such as failures or traffic statistics, and used
the information it received to compute declarative data plane
policies.  These policies specified much of the same information as
lists of OpenFlow rules, but unlike OpenFlow, they were composable.  For
instance, one could specify a network monitoring policy separately
from a network routing policy and then implement both policies
simultaneously, without fear of conflicts, by invoking a single
function.  Under the covers, Frenetic 
generated OpenFlow rules and installed them
``consistently''~\cite{consistent-updates} to avoid transient bad
behaviors.  Composition and consistent updates
raised the level of abstraction at which
network engineers could implement policy and helped fend off some of
the errors that can arise due to poorly-synchronized rule installation.

Soon afterwards, inspired by Frenetic, researchers looked to extend the set of
policies network engineers could craft to specify intended routing
behavior.
For instance,
NetCore~\cite{netcore} generalized Frenetic's
simple packet patterns, allowing users to classify traffic
using more general boolean predicates over packets, and demonstrated
it was possible to compile
such programs to OpenFlow.
Pyretic~\cite{pyretic} extended NetCore's policy language to allow a
new kind of \emph{sequential composition} to complement Frenetic's
\emph{parallel composition}).  FatTire~\cite{fattire} went a step
further, adding the
abstraction of \emph{paths}, specified by regular expressions.
These paths represented the first real \emph{network-wide}
abstraction.
%FatTire also introduced the idea of specifying the
%number of back-paths required for fault tolerance and implemented such
%requirements using OpenFlow 1.3's fast-failover mechanisms.
% A year later, NetKAT~\cite{netkat} laid out a more general design still in which
% regular expressions for describing paths, could be interleaved with
% boolean predicates for classifying the traffic that should follow
% those paths.  Indeed, by connecting these various network language
% designs with the well-established theory of Kleene Algebra with
% Tests~\cite{kozen:kat}, network programming languages acquired
% rich equational and semantic theories for reasoning about the
% correctness of data plane programs.

Thus, in the five-year period between 2008 and 2013,
researchers had converged on two essential elements of stateless,
network-wide data
plane programming:  (1) regular expressions to describe paths and (2)
boolean predicates to classify packets and to choose the paths.  In 2014, Anderson \emph{et al.}~\cite{netkat}
recognized that network programming languages possessing this
combination of features were instances of a well-known algebraic
structure called a Kleene Algebra with Tests
(KAT)~\cite{kat}.  Through this connection, a rich semantic
theory and a host of algorithmic techniques could be adapted from the
world of formal algebra to the study of network programs.

\section{Propane's Contributions}

While SDN was the hot topic of the day in academia,
most networks, both big and small, continued using
traditional routing protocols such as
OSPF and BGP.  Even modern data centers, which might use SDN around
the edge, often continued to use traditional routing in their
core.  In part, this continued use is certainly
a legacy software and hardware issue.  But it is also likely that
traditional routers, which have the benefit of being plug-and-play,
simply perform well enough in many common
cases.  Finally, regardless of whether a network uses SDN internally
or not, it is necessary to communicate with peers, and the only
current means of doing so is via BGP.  Hence, interfacing with
traditional distributed protocols remains essential, even in the SDN
world.

The primary contribution of Propane is to demonstrate that the kinds
of high-level abstractions used to specify \emph{data plane} policy in SDN could also be adapted to specify
\emph{control plane} policy in traditional networks. In particular,
fundamental network-wide abstractions such as paths, specified via
regular expressions, and boolean expressions, used to
classify traffic, could be combined, as in the SDN world, to denote
the expected flow of data plane traffic.  

However, there are two significant
differences at the level of operator specifications.  First, whereas SDN
programs concern themselves only with intra-domain routing,
Propane could simultaneously specify
both intra- and inter-domain traffic patterns.  Hence, in a single
uniform
notation, network engineers could specify the way they wished to
interact with their peers and how they wanted to route traffic through
their own network.  Second, when failures
occur or a route is withdrawn by the peer, the control plane will recompute its routing decisions and
choose a backup route---these backups must be specified up front,
along with the primary routes.  Propane added relations between paths
to allow operators to specify path preferences such that a lower-preference path is taken only when a higher-preference path is unavailable.

A second key contribution of the Propane is to
demonstrate how global specifications provided can be compiled
and implemented correctly using traditional distributed protocols.  
To do so, the Propane system uses BGP as the
implementation protocol because of its flexibility.  However,
it turns out that not all regular sets can be implemented by path vector protocols
like BGP.  Consequently, Propane defined an analysis to inform users when
their policies cannot be implemented in BGP.  The original
SIGCOMM paper describes the analysis and compilation process briefly;
Beckett's thesis~\cite{beckett:thesis}, which won the 2018 ACM SIGCOMM
dissertation award, fills in the details.

% Unfortunately, management of traditional networks continues to be a
% challenging task.  Indeed, one regularly hears of major networks, some
% of them engineered by the most competent tech firms in the business,
% suffering outages due to changes in network misconfiguration.  We
% speculate that one reason for that may be the gap between the
% intentions of network engineers and the specifications mechanisms
% available to network operators.  On the one hand, objectives are
% phrased in terms of network-wide properties, such as reachability or
% access to servers; on the other hand the mechanisms use to implement
% those properties are device-local.

% Familiar with the history of the development of SDN abstractions, we
% asked ourselves whether such abstractions could be used to program
% conventional routers instead of Hence, the key question we asked 

% So the essential question we asked when beginning the
% development of Propane was whether the high-level abstractions
% developed for specifying SDN data plane routes could be used instead to
% specify control plane mechanics and whether it would be possible to
% compile such specifications to legacy devices so commodity hardware
% and software could be reused.

\section{Continuing Challenges}

While the original work supplied a proof of concept, much work
remained, and continues to remain, to provide the surrounding
infrastructure necessary for Propane to be adopted by mainstream network engineers.

\paragraph*{Scaling} One of the first challenges was to improve the scaling
properties of Propane to make it attractive to engineers of large
networks.  To tackle this problem, in a follow-on system called Propane/AT~\cite{abstract-propane}, we stole an idea in use in
industry: the notion of templates.  Rather than specifying concrete
locations and destinations, we allow Propane-like specifications to include
template variables.  In a first compilation phase, we analyze the
Propane specification with respect to these parameters and an
\emph{abstract topology} and ensure that any legal instantiation of
the parameters will generate a control plane and concrete topology
with desirable properties (\emph{e.g.}, the appropriate level of fault
tolerance).  In a second compilation phase, we instantiate the
parameters and convert the abstract topology to a valid concrete
topology.  We found that this two-phase compilation strategy
dramatically improved compilation times for Propane.  Using abstract
topologies, Propane can compile data center configurations up to two
orders of magnitude faster.  These generated configurations also
allow certain kinds of incremental changes to network configuration
without recompilation and reinstallation of all configurations on all
switches.  
%Beckett describes the details of incremental compilation and the scaling of
%our revised architecture in follow-on work~\cite{abstract-propane} and
%in his thesis~\cite{beckett:thesis}.

\paragraph*{Incremental deployment}  A significant challenge in
deploying Propane industrially is incremental deployment. 
At the moment, Propane is designed for new
networks. How should Propane interact
with existing networks that operate using completely different, ad
hoc configuration system?  This is a rich problem, worthy of future
study, and the topic of an ongoing NSF grant~\cite{nsf-propane}.

One possible approach is to analyze the set of
low-level configurations that are present in the existing
network.  Such an analysis could identify the paths allowed and
synthesize a matching Propane specification.  The simplest way of
doing so may list all the paths through the network one-by-one.
However, such a listing is likely very verbose and compact specifications
are almost always much preferred over verbose ones.  Another approach to
finding a specification would be to try to find a compact
generalization of the naive list of paths.  However, doing so might involve
admitting more paths in the specification than are present in the
existing network.  In other words, a compact generated specification
might over-approximate the set of actual routes.  But how much
overapproximation will a user accept?  What notation should one use
to cut out overapproximations?  These and similar questions
require further research.  

\paragraph*{Incremental evolution}
Once Propane is deployed, engineers will undoubtedly need to update
policy from time to time to addess security vulnerabilities, add or
remove hosts, expand capacity, or change routing decisions.  While
Propane/AT~\cite{abstract-propane} provides mechanisms that allow for
incremental update of the network topology, it does not provide mechanisms for
changing policy.  One approach to solving this problem would be to
adapt recent research on network repair~\cite{Gember-Jacobson:SOSP17}
to the problem.  The idea here would be that the new Propane
program would be the specification and the existing set of
configurations be ``repaired'' to meet this new specification.
Ideally, such repairs would generate a minimal set of commands that
could be issued to update routers.

\section{A Key Lesson:  The Importance of Small Models}
\label{sec:conclusions}

The programming languages that software engineers use on a day-to-day
basis are extremely complicated.  This is true of C++, Python, Haskell, and
JavaScript.  It is also true of Cisco IOS and Juniper JunOS, the
languages network operators use to program their networks.  In order to understand
how these languages work in a deep sense, how to program with them,
and how to build reliable abstractions on top of them, one cannot
tackle the whole language all at once.  It is necessary to build
small, simple models first---little idealized languages---which might
not have every bell and whistle, but that are more uniform than their
real-world counterparts.  Such
small models will almost always leave out elements of the
real language, which will invariably frustrate practitioners.
However, that is
not a bug  but a feature---it frees the researcher to focus on
what is \emph{left in} the small model and to ignore additional
complexity that is \emph{left out}.

In a sense, OpenFlow 1.0 was a small model for packet forwarding.  It
provided an understanding of the network dataplane so
simple that even programming language researchers could understand it!
Once we understood this simple forwarding model,
we could manipulate, transform, abstract, and extend it. And then, finally,
we could begin to apply the lessons learned in this simple setting to
more expansive contexts.  The
latter step is where Propane comes in as it adapted ideas developed in
the world of early SDN dataplane to the
more complex setting of the traditional router.  Going forward, we hope
to see the networking community develop more small models for other
components of the networking stack.

\para{Acknowledgments}
We thank R. Aditya, George Chen,  Lihua Yuan, and the SIGCOMM reviewers for feedback on the original
work. That work was supported in part by the National Science
Foundation awards CNS-1161595 and CNS-1111520 as well as a gift from
Cisco.

The current paper is supported in part by the National Science
Foundation award 1703493.  We thank Jennifer Rexford and George Varghese for
many discussions about Propane over the years and for ideas concerning its evolution.


\balance

\bibliographystyle{abbrv}
\bibliography{references}

% The bibliography should be embedded for final submission.


\end{document}