Improvement Of PSTM And Its Correctness Analysis

Transactional memory(STM)is a concurrency control mechanism which is analogous to database transactions.Compared with locks,it aims to provide an easier and safer way to access share memory.Python Software Transactional Memory(PSTM)is an STM implementation in Python language.Its presentation fills a gap that Python lacks an applicable and reliable STM.PSTM satisfies the basic transaction properties,however it does not satisfy opacity,which defines conditions for serialising concurrent transaction.To alleviate this issue,we modify the PSTM implementation and present an improved PSTM called PSTM-M.Based on PSTM-M,we verify opacity of this implementation.To begin with,we analyze the PSTM architecture based on the source code.Besides,we present the implementation of PSTM-M by modifying the codes in server side of PSTM and leaving the codes in RPC and client unchanged.Also,this thesis designs and implements two experiments.Experiment 1 reproduces the situation that PSTM does not satisfy opacity.Experiment 2 aims to compare the time cost of PSTM-M with PSTM's.The results indicate that there is no much difference in time cost between these two implementations.Then,we present the formalization of opacity based on the history model of transaction.To simplify the proofs,we present three conditions which guarantee opacity if they are satisfied by an STM.We also prove the equality between the conditions and opacity.In addition to that,we give the formalization of PSTM-M via IOA(Input/Output Automata)and based on the formalization,we prove opacity of PSTM-M.The proof is carried out by induction and proceeds via the history model of transactional memory.Finally,to make the proof more convincing,we give a machine-checked proof for the opacity of PSTM-M based on the theorem prover Coq.We first model PSTM-M as pstm_trace which is built by inductive type in Coq.Then we remove all non-committed transactions in pstm_trace and transfer a pstm_trace into a cnpt(committed non-conflict pstm trace).Finally,we construct the sequential trace based on cnpt.We prove that every step in those translations is valid and the sequential trace preserves all the transaction orders in the original trace.Combining all the theorems,we prove that PSTM-M satisfies opacity.The proof of PSTM-M's opacity indicates that PSTM-M overcomes the shortages in PSTM and ensures safety of data access in parallel computing.