Proving Correctness of Parallel Implementations of Transition System Specifications
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.
Cite
@article{arxiv.2302.04661,
title = {Proving Correctness of Parallel Implementations of Transition System Specifications},
author = {Frank S. de Boer and Einar Broch Johnsen and Violet Ka I Pun and Silvia Lizeth Tapia Tarifa},
journal= {arXiv preprint arXiv:2302.04661},
year = {2023}
}