“在共享内存系统中,信号量是带非负整数状态 $S\in\mathbb N$ 的同步对象。其两个基本原子操作通常记为 $P/V$、 或 :”
形式陈述 ​
共享内存计算模型固定进程集合
一次原子步由某个进程执行局部计算,或对一个基础对象完成规格允许的原子操作,并据此改变自己的局部状态与
模型还必须声明三类参数。第一,基础对象提供普通读写、原子寄存器还是 read-modify-write;第二,底层内存一致性模型允许哪些读值与重排;第三,哪些无限执行算可容许,例如正确进程是否持续获得步骤。安全性通常量化所有符合对象和内存模型的交错;wait-free、lock-free、无饥饿等进展性质还需分别绑定进程故障与公平性,不能从“共享内存”四字推出。
进程通过共享对象间接通信。例如原子寄存器提供
顺序概念要按层分开。程序顺序只排列同一进程的动作;happens-before再加入同步边并取传递闭包,通常仍是偏序;顺序一致性寻找一个保留程序顺序、能解释所有读值的全序;线性一致性针对对象历史,还保留不重叠操作的实时顺序。原子寄存器是一种对象规格,不是这些关系的别名。
直觉
共享内存把通信编码在共同状态里。写者不指定收件人,读者也不接收显式消息;信息是否传到另一个线程,取决于读到了哪次写以及同步是否建立了可见性。分析者能看到完整配置,进程本身却只能通过获准的对象操作观察其中一小部分。
源代码的一行常包含多个底层动作。x = x + 1 至少要读、计算、写;即使单次字读写原子,整个复合更新也未必原子。可靠证明应先确定基础原语与内存模型,再把高级操作精化到这些步骤,而不能从语句外形推断不可分割性。
例子与边界
在把普通访问抽象成顺序一致的原子寄存器读写时,从共享整数 x = x + 1。一种合法的细粒度交错是
最终 fetch_add(1),两次 RMW 在对象规格中不可分割,最终值才必为
多字结构还可能产生混合快照。若写者依次把 (version,payload) 从 (0,A) 改为 (1,B),无同步读者可能观察到 (1,A);两个字段各自原子不等于跨字段不变量原子。解决方案可以是锁、版本校验或线性一致的多字对象,所需保证必须写进接口。
与消息传递系统相比,共享内存没有独立的在途消息状态;消息模拟共享寄存器时,需要服务器副本、请求—响应与 quorum 才能定义读写结果。反方向用共享队列模拟消息,也要另行规定队列原子性和进展。两种模型可相互模拟,不表示故障成本或可解性条件相同。
推论与应用
抽象数据类型给出共享对象的顺序规格,RMW 提供不可分割更新基础。互斥锁、自旋锁、信号量与条件变量分别约束所有权、等待方式和唤醒条件;调用方式相似并不会自动给出相同公平性或故障行为。
数据竞争从语言内存模型侧识别未排序的冲突访问,SC-for-DRF 则在模型特定前提下把 race-free 程序映回较强语义。对象层的线性一致性、算法层的互斥与 lock-free 进展回答不同问题:历史可能线性一致却让某个线程永远饥饿,也可能无数据竞争却仍有检查—行动逻辑错误。
参考资料
- Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996,Chs. 9–13。
- Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004,Chs. 4–5。
- Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012,Chs. 2–3。