2023-01-25
Proving correctness of parallel implementations of transition system specifications
Publication
Publication
The overall problem addressed in this paper is the long-standing problem of program correct- ness, 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) ob- jects. 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.
| Additional Metadata | |
|---|---|
| doi.org/10.48550/arXiv.2302.04661 | |
| Organisation | Computer Security |
|
de Boer, F., Johnsen, E. B., Pun, V. K., & Tapia Tarifa, L. (2023). Proving correctness of parallel implementations of transition system specifications. doi:10.48550/arXiv.2302.04661 |
|
