Certifying Concurrent Porgrams Using Transactional Memory

The multicore architecture, which has provided infrastructures of better performance, has become popular. To benefit from this growth in performance, programmers are required to develop multi-threaded programs. Whereas it is difficult to ensure correctness for sequential programs, it is even more so for concurrent programs due to the interaction between multiple threads. Traditionally, programmers use locks to achieve mutual exclusion on concurrent access to shared resources. But lock-based programming is difficult to reason about and may lead to problems such as deadlock. Transactional memory (TM) is proposed as an alternate concurrency-control mechanism to avoid many of the pitfalls of the lock-based one. TM systems manage data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound.This dissertation presents a reasoning method for programs using TM and formalizes it into a Hoare-style verification framework. The reasoning method is based on invariance proof and Hoare-style reasoning and supports modular verification. The proof-carrying code (PCC) style framework is proved sound with respect to the TM semantics. And a comparison between lock-based reasoning and TM-based reasoning is presented and shows the convenience of the latter. This dissertation makes the following contributions:It presents a Hoare-style reasoning method to reason about source-level programs using TM. Even though programming using transactions is supposed to reason about easily, there are subtle properties expected by multithreaded programs. To ensure such properties are correctly enforced in a concurrent program, programmers must reason about the behaviors of their programs thoroughly. This dissertation presents a method to perform such TM-based reasoning. And the presented reasoning is based on the same intended semantics of different TM systems: to provide a programming structure that executes atomically and in isolation. This makes the presented reasoning compatible with various TM systems that respect the same intended semantics.It also presents a proof-carrying code style framework to certify the properties of assembly level programs using TM. The presented framework brings PCC into the brand-new TM area. The inference rules of the framework are proved sound with respect to the TM semantics. And examples are also given to illustrate the construction of the proofs for programs in the framework, demonstrating the effectiveness of the framework.The presented framework addresses safety issues at assembly-level directly as PCC systems do. So the complicated and error-prone compilation and optimization do not need to be trusted. And the presented reasoning method is formalize into framework and is sound due to the soundness of the framework. All the work on the framework, including its soundness proof and examples, is mechanized in proof assistant Coq. This makes our work more reliable.Through thorough comparison, it shows the convenience of TM-based reasoning over lock-based reasoning.