Chapter 4. Verification of Concurrent Programs
The previous chapters have shown that concurrent programs can have subtle errors, that the errors cannot be discovered by debugging and that corrections cannot be checked by testing. For this reason, formal specification and verification of correctness properties are far more important for concurrent programs than they are for sequential programs. In this chapter we will explore several such methods.
We begin with a short section on the specification of correctness properties and then present the most important technique for proving properties, inductive proofs of invariants. This technique is used to prove that mutual exclusion holds for the third attempt. Inductive proofs are easy to carry out once ...
Get Principles of Concurrent and Distributed Programming, Second Edition now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
