Abstractions for reasoning about concurrency

Abstraction is essential to achieve separation of issues and to help in the understanding of complex systems.

The track record of deploying abstraction in the development of computer programs is both long and successful (Christopher Strachey was an early contributor). One can compare the layers of abstraction used in a program explanation with the outline of a mathematician's proof of a non-trivial theorem. The formalism chosen governs the difficulty of completing detailed proofs that can be verified with mechanically checkable rules. Reasoning, whether formal or informal, about intricate concurrent programs can be difficult and it is, therefore, crucial to be selective in the choice of abstractions.

This talk will review, at a general level, abstractions and techniques for reasoning about the development of concurrent programs.  For example, it will identify dangers in the use of so-called auxiliary variables; it will reconsider the idea (hatched in Oxford) of rely/guarantee conditions -- but again at a conceptual rather than detailed level. Hopefully there will also be time to make similarly high-level comments about separation logic.