The Vision
Can we do for routing protocols what YACC did for parsers?
That is, can we define a high-level declarative language
that can be used to specify routing protocols in such a way
that implementations can be generated automatically?
This is the goal of metarouting.
Like YACC, metarouting is based on a solid
theoretical foundation.
Whereas YACC is based on context-free grammars,
metarouting is based on algebraic structures
related to semirings (Sobrinho's Routing Algebras are an example).
Routing algebras provide an abstract formalism which
captures the policy component of routing protocols ---
how routes are described, how best routes are selected, and
how routing policies are defined and applied.
A routing protocol is an algebra together with a
mechanism (such as link-state or path-vector) for
computing routing solutions.
For correctness, each mechanism requires specific
algebraic properties to hold in the associated algebra.
The main innovation of metarouting centers around the
definition of a metalanguage for the specification
new routing algebras.
The language is designed so that the algebraic properties
required by mechanisms can be automatically derived
in much the same way that type information is derived in
programming languages.
We envision a world in which routers do not implement any
routing protocols but rather come with a
routing metalanguage compiler.
The network operator community could then take
on the task of standardizing and developing routing
protocols, leaving the definition and implementation of
the metalanguage to the IETF and the vendors.
Progress Report (July 2011)
Beta-release of metarouting prototype: mre_beta.tgz.
Implementation is in Coq (by Vilius Naudziunas),
with extracted code in Ocaml.
A simple interface is provided, writting in Ocaml.
Note: this is a very preliminary version.
In the process of implementing a prototype system based on the
ideas of the SIGCOMM 2005 paper,
we encountered the following issues.
- Need for necessary and sufficient conditions. The SIGCOMM 2005 paper was based on sufficient conditions
for each constructor in the metalanguage and each property of interest. However, this leads to user (specification writer)
frustration when the tool says I don't know. Thus, we have been developing
necessary and sufficient conditions ("if-and-only-if rules") for all of our constuctors and properties.
An example of this type of work can be found here
- Need for more expressive language.
The number of theorems required explodes.
The combination of these first two issues leads to a large increase
in the number of if-and-only-if theorems that need to be proved and introduces many additional properties.
(Remember, this theorem proving is done by the metarouting language designers at design time so that
specification writers will never have to prove theorems!)
It bacame increasing difficult to manage this by hand, and we moved the metarouting prototype to
an implementation in Coq (This work is being done by Vilius Naudziunas.)
The implemetation extracts Ocaml code.
Beyond one-algebra, one-algorithm. In practice, routing domains are often partitioned into
disjoint regions where differnt (distributed) algorithms are used to select paths.
Arc-oriented vs. node-oriented configurations.
Basic algebraic theory of local optima.
- Related Links
- Current Members
- Past Members
- Funding: We would like to thank