无阻碍性是一种经典的描述并发对象的进展性(progress)的性质，用于给用户程序提供终止性方面的保证(即描述当用户调用对象的方法时，在什么情况下一定能够返回)。因为其独特的优势，满足此性质的实现已经应用在了某些实际的场景中，如软件事务内存(software transactional memory)和匿名且错误耐受的分布式计算(anonymous and fault-tolerant distributed computing)。但是，现有的验证工作并不支持对于无阻碍性的验证，或者只支持对少数特定种类实现的验证。
为了填补这一空白，南京大学冯新宇教授团队撰写了论文：验证无阻碍性的程序逻辑。
文章信息
标 题：
A program logic for obstruction-freedom
引用格式：
Zhao-Hui LI, Xin-Yu FENG. A program logic for obstruction-freedom. Front. Comput. Sci., 2024, 18(6): 186208
阅读原文：
文章概述
本文首次提出了一个能够验证无阻碍性的程序逻辑，而且它同时也能够验证线性一致性(一种功能正确性)。此外，还总结了一套简单易懂的方法，可以将一个只能验证线性一致性的程序逻辑扩展成支持验证无阻碍性。最后，使用此程序逻辑验证了一个实用的无阻塞双端队列的实现满足无阻碍性，此实现来自于首先提出无阻碍性定义的那篇经典论文。
技术步骤
在尝试解决问题的过程中，本文发现，如果将无阻碍性视为一种传统的进展性性质，并通过证明“最终一定会发生某些好的事情”的思路来验证它，那么将不可避免地会遇到棘手的问题。为了解决这个问题，受验证安全属性 (safety property) 的方法的启发，他们采用了一种间接的方法，即通过证明“某些坏的事情永远不会发生” 的思路来验证无阻碍性。具体来说，通过无阻碍性的定义，他们发现无阻碍性允许由无限次的干扰 (interference，即并发环境中其他线程的行为) 所引起的发散 (divergence，即不终止的执行)，但不允许由有限的干扰引起的发散。因此，他们通过防止由有限的干扰引起的发散来证明无阻碍性。为了验证不存在这样的发散，他们设计了一种简单的方法，只需要在标准的 while 规则中添加一个副条件（一个串行环境下的完全正确性断言）。
未来展望
在未来，作者希望设计自动化验证非阻碍性的工具。因为已经提出了一套简单易懂的方法可以将现有的验证线性一致性的逻辑拓展成验证非阻碍性的逻辑，所以作者觉得也许可以用这种方法来将现存的验证线性一致性的自动化工具拓展成验证非阻碍性。
相关内容推荐：
文章精要 | 南京大学李宣东教授团队：通过实证研究重新审视与加强Bug和非Bug问题的自动分类 2024 18(5)：185207
文章精要 | 北京航空航天大学肖利民教授等：通过模型和量化分析最小化周期性复制系统中的同步成本 2024 18(5)：185205
文章精要 | 北京航空航天大学杨海龙副教授团队：面向申威众核处理器的深度学习张量优化代码生成技术 2024 18(1)：181201
文章精要 | BTC-阴影: 一个用于揭示比特币交易图中非法行为的可视化分析系统 2023 17(6)：176215
文章精要 | 迭代式安卓自动化测试 2023 17(5)：175212
文章精要 | 华中科技大学刘海坤教授团队：UCat：面向Unikernel的异构内存管理机制 2023 17(1)：171204
《前沿》系列英文学术期刊
由教育部主管、高等教育出版社主办的《前沿》（Frontiers）系列英文学术期刊，于2006年正式创刊，以网络版和印刷版向全球发行。系列期刊包括基础科学、生命科学、工程技术和人文社会科学四个主题，是我国覆盖学科最广泛的英文学术期刊群，其中12种被SCI收录，其他也被A&HCI、Ei、MEDLINE或相应学科国际权威检索系统收录，具有一定的国际学术影响力。系列期刊采用在线优先出版方式，保证文章以最快速度发表。
《前沿》系列英文学术期刊 中国学术前沿期刊网 http://journal.hep.com.cn/ |
