MULTIVAL Progress Report 2011
by the VASY project team at INRIA

This page is an excerpt from the VASY project-team activity report for the year 2011 created by selecting those parts related to the MULTIVAL project. Thus, it is not intended to cover all activities performed in MULTIVAL, but only those in which the VASY project team has been involved.

In 2011, the VASY project team contributed to MULTIVAL by focussing our activities on the enhancement of CADP and, in collaboration with our partners, on the verification of the Dynamic Task Dispatcher.

1. VASY team members participating in MULTIVAL

in close collaboration with

2. Study of the Dynamic Task Dispatcher (STMicroelectronics)

STMicroelectronics studied Platform 2012, a many-core programmable accelerator for ultra-efficient embedded computing in nanometer technology. This flexible and configurable multi-cluster platform fabric targets a range of emerging video, imaging, and next-generation immersive multimodal applications. Configurability options include the number of clusters, the number and type of processing elements (PE) per cluster, specialization of the architecture and instruction-set of the PEs, and finally, support of hardware-accelerated PEs. The platform is supported by a rich programming environment which embodies a range of platform programming models.

In 2011 we focused on the DTD (Dynamic Task Dispatcher) hardware block that assigns a set of application tasks on a set of PEs. It is called dynamic because each task itself might add tasks to the set of those to be dispatched by the DTD. The DTD is synthesized from a C++ model, optimized to generate an efficient hardware block. Due to the intrinsic complexity of the DTD, STMicroelectronics was interested in the co-simulation of this C++ code with a formal model of the DTD.

In a first step, we generalized the LOTOS NT model of the DTD developed in 2010 to allow the handling of an arbitrary number of PEs (1,200 lines of LOTOS NT). We also modeled as LOTOS NT processes the different sets of tasks corresponding to various applications. To express the operations provided by the DTD, we had to include a call-stack in the model of each PE, as a means of circumventing the static-control constraints of CÆSAR forbidding recursion over parallel composition. STMicroelectronics judged LOTOS NT to be essential in modeling the DTD, because using LOTOS instead would have been extremely difficult, requiring complex continuations with numerous parameters. We also wrote twelve scenarios (1,000 lines of LOTOS NT) describing applications to be dispatched by the DTD. For each scenario and for up to six PEs, we generated the corresponding LTS (up to 100 million states and 500 million transitions).

Then, for each generated LTS, we verified several properties, such as the correctness of assertions inserted in the model (by checking the set of transition labels), the termination of the scenario, or that each task is executed exactly once. We expressed the latter properties using the MCL language [MT08] and verified them using the EVALUATOR 4 model checker. This allowed us to point out a difference between our implementation and the one from the architect, highlighting a high sensibility on the order of terms in an equation, revealing an under-specified mechanism. We also verified the correctness of a complex optimization.

Having gained confidence in the LOTOS NT model, we applied the EXEC/CÆSAR framework to co-simulate the C++ and LOTOS NT models of the DTD, a challenge being the connection of the asynchronous LOTOS NT model with the synchronous C++ model, because one step of the C++ model corresponds, in general, to several transitions of the LOTOS NT model.

This case study enabled us to discover and correct a few bugs in CADP and led to a publication in an international conference [LS11].

3. Compilation of LOTOS

The CADP toolbox contains several tools dedicated to the LOTOS language, namely the CÆSAR.ADT compiler for the data type part of LOTOS, the CÆSAR compiler for the process part of LOTOS, and the CÆSAR.INDENT pretty-printer.

In 2011, in addition to fixing four bugs in the CÆSAR and CÆSAR.ADT compilers, we improved the LOTOS dedicated tools of CADP as follows:

• We revised the predefined type libraries and C code generated by CÆSAR and CÆSARADT to suppress warnings emitted by recent versions of GCC.

• We enhanced the format in which values of singleton and tuple types are displayed to end users.

• We modified the predefined libraries for natural (unsigned) and integer (signed) types so that users can now indicate the precise number of bits (between 1 and 64) to be used for the machine representation of these types, and can also determine the precise range (lower and upper bound) to be used for values of these types.

• We further modified these two libraries to enable (optional) overflow and underflow checking during arithmetic operations on the natural and integer types.

4. Translation from LOTOS NT to LOTOS

The LNT2LOTOS, LNT.OPEN, and LPP tools convert LOTOS NT code to LOTOS, thus allowing the use of CADP to verify LOTOS NT descriptions. These tools are officially part of CADP since 2010 and have been used successfully for many different systems (including the Dynamic Task Dispatcher).

In 2011, we continued enhancing these tools, of which we delivered four new releases. In addition to 13 bug fixes, the following enhancements have been brought:

• The LOTOS NT language was extended with range types (which are interval subtypes of character, integer, or natural types) and predicate types (which are subtypes of existing types, a boolean predicate being used to determine the domain of each subtype).

• The LOTOS NT language was enriched with the concept of "module pragmas", which specify implementation constraints for predefined types such as naturals, integers, and strings. Also, the predefined operations "first" and "last" have been added for enumerated types.

• The LNT2LOTOS translator was made semantically stricter by adding checks for overflow and underflow when doing natural and integer arithmetics, checking that range type bounds and array type bounds belong to the domain of admissible values for their parent types, and adding additional checks for type pragmas.

• The LOTOS code generated by the LNT2LOTOS translator was optimized by handling equation premises (in the data part) and boolean guards (in the behavior part) that are always false or always true. Other optimizations have been added for process definitions whose bodies are empty or only contain a call to another process, for "case" statements that are followed by no instruction or only a "null" instruction, and for "while" loops with an empty body.

• The speed of processing LOTOS NT specifications containing several modules has been made between two and three times faster.

• The error and warning messages issued by the LOTOS NT tools have been enhanced.

• The reference manual has been corrected, reorganized and comprehensively edited. Two new appendices have been added, one that lists all the predefined functions, and another one (20 pages) giving the formal semantics of LOTOS NT.

5. Mastering the Software Quality of the CADP tools

To support the usage of CADP in industry and academia, we pursued our efforts to master the software quality of CADP:

• We added support for Mac OS X 10.7 ("Lion") and enhanced the documentation for Mac OS X.

• We corrected one bug in the INSTALLATOR installation assistant, two bugs in the TST platform-checking command, and brought two bug fixes and one usability enhancement in the EUCALYPTUS graphical user-interface. We also provided a workaround for supporting recent versions of UBUNTU.

• We continued building a comprehensive validation framework, based on non-regression testing and semantical checking for the CADP tools. This framework allows functional testing of individual tools as well as integration testing for several CADP tools used together to perform complex verification scenarios on various computing platforms and using various compilers.

6. Other enhancements to the CADP tools

Finally, there have been significant software developments done in MULTIVAL that will not be detailed here, since they are not immediately visible to the industrial users of the CADP tools. More information can be found in the corresponding sections of the VASY project team activity report for 2011. Notable changes include:

• Enhancements to the BCG format and libraries (section 6.1.1)

• Enhancements to CÆSAR_SOLVE and the OPEN/CÆSAR libraries (section 6.1.2)

• Enhancements to the Evaluator tool (section 6.1.3)

• Enhancements to the compositional verification tools EXP.OPEN, PROJECTOR, BCG_MIN, and SVL (section 6.1.4)

• Enhancements to the distributed verification tools DISTRIBUTOR and BCG_MERGE, and the addition of the PBG_CP, PBG_INFO, PBG_MV, and PBG_RM tools (section 6.1.5)

7. References

[LS11]

Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP.
Etienne Lantreibecq and Wendelin Serwe.
Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2011 (Trento, Italy), G. Salaün and B. Schätz (editors), Lecture Notes in Computer Science, Springer Verlag, August 2011, vol. 6959, p. 180-195.

[MT08]

A Model Checking Language for Concurrent Value-Passing Systems.
Radu Mateescu and Damien Thivolle.
Proceedings of the 15th International Symposium on Formal Methods FM'08 (Turku, Finland), J. Cuellar, T. Maibaum, and K. Sere (editors), Lecture Notes in Computer Science, Springer Verlag, May 2008, vol. 5014, p. 148-164.