Paper: Independence and Concurrent Separation Logic (at LICS 2006)

Authors: Jonathan Hayman Glynn Winskel

Abstract

A compositional Petri net based semantics is given to a simple pointer-manipulating language. The model is then applied to give a notion of validity to the judgements made by concurrent separation logic that emphasizes the processenvironment 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.

BibTeX

  @InProceedings{HaymanWinskel-IndependenceandConc,
    author = 	 {Jonathan Hayman and Glynn Winskel},
    title = 	 {Independence and Concurrent Separation Logic},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {147--156},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }