History for Concurrency

removed:
-

changed:
-There have been significant advances on reasoning about (shared memory) concurrent programs, including the Owicki-Gries theory, temporal logic (Pnueli) , and  rely-guarantee method (Jones, Chandy, Misra). More recently, 
There have been significant advances on reasoning about (shared memory) concurrent programs, including the Owicki-Gries theory, temporal logic (Pnueli) , and  rely(or assume)-guarantee method (Jones, Chandy, Misra). More recently, 

changed:
-However, what we see is a mishmash of specific techniques, and very specific advances whose limitations and whose fundamental assumptions are not well understood. For example, Boogie and concurrent separation logic both speak of "ownership", but it is not easy to connect them (their modes of expression being somewhat distant).  A proper theory of modular reasoning about concurrency would lay bare the primitive assumptions that give rise to modular reasoning, giving Boogie and separation logic as instances and, perhaps, other, improved methods. Such a theory does not seem near at hand.
However, what we see is a mishmash of specific techniques, and very specific advances whose limitations and whose fundamental assumptions are not well understood. For example, Boogie and concurrent separation logic both speak of "ownership", but it is not easy to connect them (their modes of expression being somewhat distant).  A proper theory  would lay bare the primitive assumptions that give rise to modular reasoning, giving Boogie and separation logic as instances and, perhaps, other, improved methods. Such a theory does not seem near at hand.

changed:
-With all this being said, the opposing position of Lamport -- that modularity is a way to make proofs harder -- should be kept in mind. 
- 
With all this being said, the opposing position of Lamport - that modularity is a way to make proofs harder - should be kept in mind.