From paul@walker.demon.co.uk Sun Oct 31 15:49:06 2004 From: Paul Walker To: occam-com@ukc.ac.uk Date: Fri, 7 Nov 1997 16:13:50 +0000 Subject: 1394 bug and formal methods MIME-Version: 1.0 X-Mailer: Turnpike Version 3.03a Message-ID: 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@natlab.research.philips.com -- Paul Walker 4Links phone/fax paul@walker.demon.co.uk P O Box 816, Two Mile Ash +44 1908 http://www.walker.demon.co.uk Milton Keynes MK8 8NS, UK 566253