VSync : Verifying Concurrent Software for Multicore Machines

VSync project is a research about the implementation of various synchronization mechanisms in the high confidence of parallel software structure and the related methods on program verification.
Our main thoughts on researching synchronization mechanisms in the high confidence parallel software are: at the assembly level, for each kind of synchronization implementation, extend the CCAP framework that proposed by Prof. Shao and design program logic (a Hoare style logic that describes and certifies concurrent program properties) in order to construct Foundational Proof Carrying Code (FPCC); the certifying framework at the assembly level can be linked with a certifying compiler or a certified compiler to guide the design and implementation of synchronization abstract at the high level. Based on these, programmers can write and certify programs with these high-level synchronization abstracts, and then compilers generate the proof-carrying code at the assembly level. At the assembly level, the correctness of the implementation of various synchronization technologies is enforced by certifying the safety property of parallel programs using these technologies.
Current research goal is to study various implementations of synchronization mechanisms (such as transactional memory and locks) and the related methods on program verification to guide the design and implementations of synchronization abstract and lay the groundwork for constructing high confidence parallel programs.
Research Contents and Methods:
Take the type theory and Hoare style logic as the main methods, with the extension of the CCAP certifying framework, study various implementations of locks, transactional memory and the mixed synchronization mechanisms and their correctness verification.
The CCAP framework is based on the CiC (Calculus of Inductive Constructions) which is a meta-logic for constructing the Hoare-style special logics in various specialized areas. On the one hand, the design of special logics can simplify the description and verification of programs in special areas. On the other hand, all these special logics can be mapped to the underlying meta-logic, so codes certified using these different special logics can be safely coexist.
Our research is mainly in accordance with the following steps: 1) define an abstract machine model (syntax and operational semantics) that has some kind of primitive instructions for synchronization inside; 2) design a program logic which is made up of the program specification language and inference rules; 3) give the soundness proof of the program logic by finishing Progress and Preservation lemmas; 4) give examples to show the effectiveness of the certifying framework; 5) the whole framework including the abstract machine model, program logic, soundness proof and examples is fully mechanized in the Coq proof assistant.
Our program logic is based on the Rely-Guarantee method which is support modular verification, and combines with Concurrent Separation Logic, Permission Control, Invariance Proof and so on.
Li, Y, Zhang Y, Chen Y, Fu M.  2010.  Formal reasoning about lazy-STM programs, accepted by Journal of Computer Science and Technology.
Download: Formal reasoning about lazy-STM programs.pdf (246.32 KB)coq-impl.rar (54.34 KB)
Fu, M, Zhang Y, Li Y.  2010.  Formal verification of concurrent programs with read-write locks. Frontiers of Computer Science in China, 4(1):65-77. DOI: 10.1007/s11704-009-0067-6.
Download: paper.pdf (317.3 KB)ccprwl_impl.rar (44.96 KB)
Fu, M, Zhang Y, Li Y.  2009.  Formal reasoning about concurrent assembly code with reentrant locks. 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE 2009).
Download: tase2009.pdf (89.95 KB)impl.rar (50.53 KB)
Li, Y, Zhang Y, Chen Y, Fu M.  2009.  On the verification of strong atomicity of programs using STM. 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement(SSIRI2009).
Download: SSIRI2009.pdf (269 KB)coq-impl.rar (54.34 KB)
Li, L, Zhang Y, Chen Y, Li Y.  2009.  Certifying concurrent programs using transactional memory. Journal of Computer Science and Technology. 24(1):110-121.
Download: jcst0901.pdf (467.14 KB)impl.rar (75.93 KB)