Database of Case Studies Achieved Using CADP

SCSI-2 Bus Arbitration Protocol.

Organisation: INRIA Rhône-Alpes / VASY (FRANCE)
FMT group / University of Twente (THE NETHERLANDS)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design.

Period: 2002

Size: about 150 lines of LOTOS

Description: When designing complex systems, it is desirable to address functional correctness and performance evaluation within the same framework, for both scientific and economic reasons. A successful approach to achieve this relies on existing description languages such as the ISO standard LOTOS and state-of-the-art verification tool sets such as CADP. Basically, the approach consists in starting from a functionally verified LOTOS specification, in which timing information is introduced to express that certain events are delayed by a random time. To support this methodology, the components of CADP are used together with a novel tool named BCG_MIN, which allows to minimize stochastic models. The approach is illustrated by an industrial case-study: the bus arbitration protocol used in the SCSI-2 (Small Computer System Interface) standard.

The system considered consists of at most 8 devices (7 hard disks and a disk controller) connected by a bus implementing the SCSI-2 standard. Each device is assigned a unique SCSI number between 0 and 7. Engineers at Bull discovered in the early 90's potential starvation problems for disks having SCSI numbers smaller than the SCSI number of the disk controller. The problem was first investigated by Massimo Zendri, who developed a Markovian queing model to study performance issues. Later, the functional aspects of the SCSI-2 arbitration protocol were formalised in LOTOS by Hubert Garavel, with an emphasis on modelling arbitration concisely using LOTOS multiway rendezvous. This LOTOS specification served as a basis for model-checking by Radu Mateescu, allowing to rediscover the starvation problem mechanically. The same LOTOS specification is also used as basis for studying performance issues in the present work.

In the SCSI-2 system, the controller can send randomly to the disk n a message "CMD !n" (command) indicating a transfer request (read/write a block of data from/to the disk). After processing this command, the disk sends back to the controller a message "REC !n" (reconnect). The CMD and REC messages are stored in 8-place FIFO queues; since the contents of these messages are not modelled, the queues are represented as simple counters in the LOTOS specification. The CMD and REC messages circulate on the SCSI bus, which is shared by all devices. To avoid access conflicts, the SCSI-2 standard defines a bus arbitration protocol based on fixed priorities: if several devices want to access the bus simultaneously, the device with the highest SCSI number is granted access. The devices are modelled as LOTOS processes executing concurrently. The arbitration (inspection of the bus content by all devices) is modelled by a multiway LOTOS rendezvous with value negotiation and pattern-matching.

To study performance aspects, the LOTOS specification is enhanced with additional information about timing characteristics:

  • A Markov delay, modelled by an action "LAMBDA !n", is introduced in the controller to model the load (transfer requests issued by the controller) that stimulates the whole SCSI-2 system.

  • A Markov delay, modelled by an action "MU !n", is introduced in the disks to model the disk servicing time, i.e., the time needed by a disk to fetch or store the requested data.

  • A Markov delay, modelled by an action "NU", determines the bus delay time, i.e., the delay between two consecutive bus arbitration periods. This parameter is introduced by using an additional LOTOS process which constrains the behaviour of the rest of the system.
A configuration with 3 disks and a controller is studied by varying the timing parameters above. Firstly, the controller is assigned the SCSI number 7 and the throughput of each disk is observed under increasing load. The throughput of the low priority disk may collapse if the bus delay is long and load is heavy. The high priority disk does not exhibit such a phenomenon, which reveals the unfairness of the arbitration mechanism. Secondly, the effect of the controller SCSI number on the disk throughputs is studied. If the controller is in the lowest position (SCSI number 0), the low and high priority disk throughputs are rather balanced, and there is no degradation of the low priority throughput.

Conclusions: A practical methodology was presented for studying the performance of a concurrent system starting from an already verified functional specification of this system. The approach is original in several respects: (a) it does not define a new formalism for modelling stochastic systems, but relies on the existing LOTOS formal description technique, adapted to the stochastic framework by adding timing information; (b) the CADP tools are used for constructing the LTS of the LOTOS specifications, and BCG_MIN is used to minimize these LTSs in the stochastic setting; (c) automation of the performance experiments is achieved by means of the SVL scripting language, which allows to integrate various tools transparently.

Publications: [Garavel-Hermanns-02] Hubert Garavel and Holger Hermanns. "On Combining Functional Verification and Performance Evaluation using CADP". In Lars-Henrik Ericsson and Peter A. Lindsay, editors, Proceedings of the 11th International Symposium of Formal Methods Europe FME'2002 (Copenhagen, Denmark), Lecture Notes in Computer Science vol. 2391, pp. 410-429. Springer Verlag, July 2002. Full version available as INRIA Research Report 4492.
Available on-line at: http://cadp.inria.fr/publications/Garavel-Hermanns-02.html
Contact:
Hubert Garavel
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 52 24
Fax: +33 (0)4 76 61 52 52
E-mail: Hubert.Garavel@inria.fr
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page