| 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.
|
 Additional Information
|
Citation:
Jonathan Hayman, Glynn Winskel,
"Independence and Concurrent Separation Logic,"
lics,
pp. 147-156,
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06),
2006
|
