Architectural support for runtime verification on ccNUMA multiprocessors

This paper presents a runtime verification (RV) framework on distributed shared-memory multiprocessors based on explicit functional/concurrency intent specification in the form of temporal logic properties. A generic programming model, that subsumes task and data parallelism, has been wrought along with an automata-based formulation of the RV problem. Algorithms are implemented for the construction and minimization of automata checkers that can be executed concurrently with multithreaded applications to assert their correct functioning. The needed architectural supporting mechanisms and the ensuing design tradeoffs are investigated using an approximately-timed transaction-level model. The simulation model confirms scalability of the proposed RV approach to large multiprocessor systems. It also quantifies the increase in the number of processors needed to replenish the monitoring-induced performance degradation.