程序语言的内存模型规定了在程序执行的过程中内存访问是如何发生的。它作为桥梁将为程序员和语言实现连接起来,帮助程序员写出正确的并发程序。在现实世界中,大多数的硬件和编译系统都是基于弱内存模型的假设,即内存访问并不是严格按照程序顺序执行,以用来支持各类优化。本文研究了弱内存模型的设计,并提出了可以支持在弱内存模型上进行程序验证的程序逻辑。具体来说,本文在弱内存模型和程序逻辑方面做出了如下的贡献：首先,本文提出一种新的弱内存模型OHMM,这是Happens-before内存模型(HMM)的变种。这个模型通过对一个简单语言赋予具体的操作语义,并通过它在抽象机上的程序行为来模拟HMM。由于OHMM所允许的程序行为是通过操作语义自然生成的,所以它自然而然的避免了所谓的凭空出现(out-of-thin-air)的程序行为。另外一方面,OHMM使用一种我们称之为重放的机制来允许某些符合一定条件的指令在抽象机上能够多次执行,来模拟现实世界中编译器和处理器优化中的投机执行和优化。总的来说,我们的模型对于无锁程序的约束会比Java内存模型(JMM)更加弱一些,因此我们将会允许更多的编译器优化算法在我们的模型上能够使用。同时,在OHMM上,程序行为在直观上会比JMM更加自然。许多在JMM上可能出现但是明显违反直观认识的程序,在我们的模型上就不再合法。我们希望OHMM可以成为可供类Java语言选择的一种新内存模型。其次,本文提出一种新的用于验证并发程序在TSO(Total Store Order)弱内存模型下正确性的程序逻辑。TSO模型所允许的弱行为是OHMM的子集。我们知道,TSO模型已经被用作X86和SPARC-TSO处理器族的模型基础,并且在一些高级语言中也正在被提案作为其内存模型的基础。我们的逻辑对LRG(Local Rely-Guarantee)进行扩展,对其加入了关于TSO写缓存的断言,这可以让我们对TSO模型中对外部线程不可见的局部的写缓存的状态进行描述。如同LRG一样,我们的程序逻辑支持对细粒度并发具有表达力强的rely/guarantee推理以及分离逻辑中的局部推理。同时,我们在逻辑上对TSO模型进行进一步抽象,把TSO共享内存分为local和shared两部分,这可以允许我们可以将那些在访问时只有单个线程能够访问的内存单元(逻辑上等同于local单元)的写操作直接写入内存,不需要经过写缓存。我们使用这个逻辑证明了一些具有代表性的并发算法在TSO上的正确性,包括Peterson’s lock算法,Simpson’s four slot算法,concurrent GCD算法以及lock的优化实现算法。