Verification of a multicore programming library

Abstract

As the demand for high performance software is constantly increasing, the need to develop multicore software is increasing, too. This results in degraded reliability of software and increased veri cation e ort since multicore software has potentially more than one execution schedule. Veri cation approaches for eliminating errors in sequential software are not adequate for full coverage of errors in multicore software. We need not only concurrency aware but also e cient and scalable veri cation methods for multicore software. We present veri cation and coverage methods for multicore software that uses message passing libraries for communication. Speci cally, we provide techniques to improve reliability of software using the new industry standard Multicore Communication API (MCAPI) by the Multicore Association. We develop dynamic predictive veri cation techniques that allow us to nd actual and potential errors in a multicore software. Some of these error types are deadlocks, race conditions, and violation of temporal assertions. We complement our veri cation techniques with a mutation testing based coverage metric. Coverage metrics enable measuring the quality of veri cation test sets. We implemented our techniques in tools and validated them on several multicore programs that use MCAPI standard. We experimentally show the e ectiveness of our methods. We show that our veri cation tool automatically veri es multicore programs and nds violation of temporal assertions, list of potential deadlocks, and race conditions. We nd errors that are not found using traditional dynamic veri cation techniques. Our coverage tool helps to improve the quality of veri cation test sets for multicore programs. Furthermore, we can potentially explore execution schedules di erent than the original execution with our coverage tool.