Verifying Parallel Programs Using Software Transactional Memory

Currently, Moore's Law has gradually come to the end by the barriers inthe laws of physics. It can not improve the performance just by increasing thenumber of transistors in uniprocessor. To solve this problem, researchers focuson multi-core processors, which mainly improve the performance through parallelcomputing. It brings a great change to software development methods since parallelcomputing has been fully supported by the multi-core and multi-processorarchitecture system. Software will no longer benefit from the advance of hardware,it needs to implement concurrence using hardware features and gets the advantageof new generation hardware. Therefore, for programmers, they need to developmore and more parallel programs to take full advantage of multi-core hardwarefeatures. However, parallel programming is quite difficult. On one hand, currentprogramming languages and tools are still not ready to transfer sequential programsto parallel programs. On the other hand, parallel programming requiresprogrammers to think in a different way from the human mind.In parallel programming, the key issue is the concurrent shared memory access.Traditionally, programmers typically use locks for concurrency management,but the traditional locking mechanism has following shortcomings: 1) granularitychoosing, coarse-grained locking makes programming be simple but has low concurrency;fine-grained locking can improve concurrency, but difficult to achieve,2)un-composition, the composition of two correct code blocks using locking mechanismmay fail, 3) easily lead to some problems such as priority inversion, convoyand deadlock.In order to provide an easy parallel programming mechanism with high concurrency,researchers introduce the concept of the concurrency control in Databaseinto programming language to build in Transactional Memory (TM). TM has twolevels: in high-level, it provides a simple program semantics to easy programming;in low-level, researchers design various fine-grained concurrent systems by usinglocks or other synchronization mechanisms to achieve high-level program semantics.Through the two-level system, it can effectively figure out the problems forprogrammer in parallel programming.TM also brings challenges for the concurrent program verification, existingverification techniques and frameworks can not be directly used to verify transactionalcodes. Focus on this problem, after studying various TM systems implemen- tation mechanisms and the combination with existing parallel program verificationtechniques, this paper presents a new logical system for verifying programs usingTM systems. It uses the verification to guide the design and implementation ofTM systems, and builds the basement for high confident software. Furthermore,the paper also focuses on some special TM system implementation algorithms,and certifies them to enforce the safety and correctness of the TM systems.The main work and contributions of this paper can be summarized into thefollowing parts:·It presents a logical system of the Foundational Proof-Carrying Code(FPCC) style for reasoning about concurrent programs using TM systems atthe assembly level. In this framework, we design a program logic which combinesconcurrent separation logic and permission accounting in separationlogic to reason about the speculative read in transactional codes. Furthermore,we also verify the atomicity property of transactional codes in thisframework, it requires the shared memory status after rolling back to beconsistent with the one when transaction begins.·The presented framework addresses safety properties at assembly level directlyas FPCC systems do. Then the complicated and error-prone compilationand optimization do not need to be trusted. All the work on theframework, including its soundness proof and examples, is mechanized inCoq proof assistant, which makes our work more reliable.·erifying the correctness of a classical software transactional memory implementationalgorithm. Unlike other work on the correctness verificationby using model checking, we use a Hoare-style Local-Rely-Guarantee-basedlogic to perform the formal proof. In the certification, we summarized thekey methods for reasoning about those speculative operations in the softwaretransactional memory implementation implementation with the globalversion-clock based validation technique.