Modular verification of concurrent programs

Abstract

Verifying concurrent systems can be difficult because of the complex interactions possible between system components. In this paper, we propose a technique to simplify the task: modular composition of sequential proofs. We model a parallel program as a set of modules that interact by procedure calls. The properties of each module are proved using a sequential-program verification technique. If the modules satisfy a set of constraints presented in this paper, we may compose the modules into a system and the properties of the modules into properties of the system. The constraints ensure that the specifications are robust for each module where they are defined or used, in the sense that they are unaffected by current actions of other modules. A specification can be guaranteed robust for module m by restricting it to local variables of m, or by using monotonic predicates, which once true remain true forever. Our technique can be used to prove safety and liveness properties of parallel programs-the liveness properties are specified using temporal logic.