Independence and concurrent separation logic

TL;DR

This paper introduces a Petri net-based semantics for a language with pointer manipulation and parallelism, providing a formal foundation for concurrent separation logic and enabling process independence analysis.

Contribution

It offers a novel Petri net model that formalizes validity and independence in concurrent separation logic, enhancing understanding of process interactions and refinement capabilities.

Findings

Soundness of concurrent separation logic rules established

Petri net model captures process independence effectively

Refinement operation adjusts atomic action granularity

Abstract

A compositional Petri net-based semantics is given to a simple language allowing pointer manipulation and parallelism. The model is then applied to give a notion of validity to the judgements made by concurrent separation logic that emphasizes the process-environment duality inherent in such rely-guarantee reasoning. Soundness of the rules of concurrent separation logic with respect to this definition of validity is shown. The independence information retained by the Petri net model is then exploited to characterize the independence of parallel processes enforced by the logic. This is shown to permit a refinement operation capable of changing the granularity of atomic actions.