【作者】 徐超；

【导师】 朱惠彪；

【作者基本信息】 华东师范大学 ， 软件工程， 2019， 硕士

【摘要】 事务性内存(Transactional memory,简称TM)是一种非常有前景的解决多核系统中同步和并发问题的机制。然而在高冲突情况下,事务性内存性能会大幅降低。为了做出改进,目前相关研究领域主流的解决方式是:引入事务调度机制(Transaction Scheduling),这也正是本文的研究对象。事务调度机制可以在事务执行之前就对事务进行预分配,以降低事务冲突,达到提高性能的目的。然而,设计一个好的事务调度机制并不容易,它需要满足很多要求,包括:1)调度机制本身不会死锁;2)不会使得事务执行出现活锁或者饥饿的现象;3)具备低冲突,负载均衡等良好性能特性。目前,已有较多研究者设计出了基于队列的事务调度机制,同时还通过仿真实验对其设计进行了一定的分析。但是,这些研究成果给出的性能评估都较为片面,忽略了必要性质验证,且实验数据结果受执行环境影响很大。这使得读者很难对比出算法之间的优劣。本文给出了一种针对事务调度机制的形式化评估方法。这种形式化研究方法可以以一种严格的、具有一般性的方式对事务调度机制的无死锁性和无饥饿性进行验证,除此之外,还可以给出事务调度机制在性能上的对比性评估。这很好地弥补了事务调度机制研究领域在理论研究以及全面评估方面的空缺。为了更方便地展现该形式化的评估方式,本文选取Popovic等人设计的事务调度机制为例来给出形式化建模与验证。首先,本文通过通信顺序进程CSP(Communicating Sequential Process)对事务调度机制进行了形式化的建模。然后,基于该模型,利用模型检测工具(Process Analysis Toolkit,简称PAT)验证了算法的无死锁性和无饥饿性,并从执行时间、执行时间加速比、冲突次数和吞吐量这几个维度给出了性能评估。最终可以得到一个针对事务调度机制做出全面评估的形式化方法。另外,为了更好地说明本文所提供方法的可拓展性,本文还选取了著名的自适应事务调度机制(Adaptive Transaction Scheduling,简称ATS),对Popovic等人提出的事务调度机制进行横向的对比和评估。这也为本文给出的形式化评估方式提供了更多的参考。更多还原

【Abstract】 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.更多还原