Ten Years of Performance Evaluation for Concurrent Systems Using CADP

This article comprehensively surveys the work accomplished during the past decade on an approach to analyze concurrent systems qualitatively and quantitatively, by combining functional verification and performance evaluation. This approach lays its foundations on semantic models, such as

Imc

(

Interactive Markov Chain

) and

Ipc

(

Interactive Probabilistic Chain

), at the crossroads of concurrency theory and mathematical statistics. To support the approach, a number of software tools have been devised and integrated within the

Cadp

(

Construction and Analysis of Distributed Processes

) toolbox. These tools provide various functionalities, ranging from state space generation (

Cæsar

and

Exp.Open

), state space minimization (

Bcg_Min

and

Determinator

), numerical analysis (

Bcg_Steady

and

Bcg_Transient

), to simulation (

Cunctator

). Several applications of increasing complexity have been successfully handled using these tools, namely the Hubble telescope lifetime prediction, performance comparison of mutual exclusion protocols, the

Scsi

-2 bus arbitration protocol, the Send/Receive and Barrier primitives of

Mpi

(

Message Passing Interface

) implemented on a cache-coherent multiprocessor architecture, and the

xSTream

multiprocessor data-flow architecture for embedded multimedia streaming applications.