1394 bug and formal methods

[Paul Walker <paul@xxxxxxxxxxxxxxxxxx>]

What do you make of this?

Clearly it would have been better never to have had the problem
described, which will probably need there to be re-runs of most 1394
silicon.

But (playing devil's advocate) if the formal methods are now so good
they can detect these problems in systems designed to deadlock, do we
need CSP and its communication model embedded in 1355 to eliminate the
deadlocks by design?

Paul

(sorry if you get multiple copies. I'm sending separately to the hic
reflector, the 1355 reflector, and the occam reflector)

  ------- Forwarded message follows -------
About two years ago an activity at Philips Research has been initiated to put
a challenge to formal verification groups around the world. The subject of this
was the part of the link layer state machine concerning the asynchronous mode.
Over the past two years several groups have been gradually involved and this
message serves to mention some relevant results to the 1394 technical community.
Below a very brief description of those results and a reference to more
detailed information is provided.

The first result was obtained by people from INRIA in France and concerns a
potential deadlock that is difficult to detect by other means such as testing
or simulation. In a nutshell, the problem can be described as follows. After
receiving a broadcast packet the link layer will inform the transaction layer
by a link data indication. After receiving this link data indication the
transaction layer shall communicate a link data response to the link layer.
The problem now is that the link layer state machine has no transition for
receiving this (even though it need not take any action upon it). As a result
this node blocks after which the whole system will deadlock. The solution is
straightforward: adding a link data response of NO_OPERATION transition from
L0 to itself in the state machine of the link layer will solve the problem.
After this correction the deadlock freeness and another four interesting
properties of the link layer protocol have also been established by this group
at INRIA.

Further pointers to these results and a more detailed description of the problem
and its solution can be found at the URL
   http://www.inrialpes.fr/vasy/pub/Press/firewire.html

This URL also provides a reference to the second problem that has been found
by Kuehne, Hooman and de Roever, and independently by Bas Luttik. This problem
occurs when the link layer receives a packet from the physical layer while it
has a pending request from the transaction layer to send some other packet.
The state machines in the standard do not specify what should happen with the
pending request from the transaction layer. The following two solutions have
been proposed:
1. Kuehne, Hooman and de Roever simply consider the pending request for
   arbitration to be lost, together with the request from the transaction layer.
2. Bas Luttik proposes to add a one place buffer to the link layer that contains
   packets received from the transaction layer but not yet sent. The link layer
   may receive a request from the transaction layer if and only if its buffer
   is empty.

With best regards,

Ron
______________________________________________________________________________
dr. R.L.C. (Ron) Koymans               Philips Research Laboratories Eindhoven
Building: WL p 320                     Prof. Holstlaan 4
Phone: +31 40 2743485                  5656 AA  Eindhoven
Fax:   +31 40 2743741                  The Netherlands
E-mail: koymans@xxxxxxxxxxxxxxxxxxxxxxxxxxx

-- 
Paul Walker                      4Links                      phone/fax
paul@xxxxxxxxxxxxxxxxxx          P O Box 816, Two Mile Ash    +44 1908
http://www.walker.demon.co.uk    Milton Keynes MK8 8NS, UK      566253