共享内存系统

共享内存把通信编码在共同状态里。写者不指定收件人，读者也不接收显式消息；信息是否传到另一个线程，取决于读到了哪次写以及同步是否建立了可见性。分析者能看到完整配置，进程本身却只能通过获准的对象操作观察其中一小部分。

源代码的一行常包含多个底层动作。x = x + 1 至少要读、计算、写；即使单次字读写原子，整个复合更新也未必原子。读到的值先进入进程局部状态，随后计算不会因别人改写共享变量而自动更新。因此分析配置既要记共享值，也要记每个进程读到的暂存值与下一条指令，才知道后续哪些写仍然可能发生。

上述一步一个基础操作的交错表示，是常用的原子共享对象模型。若分析硬件弱内存，$m$ 必须包含模型所需的缓冲或传播状态，或改用带读值关系的公理化执行；不能只保留一个“所有线程立即看到”的整数状态，却声称已经包含任意弱内存行为。

在把普通访问抽象成顺序一致的原子寄存器读写时，从共享整数 $x=0$ 开始，进程 $p,q$ 都执行 x = x + 1。一种合法的细粒度交错是

最终 $x=1$。丢失更新来自复合操作被拆开；把单次读写称为原子寄存器仍不能排除它。若改用一次原子 fetch_add(1)，两次 RMW 在对象规格中不可分割，最终值才必为 $2$，但返回值的先后仍由调度决定。

多字结构还可能产生混合快照。若写者依次把 (version,payload) 从 (0,A) 改为 (1,B)，无同步读者可能观察到 (1,A)；两个字段各自原子不等于跨字段不变量原子。这个反例甚至不需要弱内存：写版本、读版本、读载荷、写载荷就是一个顺序一致交错。解决方案可以是锁、版本校验或线性一致的多字对象，所需保证必须写进接口。

仅“读版本—读载荷—再读版本，两次版本相等就接受”也未必修好该例：写者改版本后暂停，读者两次都读到 1，仍会接受旧载荷。采用版本校验必须设计完整协议，例如用奇偶版本明确标出写入中，并配合规定的内存序；检验不是一个可以脱离写协议独立添加的补丁。

与消息传递系统公理库消息传递系统Message-passing system进程仅通过发送和接收消息交互的分布式模型。相比，共享内存没有独立的在途消息状态；消息模拟共享寄存器时，需要服务器副本、请求—响应与 quorum 才能定义读写结果。反方向用共享队列模拟消息，也要另行规定队列原子性和进展。两种模型可相互模拟，不表示故障成本或可解性条件相同。

抽象数据类型公理库抽象数据类型Abstract data type · ADT由值集合与操作语义定义、独立于具体表示的数据接口。给出共享对象的顺序规格，RMW公理库读改写原语Read-modify-write operation · RMW将读取旧状态、依据旧状态决定更新及返回结果合为一个原子状态转移的同步原语；其内存序和进度保证需另行规定。 提供不可分割更新基础。互斥锁公理库互斥锁Mutex · Mutex lock · 互斥量以获取、释放与所有权封装临界区互斥的同步对象。、自旋锁公理库自旋锁Spinlock · Spin lock获取失败时以原子操作持续轮询、等待锁在短时间内释放的互斥锁实现族。、信号量与条件变量分别约束所有权、等待方式和唤醒条件；调用方式相似并不会自动给出相同公平性或故障行为。

数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。从语言内存模型侧识别未排序的冲突访问，SC-for-DRF 则在模型特定前提下把 race-free 程序映回较强语义。对象层的线性一致性、算法层的互斥与 lock-free 进展回答不同问题：历史可能线性一致却让某个线程永远饥饿，也可能无数据竞争却仍有检查—行动逻辑错误。