## Θ Metarouting |

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.

**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- Lexicographic Products in Metarouting. Alexander Gurney, Timothy G. Griffin. International Conference on Network Protocols (ICNP), October 2007, Beijing.

**Need for more expressive language**.- Pathfinding through Congruences. Alexander Gurney, Timothy G. Griffin. 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 12), June 2011, Rotterdam
- Neighbor-specific BGP: An algebraic exploration. Alexander Gurney, Timothy G. Griffin. International Conference on Network Protocols (ICNP), October 2010, Kyoto.

**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.- A model of Internet routing using semi-modules. John N. Billings and Timothy G. Griffin. RelMiCS11/AKA6, November 2009.
- Hybrid Link-State, Path-Vector Routing. M. Abdul Alim, Timothy G. Griffin. ASIAN INTERNET ENGINEERING CONFERENCE (AINTEC) 2010 November 15--17, 2010, Bangkok, Thailand.
- On the interaction of multiple routing protocols. M. Abdul Alim, Timothy G. Griffin. Work in progress.

**Arc-oriented vs. node-oriented configurations**.- A model of configuration languages for routing protocols. Philip J. Taylor and Timothy G. Griffin. PRESTO workshop (at SIGCOMM 2009)

**Basic algebraic theory of local optima**.- Towards a Unified Theory of Policy-Based Routing. Chi-kin Chau, Richard Gibbens, Timothy G. Griffin. University of Cambridge. INFOCOM 2006.
- Increasing Bisemigroups and Algebraic Routing. Timothy G. Griffin and Alexander Gurney, RelMiCS10/AKA5, April 2008.
- The Stratified Shortest-Paths Problem (Invited Paper). Timothy G. Griffin. Conference on COMmunication Systems and NETworkS (COMSNETS) 2010. Here are the talk slides.
- Routing in Equilibrium. João Luís Sobrinho and Timothy G. Griffin. The 19th International Symposium on Mathematical Theory of Networks and Systems (MTNS 2010).

- Related Links
- An Algebraic Approach to Internet Routing (Michaelmas Term 2010)
- Graphs, Dioids and Semirings : New Models and Algorithms, by Michel Gondran , Michel Minoux.
- Quagga Routing Suite
- XORP
- The Click Modular Router Project
- BinPAC
- Current Members
- M. Abdul Alim
- Timothy G. Griffin
- Vilius Naudziunas
- João Luís Sobrinho
- Philip Taylor
- Past Members
- Alex Gurney
- John Billings
- Balraj Singh
- Funding: We would like to thank