Notes and Further Reading

We are indebted to David Holmes for initially pointing out the problems with the bounded buffer and read – write lock that we have exposed in this chapter. He also motivated this chapter by suggesting that we should address the problem of verifying implementations. David is a Senior Research Scientist at the Cooperative Research Centre for Enterprise Distributed Systems Technology (DSTC Pty Ltd.), located in Brisbane, Australia.

We pointed out in this chapter that our model of notification ignores the effect of an interrupt exception. It is possible, for a thread waiting to be notified, to be interrupted before actually returning from the wait() call. As a result it returns via an InterruptedException not a normal return and essentially, the notification is lost even though other uninterrupted threads may be waiting. This means that programs that use notify() and allow InterruptedException to be thrown directly are not guaranteed to work correctly. Although we use this technique in the book, it does not result in inconsistencies since in all cases, the interrupt exception is used to terminate all active threads. However, it is another reason for using notifyAll() rather than notify(). This may sometimes result in a large number of unnecessary thread activations and consequently be inefficient. For example, in the semaphore program of section 5.2.2, a better way to deal with the lost notification problem is to catch the InterruptedException and perform an additional notify() before rethrowing the exception. Thanks again to David for pointing this out.

The earliest attempt to prove a program correct appears to be that of Turing who presented a paper, Checking a large routine, on 24 June 1949 at the inaugural conference of the EDSAC computer at the Mathematical Laboratory, Cambridge. He advocated the use of assertions “about the states that the machine can reach”. The formal foundations for techniques for program correctness were laid in the 1960s with contributions by pioneers such as McCarthy, Naur, Floyd, Dijkstra and Hoare (Morris and Jones, 1984). Again, the essence of the approach is to associate logical assertions, pre- and post-conditions, with the statement blocks in a program. Invariants are used to characterize the properties preserved by loops, later extended to characterize objects and monitors (see Chapter 5). This work was initially targeted at proving the correctness of sequential programs, and involved both a proof of satisfaction of the program post-condition and a proof of termination. The correctness of concurrent programs is more complex, requiring that the techniques deal with nonterminating and nondeterministic programs. The foundations were again laid in the 1960s by the insights of researchers such as Dijkstra and Petri, but it was in 1977 that Lamport proposed that correctness of concurrent programs should be argued for two sorts of properties: safety and liveness.

Since those early pioneering days, much research work and experience have been gained. The 1996 state-of-the-art papers on concurrency (Cleaveland, Smolka, et al.) and formal methods (Clarke, Wing, et al.) provide an excellent overview. All these techniques have had major impact on the design of programming languages and programming methods. However, because of the effort involved, the impact on practice has been limited to a relatively small number of specific circumstances, such as safety-critical software, software which is difficult or impossible to update or software to be used in vast numbers of consumer products. The advance of techniques and technology in theorem proving and model checking over the last ten years has made program verification more accessible and practical.

The approach adopted by many current researchers is to try to extract a model directly from the code. Techniques used vary from code annotation, which provides the mapping between code and model, to various abstraction techniques which hide program detail irrelevant to the particular property or concern. Notable amongst these are the FeaVer Toolset for C programs (Holzmann and Smith, 2002), FLAVERS for Ada programs (Cobleigh, Clarke and Osterweil, 2002), the Java PathFinder tool (Havelund and Pressburger, 2000) and the Bandera toolset (Corbett, Dwyer, Hatcliff, et al., 2000) for Java programs.

Other approaches are attempting to develop verification tools tailored to work directly on a program in a specific programming language. A second version of the Java PathFinder tool (Brat, Havelund, Park, et al., 2000), Microsoft’s SLAM project for C (Ball and Rajamani, 2002), and the Blast tool for C (Henzinger, Jhala, Majumdar, et al., 2003) are examples of this work.