Keywords

MCC, Multicore Communication, API applications, MCAPI, verification tool

Abstract

We present a dynamic verification tool MCC for Multicore Communication API applications – a new API for communication among cores. MCC systematically explores all relevant interleavings of an MCAPI application using a tailormade dynamic partial order reduction algorithm (DPOR). Our contributions are (i) a way to model the non-overtaking message matching relation underlying MCAPI calls with a high level algorithm to effect DPOR for MCAPI that controls the lower level details so that the intended executions happen at runtime; and (ii) a list of default safety properties that can be utilized in the process of verification. To our knowledge, this is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. Our result is the demonstration that we can indeed develop a dynamic model checker for MCAPI that can directly control the non-deterministic behavior at runtime that is inherent in any implementation of the library without additional API modifications or additions.

Original Publication Citation

S. Sharma, G. Gopalakrishnan, E. Mercer, and J. Holt, "MCC - A runtime verification tool for MCAPI user applications", in Proceedings of Formal Methods in Computer Aided Design (FMCAD), Austin, USA, November 29.