FormalFame 2003 Activity Report



This page is an excerpt from the VASY project activity report for year 2003. It is composed of the parts that concern the FORMALFAME contract.


BULL Jack Abily
Sylvie Lesmanne (project leader)
Solofo Ramangalahy
Yehong Xing
INRIA / VASY Damien Bergamini (software engineer)
Hubert Garavel (research director)
Radu Mateescu (research scientist)


Since 1995, there has been a long-standing collaboration of VASY and BULL, to which the former PAMPA team of INRIA Rennes participated until December 2000. This collaboration aims at demonstrating that the formal methods and tools developed at INRIA for validating and testing telecommunication protocols can also be successfully applied to BULL's multiprocessor architectures. The long-term objective is to develop a complete and integrated solution supporting formal specification, simulation, rapid prototyping, verification, test generation, and test execution.

A first phase of this collaboration took place from 1995 to 1998 in the framework of the DYADE joint venture between BULL and INRIA. Two case studies were successfully tackled: the POWERSCALE bus arbitration protocol and the POLYKID multiprocessor architecture. The feasibility of the proposed approach was established and BULL expressed its interest in pursuing the collaboration for its new architectures.

Since October 1998, we have been working on FAME, the CC-NUMA multiprocessor architecture developed by BULL for its NOVASCALE series of high-performance servers based on INTEL ITANIUM 64 bits processors. Initially informal, this collaboration was officialized in 1999 as a DYADE action named FORMALFAME, which lasted until the end of DYADE in March 2001. Since then, the collaboration is going on under the form of a BULL-INRIA contract, for which we kept the name FORMALFAME. This contract gathers VASY team and the BULL team of Sylvie Lesmanne (who succeeded Anne Kaszynski in March 2002) in Les Clayes-sous-Bois, the coordination being ensured by a BULL engineer (M. Zendri, then N. Zuanon, then S. Ramangalahy) located at INRIA Rhône-Alpes.

FORMALFAME successively focused on several critical components of the FAME architecture: the CCS circuit that manages communications for a group of four processors and the NCS circuit that manages network communications (from October 1998 to November 1999), the B-SPS circuit that implements the cache coherency protocol (from December 1999 to March 2002), and, since then, the PRR block and the ILU unit, which are two sub-components of the B-SPS circuit to which a particular attention is drawn. For each of these components, LOTOS descriptions were written, which provided a formal basis for testing and verification.

In 2003, the results obtained by FORMALFAME concern, on the one hand, the validation and testing of PRR and ILU and, on the other hand, the improvement of various CADP tools.

Progress report

Since October 1998, we have been co-operating with BULL in the framework of the FORMALFAME contract devoted to the use of formal methods for verifying and testing multiprocessor architectures. Our work targets at FAME, the CC-NUMA architecture developed by BULL for its NOVASCALE series of high-performance servers based on 64 bits INTEL ITANIUM processors. The core of FAME is a complex circuit (named B-SPS), which implements the FAME cache coherency protocol and performs routing between processors and input/output nodes. The complexity of this circuit comes both from the internal parallelism inherent to routing and from multiple accesses to shared data, the consistency of which must be preserved.

After studying the B-SPS as a whole (1999-2002), FORMALFAME currently focuses on two complex sub-components of B-SPS: the PRR (Pending Request Responses) block and the ILU (InterLeaving) unit, which are modeled and analyzed in great detail. In 2003, work took place in two directions:

Back Back to the VASY Home Page