Paper Info
Title
MCC: A runtime verification tool for MCAPI user applications
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 tailor- made dynamic partial order reduction algorithm (DPOR). Our contributions are (i) to understand the MCAPI semantics, (ii) model the non-overtaking message matching relation under- lying MCAPI calls, (iii) design a high level algorithm to effect DPOR for MCAPI, and (iv) engineer the lower level details so that the intended executions happen at runtime. We also identify several default safety properties that can be automat- ically generated. This is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. We identified that every MCAPI connection-less type receive call is non-deterministic, and to solve this problem, we compute all possible non-deterministic communication matches at runtime. Our results are (i) the demonstration that we can indeed develop a dynamic model checker for MCAPI, and that (ii) the attempt to design a dynamic verifier of an API that has not yet seen much use may reveal additional verification/debugging oriented API calls that can be invaluable.
Year
DOI
Venue
2009
10.1109/FMCAD.2009.5351145
FMCAD
Keywords
Field
DocType
mcc,runtime verification,formal verification,message passing,partial order reduction
Yarn,Programming language,Model checking,Computer science,Runtime verification,Real-time computing,MCAPI,Partial order reduction,Multi-core processor,Message passing,Formal verification
Conference
Citations 
PageRank 
References 
12
0.67
4
Authors
4
Name
Order
Citations
PageRank
Subodh Sharma1705.99
Ganesh Gopalakrishnan21619130.11
eric mercer312511.06
Jim Holt4181.91