Parallel Runtime Verification Approach for Alternate Execution of Multiple Threads

摘要

Since resources are shared by threads created in a multithreaded program, these threads are not completely independent of each other. The execution of these threads usually needs to satisfy a certain order restriction. In this paper, we employ a multi-core machine based parallel runtime verification approach to efficiently monitor the alternate execution of multiple threads. First, the problem is described in Modeling, Simulation and Verification Language (MSVL). Second, the desired periodically repeated property is specified by a Prepositional Projection Temporal Logic (PPTL) formula. Third, the state sequence generated by the execution of the MSVL program is divided into several segments which are verified in parallel. Finally, verification results for different segments are merged. Experimental results show that the alternate execution of multiple threads implemented through invoking Windows Application Programming Interface (API) functions SuspendThread and ResumeThread will lead to these threads out of sequence.