A 2-Phase Method for Validation of Matching Pair Property with Case Studies of Operating Systems

Memory leaks, asymmetric synchronization, and several other defects are examples of violation of the matching pair (MP) property. The property involves matching between two types of events on every execution path. We present a practical method to validate the MP property for large software. The method is designed to address the validation challenges resulting from the cross-cutting semantics and presence of invisible control flow. The method has two phases: the macro analysis and the micro analysis. The macro analysis phase incorporates important notions of signature and matching pair graph (MPG). Signatures enable a decomposition of the problem into small independent instances for validation, each identified by a unique signature. The MPG(x) defines for each signature x a minimal set of functions to be analyzed for validating the instance given by signature x. The micro analysis phase produces the event traces on all relevant execution paths through the functions belonging to a MPG(x). A fast and accurate analysis of large software is possible because the macro analysis can exactly identify the functions that need to be analyzed and the micro analysis can efficiently compute all the relevant event traces. We demonstrate the method through case studies of the Xinu and the Linux kernels.