Verifying Parallel Low-Level Programs For Multi-core Processor

As the multi-core processor is widely used and advanced high-trusted software is required, the verification of parallel programs for multi-core processor becomes more and more important. This paper presents a proof framework about the verification of parallel programs, including the definition of our abstract machine, the formal specification for object code, logic inference rules and the proof of soundness theory. Finally, we provide some extension methods based on our framework.We directly certify the code at an assembly-level in order to disregard the verification of compilers. The classic spin lock technology is introduced to implement the mutually exclusive access to shared memory. Our proof framework supports Hoare-logic style reasoning. In addition, we use high-order logic to describe both operational semantics and safety policy. Programmers can verify the partial correctness of multi-core parallel programs in our framework.The main contributions of this thesis include:1. A proof framework about the verification of parallel programs for multi-core processor is proposed. It would enrich the application format and content of Proof-Carrying Code (PCC). Also, it would give a new thought for the verification of multi-core programs.2. This framework is sound. We have finished the proof of soundness theorem with proof assistant Coq. So, a program certified using our system is free of unchecked runtime errors.3. We have analyzed and provided some effective methods on how to extend MCAP framework in following three aspects: real-assmbly-level verification, modular verification with function call/return, and the improvement of the presentation ability of program specification.