Marrella: A tool for simulation and verification

Abstract

This paper presents the structure of our tool Marrella the construction of which has been motivated by practical problems in the context of simulation and parallel program debugging, where the correct evaluation of global properties requires a careful analysis of the causal structure of the execution. The underlying model is based on prime event structures that are considered as exhibiting all the behaviors of distributed programs: the tool gives the possibilities of generating one, some or all of their executions. On one hand, a careful implementation spares memory; on the other hand, precise and neat algorithms benefit from the trace properties of prime event structures and thus gain in avoiding the enumerations of equivalent interleavings.