The place to get started is

•Resources, Concurrency and Local Reasoning .PW O'Hearn, Theoretical Computer Science 375(1-3) (Reynolds Festschrift), pp271-307, May 2007. A preliminary version appeared in the Proceedings of CONCUR'04, LNCS 3170, pp49-67.

Some highlights: we can transfer portions of heap between processes, as in a resource manager or in efficient message passing; we can do modular reasoning in the presence of semaphores (e.g., split binary semaphores without maintaining a global invariant); we do parallel mergesort with no rely or guarantee conditions, the proven processes automatically mind their own business.


That paper grew out of a note from January 2002 which showed some modular reasoning about concurrency. At that time I had no model and was scared about soundness. Then John Reynolds showed surprising subtleties regarding soundness, and we were facing an extremely difficult problem in the semantics of concurrency. We needed expert help, and it arrived in Steve Brookes who rode in and saved the day (and the whole approach).

  1. •A Semantics for Concurrent Separation Logic .SD Brookes, Theoretical Computer Science 375(1-3) (Reynolds Festschrift), pp227-270, May 2007. A preliminary version appeared in the Proceedings of CONCUR'04, LNCS 3170, pp16-34.


The next step adapted a nice idea of John Boyland to allow processes to share read permissions.

•Permission Accounting in Separation Logic, by R Bornat, C Calcagno, P O'Hearn and M Parkinson, POPL 2005, 59-70.

A highlight: a nice proof of the classic readers-and-writers program. In the original TCS paper I emphasized that proven programs are race-free, and Steve Brookes showed a theorem to that effect. Doug Lea then pointed us to a challenge, some extremely racy non-blocking algorithms.


After a lot of discussion in the East London Massive, and some unsuccessful attempts, Matthew Parkinson finally gave a proof of such an algorithm.

•Modular Verification of a Non-blocking Stack  M Parkinson, R Bornat and P O'Hearn, POPL 2007

Of course, there is no conflict with the ``no races'' theorem: the concurrent separation logic just forces you to be explicit about granularity, by wrapping little critical sections around those portions of code considered atomic. Fine-grained concurrent algorithms have received further attention in logics that attempt to merge the merits of rely/guarantee (good treatment of interference) and separation logic (good treatment of independence, avoidance of global states).


 

Further Papers. A list of some further papers.

  1. •A Marriage of Rely/Guarantee and Separation Logic Matthew Parkinson and Viktor Vafeiadis.  CONCUR’07

  2. •On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning Xinyu Feng, Rodrigo Ferreira and Zhong Shao. ESOP'07.

  3. •Independence and Concurrent Separation Logic Jonathan Hayman and Glynn Winskel, Proceedings of LICS'06

  4. •To add: more papers of Gotsman, Hobor, Dodds, Feng...