The Art of Concurrency

Chapter 3. Proving Correctness and Measuring Performance

This chapter takes a look at topics related to the final two steps of the threading methodology. The first is knowing when your concurrent algorithms will run correctly or at least have a good idea that you’ve done a good job of designing an error-free concurrent algorithm. The second topic covers some of the ways you can measure how well your concurrent code is executing in parallel. Finally, I’ve put in a little history review (don’t worry—it’s short, it’s related to the topic of this book, and it never hurts to know where you’ve been to have a clue about where you might be going).

Verification of Parallel Algorithms

In his 2006 book Principles of Concurrent and Distributed Programming, Second Edition (Addison-Wesley), M. Ben-Ari defines an abstraction for formally verifying the correctness and other properties of concurrent algorithms. Unlike other theoretical abstractions in computer science that deal with hardware (e.g., PRAM), Ben-Ari’s abstraction deals with how concurrent programs execute. I don’t want to get into all the details and justifications for this abstraction here. I recommend that you read Ben-Ari’s book for that and for another good resource in concurrent algorithm design. I want to cover just enough for you to understand the principles and the basic idea of the concurrency abstraction and how to prove concurrent ...