Parallel Runtime Verification For Multithreaded Programs

Modern operating systems,embedded systems,avionics systems and other safety systems are generally developed using C/C++ language,so the research of runtime verification for C programs become very important.Mainstream runtime verification mainly aims at the memory safety and formal specification of programs.Firstly,the code related to memory operations and specifications in C program is instrumented,and then the C program is compiled and run to verify whether the oriented program meets the memory safety and the given specifications.But the existing technologies have many limitations.On the one hand,most of the existing technologies can only deal with single-threaded C programs.For multi-threaded C programs,they may cause the problem of competitive accesses to runtime information,resulting in erroneous verification results.On the other hand,runtime verification for formal specifications mostly deal with multiple monitors in a serialized manner.When the number of specifications is large,the serialized operation of multiple monitors will lead to a significant reduction in runtime performance.In view of the above two limitations,this paper mainly studies the runtime verification for multithreaded C programs and the parallel verification technology for multiple monitors.Our work and innovations include:Firstly,we propose a runtime verification algorithm for multi-threaded C programs to defect the memory safety errors.The algorithm uses hashtables with locks or lock-free hashtables to insert,search and delete pointer metadata,so that the multi-threaded C programs after instrumentation can access pointer metadata concurrently,thus realizing the runtime verification of memory safety of multithreaded C program.Secondly,we propose a formal specification verification algorithm for multi-threaded C programs.The algorithm uses lock-free queue to store and process the events generated by the program,and performs enqueueing and dequeueing,so that the multi-threaded C program after instrumentation can access the event generated by the program concurrently,thus realizing the runtime verification of the formal specifications of mult-ithreaded C program.Thirdly,for the verification of multiple monitors,we propose a parallel verification algorithm.The basic principle is to distribute the monitor generated by specifications to multiple threads equally according to the number of specifications and the number of threads,and accomplishs the interactions between user threads and monitor threads by semaphores,thus realizing multiple monitors parallel verification.Finally,based on the new verification algorithm,we implement the tool Movec,and compare it with the existing technologies on MiBench and SARD test sets.Experimental results show that Movec can detect more safety errors than Addresssanitizer.The runtime overload generated by using hashtable with locks is positively related to the number of threads to be verified,while the runtime overload generated by using lock-free hashtable is independent of the number of threads to be verified.For formal specifications verification,the parallel runtime verification of formal specifications for multi-threaded C program is implemented by using lock-free queue and parallel verification.The experimental results show that the runtime overload generated by the multiple monitors parallel verification algorithm is about 40% less than that of the serialized verification algorithm.