Subject: Re: [babel] babel Digest, Vol 17, Issue 4

From: Tony Przygienda <[email-masked]>
Date: Wed, 4 Jan 2017 12:35:52 -0800

FSM cannot "overspecify" a protocol unless you are perfectly happy with
"undefined" behavior on certain transitions. The underspecification of
transitions tends to hit very, very late in the game under heavy
deployments resulting in hard-to-phatom non-interoperable behavior and
confusing protocol "spec patches" or worst, exploits. Case in point were
some TCP CLOSE corner cases (cleaned up in the mid 90's) and BGP peer
establishment FSM (long denied, finally provided after many, many
interesting corner cases, especially on collisions). A sure indication is
proliferation of "last resort" timers on a protocol or clauses like "if
anything bad happens, just reset".

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

Yes, FSMs can be quite a lot of work and hence shunned for simple,
hacked-up protocols ...  In OSPF, it was largely a question of "style"
given John is a mathematician by trade but it is my observation that
long-term stable, maintainable asynchronous software with transition chains
longer than 2 states is almost always religiously written with FSMs rather
than switch statements and bits sprinkled around ...

--- tony

On Wed, Jan 4, 2017 at 12:00 PM, <[email-masked]> wrote:

> Send babel mailing list submissions to
>         [email-masked]
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://www.ietf.org/mailman/listinfo/babel
> or, via email, send a message with subject or body 'help' to
>         [email-masked]
>
> You can reach the person managing the list at
>         [email-masked]
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of babel digest..."
>
> Today's Topics:
>
>    1. Re: [PATCH 2/4] address IETF-97 slides section I point 2
>       (Juliusz Chroboczek)
>
>
> ---------- Forwarded message ----------
> From: Juliusz Chroboczek <[email-masked]>
> To: Denis Ovsienko <[email-masked]>
> Cc: Babel at IETF <[email-masked]>
> Date: Tue, 03 Jan 2017 22:46:13 +0100
> Subject: Re: [babel] [PATCH 2/4] address IETF-97 slides section I point 2
> > The normative text in 6126-bis does not define the protocol instance
> > behaviour in terms of a finite state machine (FSM).
>
> There is no FSM in Babel.  Babel is described in terms of a set of
> conceptual data structures and a set of requirements.  I do not know
> whether Babel can be described by an FSM, I suspect any such description
> would be over-specified.
>
> > In RFC 2328 (OSPF version 2) Sections 9 (The Interface Data Structure)
> > and 10 (The Neighbor Data Structure) use FSMs extensively to define the
> > protocol instance.
>
> [...]
>
> > (And so on, about 40 pages in those two sections altogether.)
>
> Right.  OSPF relies crucially on the reliability of the flooding
> procedure, so it is quite natural that the spec spends a lot of space
> describing the reliability features in excruciating detail.  Babel's
> design is very different -- Babel is designed to be robust in the presence
> of an unreliable protocol, and Babel's properties are preserved even in
> the presence of packet loss, of packet delay, and even of packets
> overtaking each other.  I have a proof of that.
>
> > RFC 4271 (BGP-4) Section 8 (BGP FSM) exists for a reason too, makes
> > similar definitions and takes 38 pages.
>
> Yes, BGP relies on a reliable transport and a reliable handshake, albeit
> for slightly different reasons (efficiency rather than correctness).
> Again, these reasons do not apply to Babel, which is not designed to carry
> large amounts of data, and does not rely on a reliable transport.
>
> > Whether we have or don't have a consensus on the exact way to reduce the
> > ambiguity, it seems wrong to me to leave the document as it is now. The
> > changes I suggested are on the list, would you like to suggest something
> > too?
>
> I made a number of proposals, the last of which was in my mail dated 14
> December 2016 with message-id <[email-masked]>.  In short,
> I intend to rewrite 3.4.1 and 3.4.2 to make them stylistically more in
> line with the rest of the document.
>
> But that's point 3 on my todo list (point 1 is integrating the extension
> mechanism in the body of the document, and point 2 is fixing the treatment
> of bit 0x80 with unknown AEs).
>
> -- Juliusz
>
>
>
> _______________________________________________
> babel mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/babel
>
>

-- 
*We’ve heard that a million monkeys at a million keyboards could produce
the complete works of Shakespeare; now, thanks to the Internet, we know
that is not true.*
—Robert Wilensky

---

From: Juliusz Chroboczek <[email-masked]>
Date: Thu, 05 Jan 2017 16:26:59 +0100

Hi Tony, good to hear from you.

> "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