弱记忆模型下的并发行为：STSO、指称语义与Pomsets研究

本文主要探讨了在弱记忆模型的背景下，针对并发行为的研究，特别是通过STSO（Store Total Store Order）、指称语义以及pomsets的视角。弱记忆模型是一种理论框架，它具有非组合性质的公理，这在处理程序的模块化推理时带来了挑战。为了克服这个难题，文中提出了一个基于pomsets的表示语义方法，这种技术能够捕捉到并发程序中允许的正确行为，从而支持更有效的模块化分析。 STSO是一种内存模型，它允许对存储的操作进行局部排序，而不是全局排序，这意味着线程可能看到其他线程的操作结果，但不一定按照它们实际执行的顺序。这对于理解现代体系结构中性能优化和弱一致性环境下的行为至关重要。在这个环境中，经典的依赖于顺序一致性假设的并发算法可能会表现出意想不到的行为，如文中提到的Dekker算法在STSO模型中的非预期执行情况。 指称语义作为一种工具，帮助理解程序执行时如何命名和引用共享资源，有助于解决弱内存模型中的问题。通过将并发行为分解为pomsets（过程调用的序列和并行活动的集合），论文构建了一个更为精确和结构化的语义框架，这有助于设计和分析在STSO这样的模型中运行的并发程序。 本文的关键贡献在于，它不仅提出了一个新的分析方法，还展示了如何利用pomsets和指称语义来分析在弱记忆模型——特别是STSO——下的并发行为，这对于理解并设计适应现代硬件架构的并发算法具有重要的理论价值。此外，它还指出了一种在线获取资源的方式，即可以通过《理论计算机科学电子笔记》（Electronic Notes in Theoretical Computer Science，Elsevier出版）第336期的文章查阅相关研究，DOI:10.1016/j.entcs.2018.03.025。 作者R.Kavanagh和S.Brookes在匹兹堡卡内基梅隆大学计算机科学系工作，他们的研究得到了加拿大自然科学和工程研究委员会（NSERC）研究生奖学金的支持。本文作为开放获取作品，遵循CC BY 许可协议，读者可以通过提供的链接访问全文。