Verification Of Low-level Concurrent Code With Several Synchronization Mechanisms

The advent of multi-core processors characterized by shared memory acceler-ates the requirement on fleetly developing shared-resource-based parallel software. It brings out many challenging research topics on building high confidential parallel softwares. In the process of building parallel softwares, the threads make interac-tion and communication through accessing shared resources, and the synchroniza-tion mechanism for accessing shared resources is key to ensure the correctness of parallel programs.At present, there mainly exist two different kinds of synchronization mecha-nisms for shared variable access control. One is locking and the other is transac-tional memory. The traditional locking synchronization mechanism manages the concurrent store and load over shared resources by lock-protected critical section. However, the locking way not only limits the execution efficiency running on multi-core processors, but also easily leads to deadlock and makes the running program to enter the abnormal state. Read-write locks and reentrant locks are the lock-based synchronization mechanisms for achieving the optimization. The read-write locks allow multiple threads to read the shared resources concurrently, and the reentrant locks permit threads to reacquire the self-owned locks to avoid deadlock on itself. Transactional Memory (TM) is a new research topic on synchronization technology for bringing the advantages of multi-core processing system into play. It attempts to utilize a sequence of grouped instructions that execute atomically and in isolation to simplify parallel programming.Our group's research topic is verification of concurrent programs using diverse synchronization mechanisms. This dissertation mainly focuses on the verification of low-level concurrent programs using read-write locks and reentrant locks. The existing formal verification framework and program logic for reasoning about the lock-based parallel programs only consider the non-reentrant exclusive locks with simple semantics and ignore read-write locks and reentrant locks. These improved synchronization mechanisms can improve the performance of parallel programs and ease parallel programming, but we cannot directly apply the existing technology to reason about them due to their complex semantics. In addition, both locking and TM have their strengthen and weakness, and the future high performance parallel software probably need to use both of them to obtain the most benefits, and the program logic for reasoning the concurrent programs with both locking and TM are required to ensure the correctness of the corresponding high confi-dential softwares. The designment of an appropriate intermediate language is the premise of reasoning about the mixing synchronization mechanisms. However, few research works concern on the language and program logic design for supporting. both locking and TM synchronization mechanisms.According to the research background of locking and TM, as well as the ex-isting research results on program verification, the major work of this dissertation is divided into the following two aspects:On the one hand, we attempt to extend the certified concurrent assemble aro-gram (CCAP) framework that proposed by Prof. Shao and design the exclusive Hoare-style program logic for reasoning concurrent assemble programs using read-write locks and reentrant locks in order to construct Foundational Proof Carrying Code (FPCC). We choose concurrent separation logic (CSL) which is fit for reason-ing concurrent program with exclusive critical sections and supports modularity as our basic logic, and due to its limitation we extend it to support reasoning about read-write locks and reentrant lock as follows:●We extend CSL to reason about concurrent programs using read-write locks primitives, and the separation conjunction in CSL is divided into "strong separation" and "weak separation". The former which do not allows resource overlaps is used to describe the resource partition among read-write and read-read threads, and the latter which allows resource overlaps is use to depict the resource partition among read-read threads. Our extension makes up the limitation of CSL which only allows strong separation over resources.●We design an inference rules for the first entry and reentry of acquiring reentrant locks based on CSL, the resource ownership transfer in the adapted CSL avoids reacquiring the same resources. Then the extended CSL can be applied to reason about concurrent programs using reentrant locks. We use Coq proof assistant to implement the proposed verification frameworks and give their soundness proof, this makes our reasoning system more reliable.On the other hand, we present a novel syntax construct "rev{C}" to describe the reversible code blocks which is closely related to TM. With the help of this construct we obtain an intermediate language to combine both locking and TM into a unified programming model. We also discuss the difficulties on reasoning about the reversible blocks, and this preliminary work gives the basis for further study of formal verification of reversible code blocks. An example is given to demonstrate the expressive power of the proposed language, and the requirements for safely executing reversible code blocks are also discussed.