事务内存(Transactional Memory)是一种模拟数据库事务执行的并发控制机制,相较于锁它为共享内存的访问提供了更简易安全的方式。PSTM(Python Software Transactional Memory)框架,是由Python语言实现的事务内存,它填补了Python缺乏成熟可靠的事务内存机制的空白。PSTM满足基本的事务特性(原子性等),但并不满足不透明性。不透明性(opacity)是一种专门针对事务内存的安全性质,它要求并发执行的事务都有一个与其等价的串行执行序列。本文针对这一缺陷,对PSTM进行修改,提出一种改进的事务内存PSTM-M,并证明其满足不透明性。本文首先从该框架的源码出发,分析PSTM框架的基本结构。通过修改PSTM服务器端代码而保持整体架构不变的方式,提出了新的事务内存PSTM-M。随后,设计并实现了两个实验:实验一重现了PSTM违反不透明性的实例;实验二对比了PSTM与PSTM-M在任务处理上时间和事务废弃个数的差异,该实验表明为保证更强的安全性,PSTM-M在执行效率上的损失处于可控范围内。接着,本文基于历史模型(History Model)给出不透明性的形式化定义。为简化后续证明,本文给出了保证不透明性成立的三个条件,并证明其与不透明性等价。随后利用输入/输出自动机(Input/Output Automata)给出PSTM-M的形式化描述。基于给出的三个条件并利用数学归纳法,对PSTM-M历史中事务成功提交的个数进行归纳,证明了PSTM-M满足不透明性。最后,为了使证明更具说服力,本文利用定理证明器Coq给出PSTM-M不透明性的机器证明。在证明中,首先利用Coq中的归纳类型将PSTM-M所有可能执行的轨迹,定义成为pstm_trace。接着保留pstm_trace中所有成功提交的事务,形成中间产物cnpt。最后从cnpt出发构建顺序轨迹从而完成PSTM-M不透明性的证明。PSTM-M不透明性的证明,保证了其在高并发下数据读取的正确性,克服了PSTM框架中所存在的缺陷。