Differences between revisions 1 and 54 (spanning 53 versions)
⇤ ← Revision 1 as of 2011-05-03 11:39:10 →
Size: 4583
Editor: viktor
Comment:
← Revision 54 as of 2011-07-25 23:44:25 → ⇥
Size: 7809
Editor: dreyer
Comment:
Deletions are marked like this. Additions are marked like this.
Line 3: Line 3:
'''Instructors:''' Viktor Vafeiadis and Derek Dreyer
'''Meeting Time:''' 2 hours, once a week		 '''Instructors:''' [[http://www.mpi-sws.org/~viktor|Viktor Vafeiadis]] and [[http://www.mpi-sws.org/~dreyer|Derek Dreyer]]

'''Teaching assistant:''' [[http://www.mpi-sws.org/~neis|Georg Neis]]

'''Meeting time:''' 2 hours, once a week, April - July 2011
Line 14: Line 17:
== Preliminary Schedule == == Schedule ==
Line 16: Line 19:
Monday 2011-04-11, 12:15. Introduction, Hoare logic (Viktor) [slides]
Monday 2011-04-17. No meeting (Easter holiday)
Monday 2011-04-25. No meeting (Easter holiday)
Monday 2011-05-02, 16:15. Owicki-Gries (Jonas) [simple examples]
Monday 2011-05-09, 16:15. Rely-guarantee (Georg)
Monday 2011-05-16, 16:15. Separation logic (Sigurd)
Monday 2011-05-23, 12:15. Concurrent separation logic
Monday 2011-05-30, 16:15. Permissions
Monday 2011-06-06, 16:15. Abstract predicates
Monday 2011-06-13, 16:15. Storable locks
Monday 2011-06-20. No meeting (LICS)
Monday 2011-06-27, 16:15. RGSep
Monday 2011-07-04, 16:15. More RGSep, LRG
Monday 2011-07-11, 16:15. Deny-guarantee
Monday 2011-07-18, 16:15. Concurrent abstract predicates
Monday 2011-07-25, 16:15. More DG		 || '''Date and time''' || '''Topic''' || '''Presenter''' || '''Files''' ||
|| Monday 2011-04-11, 12:15.|| Introduction, Hoare logic || Viktor || [[attachment:cpl1.pdf|slides]] ||
|| Monday 2011-04-17. |||||| ''No meeting (Easter holiday)'' ||
|| Monday 2011-04-25. |||||| ''No meeting (Easter holiday)'' ||
|| Monday 2011-05-02, 16:15. || Owicki-Gries || Jonas || [[attachment:slides-jonas-2011-05-02.pdf|slides]] [[attachment:owicki-example.pdf|example]] ||
|| Monday 2011-05-09, 16:15. || Rely-guarantee || Georg || [[attachment:slides-georg-2011-05-09.pdf|slides]] [[attachment:notes-2011-05-09.txt|example]] ||
|| Monday 2011-05-16, 16:15. || Separation logic || Sigurd || [[http://www.ps.uni-saarland.de/~sdschn/pdfs/sep.pdf|slides]] ||
|| Monday 2011-05-23, '''''12:15'''''. || Concurrent separation logic || Beta || [[attachment:slides-beta-2011-05-23.pdf|slides]] [[attachment:example-wehrman.pdf|counter-example]] ||
|| Monday 2011-05-30, 16:15. || Permissions || Matt || [[attachment:2011-05-30--CPL--Permissions.pdf|slides(M)]] [[attachment:slides-cslsound.pdf|slides(V)]] ||
|| Monday 2011-06-06, 16:15. || Abstract predicates || Scott || [[attachment:slides-scott-2011-06-06.pdf|slides]] ||
|| '''Thursday 2011-06-16, 16:15.''' || Storable locks || Derek || ||
|| Monday 2011-06-20. |||||| ''No meeting (LICS)'' ||
|| '''Thursday 2011-06-30, 16:15.''' || RGSep, LRG || Arthur || [[attachment:slides-arthur-2011-06-30.pdf|slides]] ||
|| Monday 2011-07-04, 16:15.|| More RGSep, SmallfootRG || Viktor + Arthur || [[http://www.mpi-sws.org/~viktor/rgsl-tutorial/part3.pdf|slides(V)]] [[attachment:slides-arthur-2011-07-04.pdf|slides(A)]] ||
|| Monday 2011-07-11. |||||| ''No meeting (POPL deadline)'' ||
|| Monday 2011-07-18, 16:15.|| Deny-guarantee || Georg || [[attachment:slides-georg-2011-07-18.pdf|slides]] ||
|| '''Thursday 2011-07-21, 16:15.''' || Concurrent abstract predicates || Gil || [[attachment:slides-gil-2011-07-21.pdf|slides]] ||
|| '''Thursday 2011-08-04, 16:15.''' || Concurrent abstract predicates (continued) || Gil || ||
Line 37: Line 42:
C.A.R. Hoare: An axiomatic basis for computer programming. CACM 1969.
Susan Owicki, David Gries: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319-340 (1976)
Rely/guarantee		  * C.A.R. Hoare: An axiomatic basis for computer programming. CACM 1969.
 * Susan Owicki, David Gries: [[attachment:owicki.pdf|An axiomatic proof technique for parallel programs I.]] Acta Informatica 6, 319-340 (1976)
Line 41: Line 45:
Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis. Sections 2.2 and 2.3 only. [entire thesis]
Joey W. Coleman and Cliff B. Jones: A structural proof of the soundness of rely/guarantee rules Journal of Logic and Computation 17: 807-841 (2007)
Leonor Prensa Nieto. The rely-guarantee method in Isabelle/HOL. ESOP 2003.		 === Rely/guarantee ===

 * Viktor Vafeiadis: Modular fine-grained concurrency verification. PhD thesis. [[attachment:vthesis-rg.pdf|Sections 2.2 and 2.3 only.]] ([[http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf|entire thesis]])
 * Joey W. Coleman, Cliff B. Jones: [[http://homepages.cs.ncl.ac.uk/j.w.coleman/papers/colemanjones-rg-soundness.pdf|A structural proof of the soundness of rely/guarantee rules.]] Journal of Logic and Computation 17: 807-841 (2007)
 * Leonor Prensa Nieto: [[attachment:prensa.pdf|The rely-guarantee method in Isabelle/HOL.]] ESOP 2003.
Line 47: Line 53:
John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002.
Peter W. O'Hearn, John C. Reynolds, Hongseok Yang: Local Reasoning about Programs that Alter Data Structures. CSL 2001.
Hypothetical frame rule, abstract predicates

Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: Separation and information hiding. POPL 2004.
Matthew J. Parkinson, Gavin M. Bierman: Separation logic and abstraction. POPL 2005.		  * John C. Reynolds: [[http://www.cs.cmu.edu/~jcr/seplogic.pdf|Separation Logic: A Logic for Shared Mutable Data Structures.]] LICS 2002.
 * Peter W. O'Hearn, John C. Reynolds, Hongseok Yang: [[http://www.dcs.qmul.ac.uk/~ohearn/papers/localreasoning.pdf|Local Reasoning about Programs that Alter Data Structures.]] CSL 2001.
Line 56: Line 58:
Peter W. O'Hearn: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3): 271-307 (2007)
Stephen Brookes: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1-3): 227-270 (2007)
Viktor Vafeiadis: Concurrent separation logic and operational semantics. MFPS 2011		  * Peter W. O'Hearn: [[http://www.eecs.qmul.ac.uk/~ohearn/papers/concurrency.pdf|Resources, concurrency, and local reasoning.]] Theor. Comput. Sci. 375(1-3): 271-307 (2007).
 * Stephen Brookes: [[http://www.cs.cmu.edu/afs/cs.cmu.edu/user/brookes/www/papers/seplogicrevisedfinal.pdf|A semantics for concurrent separation logic.]] Theor. Comput. Sci. 375(1-3): 227-270 (2007).
 * Viktor Vafeiadis: [[http://www.mpi-sws.org/~viktor/cslsound/|Concurrent separation logic and operational semantics.]] MFPS 2011.
Line 62: Line 64:
John Boyland: Checking Interference with Fractional Permissions. SAS 2003
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson: Permission accounting in separation logic. POPL 2005.		  * John Boyland: [[http://www.cs.uwm.edu/~boyland/papers/permissions.pdf|Checking Interference with Fractional Permissions.]] SAS 2003.
 * Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson: [[http://www.cl.cam.ac.uk/~mjp41/permissions_paper.pdf|Permission accounting in separation logic.]] POPL 2005.

=== Hypothetical frame rule, abstract predicates ===

 * Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: [[http://www.cs.ox.ac.uk/people/hongseok.yang/paper/p84-yang.ps|Separation and information hiding.]] POPL 2004. (there is also a [[http://www.cs.ox.ac.uk/people/hongseok.yang/paper/hiding-TOPLAS.pdf|journal version]])
 * Matthew J. Parkinson, Gavin M. Bierman: [[http://www.cl.cam.ac.uk/~mjp41/p205-parkinson.pdf|Separation logic and abstraction.]] POPL 2005.
Line 67: Line 74:
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv: Local Reasoning for Storable Locks and Threads. APLAS 2007
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli: Oracle Semantics for Concurrent Separation Logic. ESOP 2008
RGSep, LRG		  * Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv: [[http://software.imdea.org/~gotsman/papers/lith-aplas07.pdf|Local Reasoning for Storable Locks and Threads.]] APLAS 2007
 * Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli: [[http://www.cs.princeton.edu/~appel/papers/concurrent.pdf|Oracle Semantics for Concurrent Separation Logic.]] ESOP 2008
 * A. Buisse, L. Birkedal, and K. Støvring: [[http://www.itu.dk/~birkedal/papers/locks.pdf|A step-indexed Kripke model of separation logic for storable locks.]] MFPS 2011
Line 71: Line 78:
Viktor Vafeiadis, Matthew J. Parkinson: A Marriage of Rely/Guarantee and Separation Logic. CONCUR 2007.
Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis. Chapter 3.
Xinyu Feng: Local rely-guarantee reasoning. POPL 2009: 315-327		 === RGSep, LRG ===
Line 75: Line 80:
=== Deny-guarantee, concurrent abstract predicates ===  * Viktor Vafeiadis, Matthew J. Parkinson: [[http://www.cl.cam.ac.uk/~mjp41/RGSep.pdf|A Marriage of Rely/Guarantee and Separation Logic.]] CONCUR 2007.
 * Viktor Vafeiadis. [[http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf|Modular fine-grained concurrency verification.]] PhD thesis. Chapter 3.
 * Xinyu Feng: [[http://staff.ustc.edu.cn/~xyfeng/research/publications/LRG.html|Local rely-guarantee reasoning.]] POPL 2009: 315-327
 * Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis: [[http://www.mpi-sws.org/~viktor/papers/sas2007-smallfootrg.pdf|Modular safety checking for fine-grained concurrency.]] SAS 2007.
Line 77: Line 85:
Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis: Deny-Guarantee Reasoning. ESOP 2009: 363-377
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis: Concurrent Abstract Predicates. ECOOP 2010: 504-528		 === Deny-guarantee ===

 * Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis: [[http://www.cl.cam.ac.uk/~mjp41/dg.pdf|Deny-Guarantee Reasoning.]] ESOP 2009: 363-377

=== Concurrent abstract predicates ===

 * Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis: [[http://www.cl.cam.ac.uk/~md466/publications/ECOOP.10.concurrent_abstract_predicates.pdf|Concurrent Abstract Predicates.]] ECOOP 2010: 504-528

Concurrent Program Logics

Instructors: Viktor Vafeiadis and Derek Dreyer

Teaching assistant: Georg Neis

Meeting time: 2 hours, once a week, April - July 2011

Abstract

Reasoning about concurrent programming is a particularly exciting topic in program verification. The focus of much of the research in this area is on developing modular and compositional methods for verification that nonetheless allow for fine-grained synchronization, as well as the sharing of mutable data structures, between multiple threads. Although some of the fundamental ideas in the area (such as Hoare logic and rely-guarantee reasoning) were developed thirty years ago, there has been major progress in the last several years, and the field is complex and highly active.

In this seminar course, we will study the development of concurrent program logics, from their roots in the late '70s up to the most recent breakthrough technologies. The course will be structured like a reading group, with one student tasked with presenting a paper each week, followed by an in-depth discussion.

The course is being co-taught by Viktor Vafeiadis (MPI-SWS, the Kaiserslautern branch) and Derek Dreyer (MPI-SWS, the Saarbruecken branch), and will be conducted by videoconferencing between the two MPI-SWS locations.

Schedule

Date and time

Topic

Presenter

Files

Monday 2011-04-11, 12:15.

Introduction, Hoare logic

Viktor

slides

Monday 2011-04-17.

No meeting (Easter holiday)

Monday 2011-04-25.

No meeting (Easter holiday)

Monday 2011-05-02, 16:15.

Owicki-Gries

Jonas

slides example

Monday 2011-05-09, 16:15.

Rely-guarantee

Georg

slides example

Monday 2011-05-16, 16:15.

Separation logic

Sigurd

slides

Monday 2011-05-23, 12:15.

Concurrent separation logic

Beta

slides counter-example

Monday 2011-05-30, 16:15.

Permissions

Matt

slides(M) slides(V)

Monday 2011-06-06, 16:15.

Abstract predicates

Scott

slides

Thursday 2011-06-16, 16:15.

Storable locks

Derek

Monday 2011-06-20.

No meeting (LICS)

Thursday 2011-06-30, 16:15.

RGSep, LRG

Arthur

slides

Monday 2011-07-04, 16:15.

More RGSep, SmallfootRG

Viktor + Arthur

slides(V) slides(A)

Monday 2011-07-11.

No meeting (POPL deadline)

Monday 2011-07-18, 16:15.

Deny-guarantee

Georg

slides

Thursday 2011-07-21, 16:15.

Concurrent abstract predicates

Gil

slides

Thursday 2011-08-04, 16:15.

Concurrent abstract predicates (continued)

Gil

Reading list

Early papers

Rely/guarantee

Separation logic

Concurrent Separation Logic

Permissions

Hypothetical frame rule, abstract predicates

Storable locks

RGSep, LRG

Deny-guarantee

Concurrent abstract predicates

cpl (last edited 2011-07-25 23:44:25 by dreyer)