Taming Concurrency: A Program Verification Perspective

Concurrency, as a basic primitive for software construction, is more relevant today than ever before, primarily due to the multi-core revolution. General-purpose software applications must find ways to exploit concurrency explicitly in order to take advantage of multiple cores. However, experience has shown that explicitly parallel programs are difficult to get right. To deliver compelling software products in the multi-core era, we must improve our ability to reason about concurrency.

Generalizing well-known sequential reasoning techniques to concurrent programs is fundamentally difficult because of the possibility of interference among concurrently-executing tasks. In this lecture, I will present reduction and context-bounding, two ideas that alleviate the difficulty of reasoning about interference by creating a simpler view of a concurrent execution than an interleaving of thread instructions. Reduction reduces interference by making a sequence of instructions in a thread appear as a single atomic instruction; it allows the programmer to view an execution as a sequence of large atomic instructions. Context-bounding reduces interference by focusing on executions with a small number of context switches; it allows the programmer to view an execution as a sequence of large thread contexts. I will present the theory behind these two approaches and their realization in a number of program verification tools I have developed over the years.

Bio: Shaz Qadeer is a researcher in the Software Reliability Research group at Microsoft Research. The goal of his research is to develop tools for improving the productivity of programmers. He has worked on many program verification tools, spanning the range from run-time verification to model checking to static analysis, with an emphasis on tools for concurrent programs. Shaz received his Ph.D. at UC Berkeley and worked at Compaq Systems Research Center before joining Microsoft Research.