Proving Correctness of Parallel Implementations of Transition System Specifications

TL;DR

This paper introduces a novel method for verifying the correctness of parallel programs by using simulation relations and a global confluence property within an active object model, demonstrated on multicore memory system simulators.

Contribution

It presents a new approach for proving correctness of parallel systems using simulation relations and confluence properties in an active object framework.

Findings

Successfully verified a parallel multicore memory system simulator.

The method abstracts fine-grained interleavings using confluence properties.

Demonstrated the effectiveness of the approach on real-world parallel systems.

Abstract

The overall problem addressed in this paper is the long-standing problem of program correctness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent) objects. The method defines correctness in terms of a simulation relation between the transition system which specifies the program semantics and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the particular model of active objects considered in this paper. As a proof-of-concept we apply our method to the correctness of a parallel simulator of multicore memory systems.