Tutorial presented at FM 2011, 21 June 2011.
Reasoning about concurrent programs has long been recognized as challenging. Early approaches often tried to identify useful cases where the messy problems caused by interference could be avoided - essentially the attempt was to show that "races" could not occur. Recently, Separation Logics have provided very convenient ways of reasoning about such situations and clever notations have made proofs about even intricate low-level code quite tractable. A different challenge is reasoning about "racey" programs. Approaches like rely/guarantee reasoning face interference head on and include assertions about permissible interference. Although some people would regard this as masochism, it transpires that accepting interference at abstract levels of design can result in some clear developments of even race-free programs. RGSep has already shown that unification of rely/guarantee thinking and separation logic offers a powerful new tool. We will try to indicate clearly the strengths of the two approaches and indicate more ways of combining these strengths.
Cliff Jones is currently Professor of Computing Science at Newcastle University (he is also FREng and FACM). He is a long-standing member of the Formal Methods community having been one of the original developers of VDM. Of most relevance to this tutorial, he originated much of the VDM material relating to program specification and design as well as the rely/guarantee approach to specifying and reasoning about concurrency. He has also been involved in the development and use of several generations of support tools for formal methods.
Viktor Vafeiadis is a researcher at the Max Planck Institute for Software Systems (MPI-SWS) specialising in the verification of concurrent programs, and is one of the developers of RGSep, a program logic that combines rely/guarantee reasoning with separation logic. Viktor received his Ph.D. in 2008 from the University of Cambridge and, prior to joining MPI-SWS, has held post-doctoral research positions at Microsoft Research and at the University of Cambridge.