无阻碍性是一种经典的描述并发对象的进展性(progress)的性质，用于给用户程序提供终止性方面的保证(即描述当用户调用对象的方法时，在啥状况下一定能返回)。因为其独特的优势，满足此性质的实现已经应用在了某些实际的场景中，如软件事务内存(software transactional memory)和匿名且错误耐受的分布式计算(anonymous and fault-tolerant distributed computing)。但是，现有的验证工作并不支持对于无阻碍性的验证，或者只支持对少数特定种类实现的验证。

  为了填补这一空白，南京大学冯新宇教授团队撰写了论文：验证无阻碍性的程序逻辑。

  本文首次提出了一个能够验证无阻碍性的程序逻辑，而且它同时也能够验证线性一致性(一种功能正确性)。此外，还总结了一套简单易懂的方法，可以将一个只能验证线性一致性的程序逻辑扩展成支持验证无阻碍性。最后，使用此程序逻辑验证了一个实用的无阻塞双端队列的实现满足无阻碍性，此实现来自于首先提出无阻碍性定义的那篇经典论文。

  在尝试处理问题的过程中，本文发现，如果将无阻碍性视为一种传统的进展性性质，并通过证明“最终一定会发生某些好的事情”的思路来验证它，那么将不可避免地会遇到棘手的问题。未解决这个问题，受验证安全属性 (safety property) 的方法的启发，他们采用了一种间接的方法，即通过证明“某些坏的事情永远都不可能发生” 的思路来验证无阻碍性。具体来说，通过无阻碍性的定义，他们发现无阻碍性允许由无限次的干扰 (interference，即并发环境中其他线程的行为) 所引起的发散 (divergence，即不终止的执行)，但不允许由有限的干扰引起的发散。因此，他们通过防止由有限的干扰引起的发散来证明无阻碍性。为了验证不存在这样的发散，他们设计了一种简单的方法，只需要在标准的 while 规则中添加一个副条件（一个串行环境下的完全正确性断言）。

  在未来，作者希望设计自动化验证非阻碍性的工具。因为已经提出了一套简单易懂的办法能够将现有的验证线性一致性的逻辑拓展成验证非阻碍性的逻辑，所以作者觉得也许可以用这种方法来将现存的验证线性一致性的自动化工具拓展成验证非阻碍性。

  文章精要 南京大学李宣东教授团队：通过实证研究重新审视与加强Bug和非Bug问题的自动分类 2024 18(5)：185207

  文章精要 北京航空航天大学肖利民教授等：通过模型和量化分析最小化周期性复制系统中的同步成本 2024 18(5)：185205

  文章精要 北京航空航天大学杨海龙副教授团队：面向申威众核处理器的深度学习张量优化代码生成技术 2024 18(1)：181201

  文章精要 BTC-阴影: 一个用于揭示比特币交易图中非法行为的可视化分析系统 2023 17(6)：176215

  Frontiers of Computer Science （FCS）是由教育部主管、高等教育出版社和北京航空航天大学共同主办、SpringerNature 公司海外发行的英文学术期刊。本刊于 2007 年创刊，双月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为周志华教授，共同主编为熊璋教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”；入选“中国科技期刊卓越行动计划项目”。

  由教育部主管、高等教育出版社主办的《前沿》（Frontiers）系列英文学术期刊，于2006年正式创刊，以网络版和印刷版向全球发行。系列期刊包括基础科学、生命科学、工程技术和人文社会科学四个主题，是我国覆盖学科最广泛的英文学术期刊群，其中12种被SCI收录，其他也被A&HCI、Ei、MEDLINE或相应学科国际权威检索系统收录，具有一定的国际学术影响力。系列期刊采用在线优先出版方式，保证文章以最快速度发表。

  特别声明：本文转载只是出于传递信息的需要，并不代表代表本网站观点或证实其内容的真实性；如别的媒体、网站或个人从本网站转载使用，须保留本网站注明的“来源”，并自负版权等法律责任；作者若不希望被转载或者可以联系转载稿费等事宜，请与我们接洽。

  FESE Drew Shindell院士：极端野火已成为全球性环境挑战

  FCS 文章精要：扬州大学李云教授团队等——表示学习：用于个性化推荐的串行自动编码器

  FCS 文章精要：天津理工大学张德干教授团队——移动边缘计算中基于多用户强化学习的任务迁移

  FIE 德国科学院院士、莱布尼茨催化所所长Matthias Beller教授等：氨基酸促进锰催化二氧化碳可逆加氢制甲酸