Checking concise specifications for multithreaded programs

Ensuring the reliability of multithreaded software systems is difficult due to the potential for subtle interactions between threads. Unfortunately, checking tools for such systems do not scale to programs with a large number of threads and procedures. To improve this shortcoming, we present a verification technique that uses concise specifications to analyze large multithreaded programs modularly. We achieve thread-modular analysis by annotating each shared variable by an \emph{access predicate} that summarizes the condition under which a thread may access that variable. We achieve procedure-modular analysis by annotating each procedure by its specification, which is related to its implementation by an abstraction relation that combines the notions of simulation and reduction. We have implemented our analysis in Calvin-R, a static checker for multithreaded Java programs. To validate our methodology, we have used Calvin-R to check a number of important properties for a file system. Our experience shows that requirements for complex multithreaded systems can be stated concisely and verified in our framework.