Runtime Verification of k-Mutual Exclusion for SoCs

We present an efficient runtime verification environment for detecting mutual exclusion predicates. Such predicates are important for keeping the safe operation of concurrent systems. Our environment models execution traces as partial order traces to increase scalability in runtime verification. We compare two techniques implemented in POTA tool, namely k-exclusion and computation slicing. The k-exclusion problem is a generalization of the mutual exclusion problem in which up to k processes may be in their critical sections at the same time. Our k-exclusion algorithm exploits the fact that if there is a k-exclusion violation then it is impossible to partition events from critical sections into k queues. We earlier presented efficient computation slicing algorithms to detect predicates from a subset of temporal logic CTL. We performed experiments using POTA tool on scalable protocols. Our comparison shows that k-exclusion is substantially better than slicing both in terms of time and space. In all fairness, slicing handles general class of predicates from temporal logic CTL, whereas k-exclusion algorithm handles only a very specific, nonetheless useful, class of mutual exclusion predicates.