IEEE 1394 Tree Identify Protocol

The Problem

The 1394 High Performance serial bus is used to transport digitized video and audio signals within a network of multimedia systems and devices. It has a scalable architecture, and it is ``hot-pluggable'', meaning that devices and peripherals can easily be added or removed from the network at any time.

The system as a whole is complex, comprising a number of distributed communicating components and using a number of different protocols for different tasks (e.g. data transfer between nodes in the network, bus arbitration, leader election). The IEEE standard IEEE 1394-1995 provides a layered description in the style of OSI, with physical, link, and transaction layers. Each layer is in turn split into different phases.

In essence, the tree identify process of IEEE 1394 is a leader election protocol which takes place after a bus reset in the network (i.e. when a node is added to, or removed from, the network). Immediately after a bus reset all nodes in the network have equal status, and know only to which nodes they are directly connected. A leader (root) needs to be chosen to act as the manager of the bus for subsequent phases of the 1394. The protocol is designed for use on connected networks, will correctly elect a leader if the network is acyclic, and will report an error if a cycle is detected.

Essentially, each node has two phases based on the number of children, c, and the number of neighbours, n. If n - c > 1 the node waits for ``be my parent'' requests from its neighbours. If n - c = 1 then the node sends a ``be my parent'' request to the neighbour which isn't a child if it hasn't already received a ``be my parent'' request from that neighbour. This implies that leaf nodes are the first to communicate with their neighbours, and that the spanning tree is built from the leaves.

The protocol may not proceed this straightforwardly because ``be my parent'' requests are not atomic and may not be sucessful. Actually, a request must be followed by an acknowledgement, and an acknowledgement of the acknowledgement!

Since requests are not atomic contention may arise (two nodes simultaneously send ``be my parent'' requests to each other). Since only one node can be the leader contention must be resolved; this is done by timing. The standard specifies that each node chooses nondeterministically whether to wait for a long or short time. If, after the wait period is over, there is a message from the other node saying ``be my parent'' then the node becomes the root. If there is no such message then the node resends its own ``be my parent'' message (and contention may result again).

This protocol is similar to one presented in Distributed Algorithms, page 501, where a different method of contention resolution is used (the node with the highest identifier becomes the root). This approach will not work for IEEE 1394 because the nodes do not have identifiers during the Tree Identification Phase. The protocols were developed independently.

Further Information

We have obtained permission to reprint those sections of the IEEE standard and supplement (1394a-2000) directly related to the Tree Identify Protocol. Contact us for a copy.

We have a special arrangement with IEEE for bulk ordering the standard and the supplement documents at substantially reduced cost (half normal non IEEE member price). Contact us to find out more.

You may also wish to visit the IEEE standards site.

Points to Address

Things we'd like you to consider during the specification process are:

  1. Which parts of the system are specified, at which level, and in which way (verbally, rigorously, formally)? Do you consider your chosen approach to be particularly expressive or particularly awkward for this sort of problem?
  2. Which parts of the system are analysed, and in what way (manual, informal, partially or fully automated)?
  3. Have assumptions about the architecture or the behaviour of the system been made explicit and are they documented?
  4. Is the solution easy to change? Following a change, can analyses be reused, or are all proofs invalidated?
  5. How long did it take:
    1. How much time has been spent on producing the solution? Give the number of person months, if possible, for the various parts of the solution.
    2. How much preparation is needed to become sufficiently expert in the used specification framework in order to be able to produce a solution to such a problem in that framework? Indicate the number of weeks of training which believe is necessary for an average programmer to learn the methods.
  6. What are the premises for a good understanding of the proposed solution?
    1. Is a detailed knowledge of the used formalism needed?
    2. Can an average programmer understand the solution (with no special training)?
    3. How much time do you believe is necessary for the average programmer without knowledge of the used specification methods to learn what is needed to be able to understand the solution? Could you discuss this solution with a non formal methods literate person, e.g. a customer.
    4. Do you believe your solution provides a suitable alternative formalisation to the IEEE standard?

Specifically, for the Tree Identify Protocol the safety and liveness requirements to be proved are:

  1. A leader is eventually chosen.
  2. Only one leader is chosen.

For after the workshop:

  1. What are the comparable other solutions and what are the major difference with respect to them? What other solutions complement the given solutions and in which respect?
If you think there's some important question we've missed, contact us.

Previous Descriptions of IEEE 1394

There are several existing specifications of the Tree Identify Process:

I/O Automata

M.C.A. Devillers, W.O.D. Griffioen, J. Romijn, and F. Vaandrager. Verification of a Leader Election Protocol - Formal Methods Applied to IEEE 1394. Formal Methods in System Design, 16(3):307--320, 2000.

J.M.T. Romijn. A Timed Verification of the IEEE 1394 Leader Election Protocol. In Fourth International Workshop on Formal Methods for Industrial Critical Systems , 1999. To appear as a special issue of Formal Methods in System Design.

D.P.L. Simons and M.I.A. Stoelinga. Mechanical Verification of the IEEE 1394a Root Contention Protocol using Uppaal2k. Report CSI-R009, Computing Science Institute, University of Nijmegen, Nijmegen, 2000.

M.I.A. Stoelinga and F.W. Vaandrager. Root Contention in IEEE 1394. In 5th AMAST Workshop on Real-Time and Probabilistic Systems, LNCS 1601. Springer-Verlag, 1999.

ELOTOS

C. Shankland and A. Verdejo. Time, E-LOTOS, and the FireWire. In M.A. Marsane, J. Quemada, T. Robles, and M. Silva, editors, Workshop on Formal Methods and Telecommunications, pages 103--119. Prensas Universitarias de Zaragoza, 1999.

LPMC

Hans Toetenel, Ronald Lutjc Spelberg, and Giosue Bandini. Parametric Verification of the IEEE 1394a Root Contention Protocol using LPMC. In proceedings of The 7th International Conference on Real-Time Computing Systems and Applications (RTCSA 2000), IEEE Computer Society Press, 2000.

G. Bandini, R.L. Spelberg, R.C.H. de Rooij, and W.J. Toetenel. Application of Parametric Model Checking - The Root Contention Protocol. In proceedings of the Hawaii International Conference on Systems Sciences (HICSS-34 2001), IEEE Computer Society Press, 2001.

mCRL

C. Shankland and M. van der Zwaag. The Tree Identify Protocol of IEEE 1394 in mCRL. Formal Aspects of Computing, 10:509--531, 1998.

Have we missed out your formal specification/analysis of the Tree Identify Protocol of IEEE 1394? Contact us and we'll update the page.

References

IEEE 1394-1995. Institute of Electrical and Electronics Engineers. IEEE Standard for a High Performance Serial Bus. Std 1394-1995, August 1995.

IEEE 1394a-2000. Institute of Electrical and Electronics Engineers. IEEE Standard for a High Performance Serial Bus (Supplement). Std 1394a-2000, 2000.

N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, Inc, 1996.


Quick links:
IEEE 1394 Workshop
FME 2001
Last revision: 21st August 2000.