Hardware Memory Models
这是Go语言作者之一的rsc语言内存模型相关博文之一;硬件内存模型的笔记。硬件内存模型对应的是汇编指令的执行,可以认为每一条指令原子执行。
Sequential Consistency 顺序一致性模型
多个进程的操作按照一定顺序执行,同一个进程的操作按顺序执行,不同进程操作可以交叉进行。
litmus test:
x86 Total Store Order Model (x86-TSO)
该模型和顺序模型一样采用共享内存,不同之处在于有一个每个进程有一个FIFO写入队列,写操作会先写入队列,适时执行。而读取时会先查询自己的写队列,再查询Shared Memory。
litmus test:
验证写队列:
各进程视角内写入顺序一致
ARM/POWER Relaxed Memory Model 宽松内存模型
ARM架构采用宽松的内存模型。各进程 不再共享内存,而是保有自己的内存副本,读写操作都操作自己的副本。
写操作的扩散(从一个副本到另一个副本)是无序的,这意味着不同进程副本所看到的写顺序可能是不一致的。
另外对于一个进程内操作而言,读操作可以被推迟到写操作之后。
Weak Ordering and Data-Race-Free Sequential Consistency
硬件内存模型是复杂且微妙的,如果每次编程都要考虑这些,心智负担就太重了。如果遵循一定的规则编程就可以做到顺序一致的执行就太好了,以下就是一个方法。
“weak ordered"出自论文“Weak Ordering – A New Definition”, 定义如下:
定义同步模型为一组内存访问约束,这些约束指定了如何,何时进行同步。硬件相对于同步模型是弱序的,当且仅当对于一切遵守同步模型的软件在硬件上运行满足顺序一致性。
”Data-Race-Free(DRF)“是 Adve和Hill提出的一个同步模型。该模型假设硬件有常规读写的内存同步操作。同步操作间的常规读写也许会打乱顺序,带却不允许跨越同步操作(类似内存屏障)。如果对于所有理想化的顺序一致执行,不同进程对同一个位置的内存操作,要么两者都是读,要么由同步操作规定先后发生顺序。那么程序被认为是data-race-free的。
示例:
原论文中有给出相关证明。这为硬件和软件开发提供准则。
小结
阅读rsc的博文对硬件内存模型有了一定的了解,这篇文章是基于汇编指令访存写的,对高级语言而言又有不同,这就是下一篇文章了。
参考
rsc. Hardware Memory Models[EB/OL]. [2022.12.06]. https://research.swtch.com/hwmm#drf.
Memory Models[EB/OL]. [2022.12.06]. https://research.swtch.com/hwmm#drf.