Achieving Correct Hop-by-Hop Forwarding on Multiple Policy-based Routing Paths

Algebra has made the tasks of modelling routing algorithms and proving their correct operation very clear. However, traditional models are only concerned with the convergence to a stable routing solution not covering distributed hop-by-hop forwarding on multiple paths (within a flow or separately per flow). This paper addresses this challenge. Currently, loop-free distributed multipath forwarding is only proven if a strict decrease in the preference of a path occurs with every added link. This is very rigid for multipath routing, limiting the amount of equal preferred paths. In this work we prove that correct distributed forwarding behaviour is possible, without the strict decrease in preference, if the possible pairs of policy values applied to the directed edges connecting two nodes obey to a particular condition. If this is not true, correct behaviour is still possible if the policies applied to links forming circuits in the network graph are constrained according to two other conditions. Modern technologies are bringing the possibility to build new routing protocols using network programmability while distributed operation is still needed in many scenarios due to scaling issues. We show how our results can be relevant in this setting and serve as a tool in the design process and/or for formal protocol verification.