Agda-routing

Requirements: Agda 2.6.4 and Standard Library 2.0

This library reasons about asynchronous iterative algorithms and network routing problems. It is organised in the same manner as the Agda standard library and contains extensions of several of the Agda standard library modules. The core contributions of this library can be found in the RoutingLib.Iteration and RoutingLib.Routing directories.

The contents of the library is described in An Algebraic Perspective on the Convergence of Vector-Based Routing Protocols by Matthew L. Daggitt, submitted for his PhD thesis at the Department of Computer Science and Technology, University Of Cambridge, 2019.

Below is a guide that helps users match up the content of the thesis with their associated formalisation in Agda.

Chapter 3 - Asynchronous iterative algorithms

A formalisation of the pre-existing theory of static asynchronous iterative algorithms can be found in the directory RoutingLib.Iteration.Asynchronous.Static and is organised as follows:

• Static schedules: RoutingLib.Iteration.Asynchronous.Static.Schedule

• Static pseudoperiods: RoutingLib.Iteration.Asynchronous.Static.Schedule.Pseudoperiod

• The static asynchronous iteration state function δ, and what it means for it to be correct:
  RoutingLib.Iteration.Asynchronous.Static

• Conditions sufficient for convergence (ACO, AMCO etc.): RoutingLib.Iteration.Asynchronous.Static.Convergence.Conditions

• Proof that our relaxation of the ACO conditions are equivalent to that of Uresin & Dubois: RoutingLib.Iteration.Asynchronous.Static.Convergence.RelaxACO

A formalisation of the new theory of dynamic asynchronous iterations can be found in the directory RoutingLib.Iteration.Asynchronous.Dynamic and is organised as follows:

• Dynamic schedules: RoutingLib.Iteration.Asynchronous.Dynamic.Schedule

• Dynamic pseudoperiods: RoutingLib.Iteration.Asynchronous.Dynamic.Schedule.Pseudoperiod

• The dynamic asynchronous iteration state function δ, and what it means for it to be correct: RoutingLib.Iteration.Asynchronous.Dynamic

• Conditions sufficient for convergence (dynamic ACO, dynamic AMCO etc.): RoutingLib.Iteration.Asynchronous.Dynamic.Convergence.Conditions

• Proof that F being a dynamic ACO implies that δ is convergent: RoutingLib.Iteration.Asynchronous.Dynamic.Convergence.ACOImpliesConvergent

• Proof that F is a dynamic AMCO implies F is a dynamic ACO is found in: RoutingLib.Iteration.Asynchronous.Dynamic.Convergence.AMCOImpliesACO

• Public facing interface that contains all convergence conditions and theorems, which should be used to prove new convergence results: RoutingLib.Iteration.Asynchronous.Dynamic.Convergence

Chapter 4 - An algebraic model for vector-based protocols

• The definition of routing algebras and path algebras as well as the definition of properties like distributive, strictly increasing, finite etc. can be found in: RoutingLib.Routing.Algebra

• The basic definitions of next-hop routing, including the definition of the network, adjacency matrices, routing states etc. can be found in: RoutingLib.Routing

• The synchronous model for an abstract vector-based routing protocol can be found in: RoutingLib.Routing.VectorBased.Synchronous

• The asynchronous model for an abstract vector-based routing protocol can be found in: RoutingLib.Routing.VectorBased.Asynchronous

• The code for ℙ(∙), the generic method of constructing path algebras from routing algebras, is in:
  RoutingLib.Routing.Algebra.Construct.AddPaths

• Some examples of basic routing algebras can be found in:

  • RoutingLib.Routing.Protocols.DistanceVector.ShortestPaths
  • RoutingLib.Routing.Protocols.DistanceVector.WidestPaths
  • RoutingLib.Routing.Protocols.DistanceVector.ShortestWidestPaths

Chapter 5 - Convergence

The proof of convergence of finite, strictly increasing distance-vector protocols is organised as follows:

• The definitions of the height function and associated metrics are in: RoutingLib.Routing.VectorBased.Asynchronous.DistanceVector.Convergence.Metrics

• The properties of the height function and associated metrics are in: RoutingLib.Routing.VectorBased.Asynchronous.DistanceVector.Convergence.Properties

• The proof that F is strictly contracting over the metric D is in: RoutingLib.Routing.VectorBased.Asynchronous.DistanceVector.Convergence.StrictlyContracting

The proof of convergence of increasing path-vector protocols is organised as follows:

• The definition of the consistent sub-algebra is in: RoutingLib.Routing.Algebra.Construct.Consistent

• The definitions of the height function and associated metrics are in: RoutingLib.Routing.VectorBased.Asynchronous.PathVector.Convergence.Metrics

• The properties of the height function and associated metrics are in: RoutingLib.Routing.VectorBased.Asynchronous.PathVector.Convergence.Properties

• The proof that F is strictly contracting on orbits and fixed points over the metric D is found in: RoutingLib.Routing.VectorBased.Asynchronous.PathVector.Convergence.StrictlyContracting

A summary of all the convergence results can be found in: RoutingLib.Routing.VectorBased.Asynchronous.Results

Chapter 6 - Rate of convergence

Note that, as discussed in the thesis, the Θ(n²) convergence time for the Qₙ gadgets is the only major proof not formalised in Agda. This is because:

1. it is time consuming to formally reason about the entire execution trace of an abstract family of graphs.

2. being a lower bound there are less severe practical consequences if it turns out to be incorrect.

3. execution traces that exhibit convincing quadratic behaviour have been generated using Python scripts.

The proof of the Ω(n²) bound on convergence in the worst case is laid out as follows:

• Definition and properties of the set of fixed/converged/real nodes: RoutingLib.Routing.VectorBased.Synchronous.PathVector.RateOfConvergence.Step1_NodeSets.agda

• Identification of the converged subtree and the minimal edge out of it: RoutingLib.Routing.VectorBased.Synchronous.PathVector.RateOfConvergence.Step2_ConvergedSubtree.agda

• Definition and properties of the set of dangerous nodes: RoutingLib.Routing.VectorBased.Synchronous.PathVector.RateOfConvergence.Step3_DangerousNodes.agda

• The main inductive step of the argument: RoutingLib.Routing.VectorBased.Synchronous.PathVector.RateOfConvergence.Step4_InductiveStep.agda

• The full inductive argument: RoutingLib.Routing.VectorBased.Synchronous.PathVector.RateOfConvergence.Step5_Proof.agda

Chapter 7 - Practicalities

• Definition of comparability: RoutingLib.Routing.Algebra.Comparable

• Definition of similarity and proof that it preserves convergence: RoutingLib.Routing.Algebra.Simulation

• Path inflation and deflation functions can be found in: RoutingLib.Data.Path.Uncertified

Chapter 8 - Agda: proofs and protocols

• Definition of the algebra BGPLite based on a fragment BGP: RoutingLib.Routing.Protocols.PathVector.BGPLite.Main

• Definition of a algebra BGPLite-sim that is similar to BGPLite yet has better algebraic properties: RoutingLib.Routing.Protocols.PathVector.BGPLite.Simulation

• Proof that BGPLite-sim i) simulates BGPLite and ii) convergent: RoutingLib.Routing.Protocols.PathVector.BGPLite.Simulation.Properties

• Proof that BGPLite is convergent: RoutingLib.Routing.Protocols.PathVector.BGPLite.Simulation.Properties

Related work

[1] Üresin, A., Dubois, M. Parallel asynchronous algorithms for discrete data. Journal of the ACM 37(3) (1990)

[2] Gurney, A.J.T. Asynchronous iterations in ultrametric spaces (2017),https://arxiv.org/abs/1701.07434

Resulting publications

[3] Daggitt, M.L., Gurney, A.J.T., Griffin, T.G. Asynchronous convergence of policy-rich distributed bellman-ford routing protocols, SIGCOMM (2018)

[4] Daggitt, M.L, Griffin, T.G. Rate of convergence of increasing path-vector routing protocols, ICNP (2018)

[5] Zmigrod, R. , Daggitt, M.L., Griffin, T. G. An Agda Formalization of Üresin & Dubois’ Asynchronous Fixed-Point Theory, ITP (2018).

[6] Daggitt M.L., Zmigrod, R., Griffin T.G. A Relaxation of Üresin & Dubois' Asynchronous Fixed-Point Theory in Agda JAR (2019)

[7] Daggitt M.L., Griffin T.G. Dynamic Asynchronous Iterations JPDC (2022)

[8] Daggitt M.L., Griffin T.G. Formally verified convergence of policy-rich DBF routing protocols, ToN (2023)