1416
Comment:
|
← Revision 3 as of 2011-02-03 20:29:04 ⇥
1439
|
Deletions are marked like this. | Additions are marked like this. |
Line 6: | Line 6: |
* SAGL is a variant of RGSep developed independently and concurrently by [[http://flint.cs.yale.edu/flint/publications/sagl.html|Feng, Ferreira, and Shao (2007)]] and is presented as a program logic for concurrent assembly programs. | * SAGL is a similar combination of rely-guarantee and separation logic developed by [[http://flint.cs.yale.edu/flint/publications/sagl.html|Feng, Ferreira, and Shao (2007)]] in parallel and is presented as a program logic for concurrent assembly programs. |
RGSep/SAGL/LRG
These three program logics are very similar to one another and are thus described together.
RGSep (Vafeiadis and Parkinson 2007) is a combination of rely-guarantee reasoning and separation logic.
SAGL is a similar combination of rely-guarantee and separation logic developed by Feng, Ferreira, and Shao (2007) in parallel and is presented as a program logic for concurrent assembly programs.
Local Rely Guarantee (LRG) is an extension of RGSep by Feng (2009) that supports hiding spatially separate rely-guarantee conditions. In LRG, rely and guarantee are 'fenced' by a precise resource invariant. The same effect without the precision requirement can be obtained in RGSep by having multiple resources as in CSL.
Papers
A Marriage of Rely/Guarantee and Separation Logic. V Vafeiadis, M Parkinson. CONCUR 2007.
On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning. X. Feng, R. Ferreira, Z. Shao. ESOP 2007.
Local Rely Guarantee Reasoning. X. Feng. POPL 2009.