= 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.