Deductive mechanical verification of concurrent systems

Society depends critically on the correct and efficient execution of computer programs. The requirements of correctness and efficiency are not independent or complimentary. The goal of efficiency often engenders complexity in the design, definition, and execution of computer programs which complicates the analysis of correctness. Modern computing systems support increased performance by providing multiple execution units operating in parallel and efficient programs utilize this support for parallel execution by decomposing computation sequences into multiple concurrent interacting threads of execution. The concurrency introduced in these programs exacerbates the difficulty of verifying the correct operation of the programs since it greatly increases the possible states the threaded execution may reach. In this dissertation, we propose the use of theorem proving for proving the correctness of concurrent programs. Specifically, we present specification methodologies and tool support for proving the correctness of concurrent programs using the theorem prover ACL2. We present the use of stuttering refinement as a means for specifying the correctness of a concurrent program implementation by relating the execution traces of the implementation with the behaviors of a much simpler specification program. Stuttering refinement allows one to hide spatial and temporal details in the implementation program in the relation with the specification while still ensuring that the implementation makes progress to matching steps in the specification. We also present reductions of the proof requirements for stuttering refinement to facilitate the proof of refinements with the theorem prover ACL2. The theorem prover ACL2 is a general-purpose theorem prover and the theorems which arise in stuttering refinement proofs tend to stress the ability of ACL2 to efficiently discover proofs. We extend ACL2 with an efficient and elegant simpli- fier which significantly increases the performance of ACL2 in handling the theorems which arise in refinement proofs. This simplifier is named KAS and we present the definition of KAS along with an argument of its soundness and limited completeness. The KAS simplifier has been designed to be extended by the user and would have application beyond the focus on stuttering refinement proofs in this dissertation. Even with the adoption of KAS, the user is burdened with the definition of inductive invariants which may require significant experienced user interaction in order to develop the appropriate definitions. We present a separate tool which uses user-guided term rewriting (extended by theorems proven in ACL2) to generate an abstract model suitable for proofs of invariants. We present the details of this procedure along with its application to several example programs. We conclude the dissertation with a proposal for the development of an integrated compiler and prover intended to avoid the specification and proof requirements for concurrent programs by automating the construction of concurrent programs which are proven correct by construction.