DocumentCode :
2510304
Title :
Independence and Concurrent Separation Logic
Author :
Hayman, Jonathan ; Winskel, Glynn
Author_Institution :
Comput. Lab., Cambridge Univ.
fYear :
0
fDate :
0-0 0
Firstpage :
147
Lastpage :
156
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 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
Keywords :
Petri nets; concurrency theory; parallel programming; programming language semantics; refinement calculus; compositional Petri net based semantics; concurrent separation logic; parallel process independence; pointer-manipulating language; process-environment duality; refinement operation; rely-guarantee reasoning; Concurrent computing; Hardware; Interleaved codes; Joining processes; Laboratories; Logic programming; Parallel languages; Parallel programming; Spatial resolution; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2006 21st Annual IEEE Symposium on
Conference_Location :
Seattle, WA
ISSN :
1043-6871
Print_ISBN :
0-7695-2631-4
Type :
conf
DOI :
10.1109/LICS.2006.30
Filename :
1691226
Link To Document :
بازگشت