论文部分内容阅读
并行编程技术由于其运算效率高且性能好的能力,一直是学术界和工业界的热点研究对象。作为其中一种解决方案的事务内存处理技术(Transactional Memory,TM),采用以事务代替锁的方式,解决了其他传统解决方案中的种种问题。而在当前市场上,TM的应用还局限于传统的交易系统和服务行业。原因可归纳为(1)支持TM技术的多核设备没有得到普及,且当下流行的编程语言并不支持TM;(2)并非所有类型的应用程序都适用于TM类型的编程模型;(3)对TM技术应用并行性的评估系统不够完善。因此,将TM范式推广到更多的应用领域受到了阻碍。为解决这三种问题,PSTM(Python Software Transactional Memory)框架应运而生。本文从该框架的源代码出发,采用进程代数演算中的通信顺序进程(Commu-nicating Sequential Processes,CSP)方法对 PSTM 框架进行了深层次的形式化分析与建模。对PSTM框架中的通信过程与组件进行多角度的抽象与分析,包括建立多层次的请求事务模型,循环提供服务的PSTM_API、PSTM-Server组件的模型,以及待更新的系统字典模型,全面刻画了 PSTM框架的通信行为。此外,本文还抽象了框架中的远程过程调用接口,并建立了一对多的队列模型,和多对一的管道模型。接着,通过使用模型检测工具(Process Analysis Toolkit,PAT)对建立的模型进行了自动化仿真与性质验证。为了简化编码,我们改进了 PAT中提供的C#库函数。将传统事务性质与PSTM框架的特点相结合,本文对该框架进行了无死锁性,原子性,隔离性,一致性和乐观性五个性质的验证。从PAT给出的验证结果和执行轨迹来看,五个性质均有效。基于对通信过程执行逻辑的判断,本文证明了 PSTM框架通信正常,能保证无死锁性,原子性,隔离性,一致性和乐观性,从横向角度验证了 PSTM框架通信的安全性。最后,本文还为PSTM框架提供了一个具有应用场景的案例分析与验证。从引入共享计数器的概念展开,提出了一个推论,即共享计数器的值等同于并行的进程个数,并对案例系统是否能满足此推论进行了正反两个角度的验证。结果表明,推论成立,从纵向角度验证了 PSTM框架通信的安全性。