OAS Casestudy: The IEEE 1394.1 FireWire Net Update Protocol

IEEE 1394 and P1394.1 FireWire standards

In 1995, the IEEE (The Institute for Electrical and Electronics Engineers) has published the IEEE 1394 standard for Serial Buses, nicknamed FireWire and i.LINK. This standard prescribes how to connect devices together into a IEEE 1394 bus, providing high-speed asynchronous and isochronous point-to-point and broadcast communication. The 1394 Trade Association is a marketing organization that promotes IEEE 1394 technology.
Technical bit: Each 1394 device has its own unique 64-bit identity number. Also, the standard describes both cable and backplane implementations. The scope of this page is the cable situation.

An example IEEE 1394 bus topology

From 1996 onwards, the IEEE 1394.1 Working Group has worked on the IEEE P1394.1 draft standard for Serial Bus Bridges. In this document, technology is introduced for connecting 1394 buses into a P1394.1 net. In May 2004, the final ballot was held, and the request for approval of the IEEE 1394.1 standard was made.

An example IEEE P1394.1 net topology

Technical bit: Contrary to what the above picture may suggest, each P1394.1 bridge consists of two separate 1394 devices each connected to its own 1394 bus. The connection between the nodes in the bridge (the bridge fabric), is not part of any bus, and facilitates communication between the two buses without merging them into one bus. Each of the two devices in a bridge is called a portal.

The P1394.1 Net Update Protocol

Both 1394 buses and P1394.1 nets are supposed to work in a plug-and-play fashion, which means that devices may be plugged in and out, or switched on and off while remaining bus/net continues to operate without too much disruption. In order to facilitate this functionality for P1394.1 nets, a protocol called net update maintains several spanning trees in the net. Obviously, if topology changes occur, this protocol must work out the changes in these spanning trees.
Technical bit: All of these trees have buses for nodes and bridges for edges. In the main spanning tree, the root bus has the prime portal, whose unique identity is used as the identity of the net. Also, each bus has either this prime portal, or a portal whose bridge points in the direction of the root bus. In the following picture, this is illustrated for two nets that are joined together by a topology change.

Two IEEE P1394.1 nets are being connected

Here are on-line descriptions of the 1394 and P1394.1 functionality, of the spanning trees, and of the net update protocol.

The Spin Model

For the project Improving the Quality of Protocol Standards (funded by NWO), an abstract model has been made of the net update protocol in the language Promela, which input to the model checking tool Spin. The model may be found here. It contains five bridges, consisting of two portals. For each portal, there are two processes in the Promela: the ordinary behaviour, and special coordinator behaviour. Separately there is an init process that initializes global variables, starts all other processes, and checks safety properties, and a process that introduces random topology changes.

Spin experiences

We have performed many non-interactive random Spin simulations on the Promela model, and found many modelling and protocol mistakes. We have attempted exhaustive verification, but the model is too complex and large for this. We have performed approximate verifications, these terminate without finding errors. The results are described in several papers, that can be found on the project page.

IEEE P1394.1 adjustments

Due to our efforts, many changes have been made to the protocol in the IEEE P1394.1 draft standard. We list some important ones here:

Synchronised bridges The two portals in one bridge are now required to only change their information in synchronisation with each other.
Unmuting The draft standard did not mention when a bridge without direction must be directed again, this has been included and adjusted many times.
Undetected loops Multiple, rapid changes to the net topology may cause a loops that does not meet the loop criterion, hence is not detected and may cause net update to not terminate. A separate net reset protocol called net panic has been introduced to remedy this situation, which is described here.
Correctness properties A number of correctness properties have been defined, which must hold in a stable situation, and which ensure that the trees have been spanned correctly. These have guided the construction of an abstract version of the protocol as well as the manual proofs for the lower level version, and have been added to the IEEE standard as a normative annex which e.g. enables debugging.

These and more changes are described elaborately over here.