Differences between revisions 2 and 3
Revision 2 as of 2011-02-03 20:27:10
Size: 1416
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 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

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