| |
|
|
Electronic Systems Design Seminar
|
 |
|
Many multithreaded software systems, such as operating systems, databases, and embedded systems are mission-critical. Programming these systems is error-prone and thus could greatly benefit from formal verification. Unfortunately, existing verification methods do not scale to real-world multithreaded programs. In this talk, I will describe a new method that exploits modularity to build a scalable checker for multithreaded programs. The method has been implemented for Java and used to check synchronization-rich parts of the Mercator web crawler, which has been in production use at Altavista for the past several years.
The focus of this talk is modular verification of multithreaded programs. Modularity is a key requirement for the scalability of program checking techniques. Modular verification of sequential programs is well- understood. A sequential program naturally decomposes into a collection of procedures. By specifying pre- and post- conditions on the procedures, each procedure can be verified separately. Multithreaded programs naturally decompose into a collection of threads where each thread is a collection of procedures. Modular verification of multithreaded programs requires not only each thread but also each procedure in a thread to be verified separately. I will show that pre- and post- conditions are insufficient as procedure specifications for modular verification of multithreaded programs. I will propose a richer procedure specification and then present a method to reduce the problem to the verification of sequential programs. I will finally describe initial experiments in which we applied this method on the Mercator web crawler. The checker verified the correctness of Mercator's implementation of reader-writer locks and the absence of data races in the code of the client threads.
Shaz Qadeer is a member of the research staff at Compaq Systems Research Center. He is interested in the formal design and analysis of concurrent systems ---hardware, software and protocols. Currently, he is working on modular verification and automatic abstraction of multithreaded software. Shaz received his B.Tech. in EE from the Indian Institute of Technology Kanpur in 1994. He received his M.S. and Ph.D. in EECS from the University of California at Berkeley in 1997 and 1999 respectively.
This is joint work with Cormac Flanagan and Sanjit Seshia.