Modeling And Verifying Transaction Scheduling For Transactional Memory Based On CSP

Transactional Memory(TM)is a mechanism with a great prospect for simplifying parallel programming.However,transactional memory performance would be greatly reduced in high-conflict situations.In order to make improvements,the current mainstream solution in the relevant research fields is to introduce a transaction scheduling,which is exactly what this paper researches on.The transaction scheduling mechanism can pre-allocate transactions before they are executed so as to reduce transaction conflicts and improve performance.However,designing a good transaction scheduling mechanism is not easy,it needs to meet a lot of requirements,including: 1)the scheduling mechanism itself should be deadlock-free;2)it will not cause a livelock or starvation in transaction execution;3)it should have good performance characteristics such as low-conflict and load-balancing.Until now,researchers have designed many queue-based transaction scheduling mechanisms,and also made analysis of their designs through simulation experiments.However,the algorithm evaluations given by these research are rather partial,ignoring the verification of necessary properties,and the results of experiments could be greatly affected by the execution environment,lack of generality.This makes it difficult for readers to compare the advantages and disadvantages between scheduling mechanisms.This paper presents a formal evaluation method for the transaction scheduling mechanism.This formal research method can verify the deadlock-freeness and starvation-freeness of the transaction scheduling mechanism in a strict and general way.In addition,it can also give comparative evaluations on the performance of the transaction scheduling mechanisms.This is a good complement to the theoretical research and comprehensive evaluation of the field of transaction scheduling mechanisms.In order to illustrate the formal evaluation method more conveniently,we select the transaction scheduling mechanism designed by Popovic et al.as an option to give formal modeling and verification.First,we apply the Communicating Sequential Processes(CSP)to formalize the transaction scheduling.Then,based on the this model,we use the model checker Process Analysis Toolkit(PAT)to verify the deadlock-freeness and starvation-freeness of the scheduling mechanism.In addition,the performance comparisons from the perspective of makespan,speedup,aborts time,and throughput are also given.Consequently,a formal approach to evaluate transaction scheduling can be achieved.Besides,in order to better illustrate the scalability of the formal method provided in this paper,we select the most classic Adaptive Transaction Scheduling to give further evaluation and comparison horizontally.This also provides more references for the formal evaluation method given in this paper.