Runtime Verification of Interleaved Concurrent Systems with Shared-Variable Communication
Abstract
The paper introduces a comprehensive framework for parallel runtime verification designed to monitor concurrent systems that utilise shared-variable communication mechanisms operating under interleaved concurrency model. The proposed framework validates system behaviour during execution to confirm adherence to correctness specifications or identify violations thereof. Concurrent systems necessitate distinct correctness criteria compared to sequential programs, particularly regarding deadlock avoidance and mutual exclusion protocols when multiple processes access shared resources under interleaved concurrency models. Traditional sequential verification frameworks lack the architectural capability to monitor parallel systems effectively, as they are fundamentally designed to track single processes rather than multiple concurrent processes executing simultaneously. This work addresses various challenges in ensuring correctness of parallel programs at both hardware and software layers while providing a theoretical analysis comparing verification methodologies including theorem proving, model checking, testing, and runtime verification. The framework uses Interval Temporal Logic (ITL) as its formal foundation alongside its expressive power for specifying complex temporal properties of parallel systems. A detailed exposition of the framework's core components, their operational roles, and their integration within the overall verification architecture is presented, demonstrating the practical applicability of runtime verification techniques for ensuring correctness in parallel computing environments.