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