[babel] Babel and undefined behaviour [was: babel Digest, Vol 17, Issue 4]

[Juliusz Chroboczek <[e-mail]>]

Hi Tony, good to hear from you.

> FSM cannot "overspecify" a protocol unless you are perfectly happy with
> "undefined" behavior on certain transitions.

Yes, Babel is tolerant of undefined behaviour in many cases.  Please bear
with me while I lecture a little.

Traditional link-state protocols are based on an algorithm that is extremely
refined: their correctness crucially depends on three non-trivial properties:

 1. the LSDBs are synchronised at all times;
 2. Dijkstra converges;
 3. the concatenation of each node's truncated tree yields a forest.

These properties are not built into the algorithm, they must be guaranteed
by the protocol.  (1) is why OSPF and IS-IS use a reliable transport and
split large routing domains into areas; (2) and (3) are why link-state
protocols are restricted to integer metrics and lowest-metric route
selection without filtering (within areas).

Babel is more similar to BGP: it uses a primitive and therefore robust
algorithm, that can survive filtering, non-isotonic metrics, unreliable
transports, and different neighbour acquisition algorithms.  The only
requirements Babel puts on the implementation are:

  1. In the flat routing case, Babel is safe (yields a loop-free tree) as
     long as:
       (a) no message is received before it is sent; and
       (b) the feasibility condition is respected.

  2. Babel is complete (eventually yields all possible routes) as long as:
       (a) every neighbour is eventually acquired;
       (b) every update is eventually received;
       (c) every request eventually reaches the source.

Because the algorithm is so robust, there are fewer requirements on the
protocol.  For example, property 2.a above can be satisfied by acquiring
a neighbour as soon as we receive a packet, as soon as we receive a Hello,
as soon as we receive an IHU, or at any other time as soon as this happens
often enough.

(Aside: note that filtering is a structured way of violating property 2b.
That's fine, Babel remains safe in the presence of filtering, although it
is no longer complete.)

(Aside: as we've discussed before, Tony, property 1.a does not assume
a global clock -- it merely says that the happens-before relation is
well-founded.)

> Descriptive language is nothing but ad-hoc extended FSM description along the
> lines "if THAT happens, do THIS" ..

There are a few places in Babel where the protocol says "it doesn't matter
when you do this, as long as it eventually happens".  I don't know how to
express that in an FSM, even a non-deterministic one.

> In OSPF, it was largely a question of "style" given John is
> a mathematician by trade

The notion of "often enough" is well established in Maths, although it's
usually called "infinitely often".  Of course, since Babel uses expiry
timers, "often enough" really means "before the timer expires and flushes
your incomplete state".

-- Juliusz