Hayman, Jonathan and Winskel, Glynn - Independence and concurrent separation logic

lmcs:1100 - Logical Methods in Computer Science, March 19, 2008, Volume 4, Issue 1
Independence and concurrent separation logic

Authors: Hayman, Jonathan and Winskel, Glynn

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.


Source : oai:arXiv.org:0802.0820
DOI : 10.2168/LMCS-4(1:6)2008
Volume: Volume 4, Issue 1
Published on: March 19, 2008
Submitted on: April 10, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.2,F.3.1,D.3.1,F.1.2


Share

Consultation statistics

This page has been seen 60 times.
This article's PDF has been downloaded 22 times.