Subject: RE: protocol vervification

From: Scott Corson <[email-masked]>
Date: Sat, 10 Nov 2001 11:37:50 -0500

JJ, Kui:

I agree that *instantaneous* loop freedom is provable (numerous protocols
have achieved this in the literature).

But in response to Kui's message, I am not aware of any protocol (that does
not use explicit hop count limits, source routing, or some other such
mechanism) that can guarantee *transit* loop freedom.  Meaning that during
the transit time of a packet through the network, the packet can be
guaranteed not to loop indefinitely.  It is my understanding that in the
presence of arbitrary topological change, packets can loop forever.  This
fact, I think, should be provable via contradiction, although I've never
seen such a proof.

Of course the likelihood of transit looping in a well designed protocol in
realistic conditions should be close to zero.  The recent debate on AODV
regards its design/performance w.r.t. realistic conditions.

-Scott

> -----Original Message-----
> From: Jose Garcia-Luna [mailto:[email-masked]]
> Sent: Friday, November 09, 2001 7:03 PM
> To: Kui Wu
> Cc: [email-masked]; [email-masked]
> Subject: Re: protocol vervification 
> 
> 
> 
> It is not impossible to prove instantaneous loops freedom.
> The work needed entails showing that a given invariant
> ensures instantaenous loop freedom if it is enforced
> (done for AODV in the past) and showing that
> all the messaging enforces the invariant. I'd say
> work is in progress on the latter.
> 
> JJ
>