Differences between revisions 1 and 3 (spanning 2 versions)
⇤ ← Revision 1 as of 2011-02-03 20:11:25 →
Size: 22
Editor: viktor
Comment:
← Revision 3 as of 2011-02-03 20:29:04 → ⇥
Size: 1439
Editor: viktor
Comment:
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:
Describe RGSep here. = RGSep/SAGL/LRG =

These three program logics are very similar to one another and are thus described together.

 * RGSep ([[http://www.mpi-sws.org/~viktor/papers/concur2007-marriage.pdf|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 [[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.
 * Local Rely Guarantee (LRG) is an extension of RGSep by [[http://staff.ustc.edu.cn/~xyfeng/research/publications/LRG.pdf|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 ====

 * [[http://www.mpi-sws.org/~viktor/papers/concur2007-marriage.pdf|A Marriage of Rely/Guarantee and Separation Logic]]. V Vafeiadis, M Parkinson. CONCUR 2007.
 * [[http://flint.cs.yale.edu/flint/publications/sagl.html|On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning]]. X. Feng, R. Ferreira, Z. Shao. ESOP 2007.
 * [[http://staff.ustc.edu.cn/~xyfeng/research/publications/LRG.pdf|Local Rely Guarantee Reasoning]]. X. Feng. POPL 2009.

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

RGSep (last edited 2011-02-03 20:29:04 by viktor)