基于操作语义的弱内存模型描述及程序逻辑研究的中期报告.docx

基于操作语义的弱内存模型描述及程序逻辑研究的中期报告
一、研究背景
随着多核处理器的普及，基于弱内存模型的并发程序编写和验证变得越来越重要。弱内存模型（weakmemorymodel）是指多核处理器中的缓存一致性协议（cachecoherenceprotocol）对于多个处理器看到的内存交互操作的顺序存在限制，从而导致程序行为不唯一的情况。例如，x86处理器采用的缓存一致性协议是MESI，而ARM处理器采用的是MOESI。
为了简化程序员对于多核处理器的编程，处理器厂商提供了弱内存模型下的编程接口（例如x86的IntelMemoryModel）。然而，这些接口往往不能完全解决在弱内存模型下并发程序的正确性问题。因此，需要进一步研究弱内存模型下程序的行为和正确性。
二、研究内容
本研究以x86处理器为对象，研究了基于操作语义（operationalsemantics）的弱内存模型下程序的行为和正确性，主要包括以下几个方面：
1.弱内存模型下的操作语义
我们以x86处理器采用的MESI协议为基础，定义了弱内存模型下的操作语义，并给出了相应的语义规则。
2.基于与式辅助记忆的程序逻辑
我们提出了基于与式辅助记忆（separationlogicwithframing）的程序逻辑，以描述弱内存模型下的并发程序。该程序逻辑扩展了传统的Hoare逻辑，支持描述并发程序的内存交互操作（例如读取和写入操作），并且能够捕获弱内存模型下的并发行为。
3.程序正确性的证明方法
我们提出了一种基于程序逻辑的证明方法，用于证明弱内存模型下并发程序的正确性。该方法基于Hoare逻辑规则，先利用程序逻辑推导出程序中每个并发线程的前置条件、后置条件和不变式，然后利用Hoare逻辑规则和线程不变式证明程序的正确性。
三、研究成果
在本中期报告中，我们完成了对基于操作语义的弱内存模型下的并发程序行为和正确性的初步研究，并获得了以下成果：
1.完成了基于MESI协议的操作语义的定义，并给出了语义规则。
2.提出了基于与式辅助记忆的程序逻辑，用于描述弱内存模型下的并发程序。
3.提出了一种基于程序逻辑的证明方法，用于证明弱内存模型下并发程序的正确性。
4.使用了Coq证明助手，初步实现了程序逻辑和证明方法，并在一些简单的并发程序上进行了验证。
下一步工作将进一步完善程序逻辑和证明方法，扩展研究对象和场景，并进一步验证与实验。