近日，中国科技大学计算机科学与技术学院、中国科大－耶鲁高可信软件联合研究中心梁红瑾特任副研究员和冯新宇教授在并发程序验证领域取得重要进展，首次设计出了一种验证并发对象无饥饿性与无死锁性的程序逻辑。该研究成果以“A Program Logic for Concurrent Objects under Fair Scheduling”为题发表在第43届编程语言原理国际会议（ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages，简称POPL）上。该论文是本年度唯一来自中国大陆研究机构的论文。此前，中国大陆研究机构作为第一署名单位仅在POPL上发表过3篇论文，其中第一篇便是由梁红瑾、冯新宇课题组在第39届POPL会议上发表的。

多处理器系统上的并发程序在执行时，有多个线程同时共享系统资源。当对共享资源的管理和使用不当时，常常会出现饥饿、死锁、活锁等活性问题，造成一个或多个线程无限期等待资源而不再响应。由于并发系统自身的复杂性，程序测试难以找出全部问题。梁红瑾等提出了一个新的程序逻辑，能够严格证明一个并发系统不可能出现饥饿、死锁、活锁等问题。该研究工作将并发环境的各种行为分为两类，称为“阻塞”和“延迟”，饥饿、死锁等问题分别对应于这两类并发环境的不同组合。然后，针对阻塞与延迟，分别设计出特定的程序规范和推理规则，保证并发系统最终一定会响应并有所进展。这样得到的程序逻辑具有很好的通用性，可定制为对各个单一性质的验证。该程序逻辑已应用于一些经典并发算法验证，例如，该工作在国际上首次形式化验证了锁耦合链表算法的无饥饿性，以及乐观链表算法和惰性链表算法的无死锁性等。该研究成果为验证实际并发程序的无饥饿性、无死锁性等活性性质提供了理论基础。

POPL是编程语言领域历史最久、水平最高的国际会议，它是讨论编程语言和编程系统最新突破的最主要论坛，内容涵盖编程语言的理论、编程语言的设计、编译器技术、程序分析、程序验证、可信软件等众多研究领域。国际期刊和会议的各种分区方法都把POPL放在该领域的最高区域中。

第43届POPL会议于1月20日至1月23日在美国佛罗里达州圣彼德斯堡召开，梁红瑾应邀报告了该研究成果，与会专家给与了很高评价。

该研究工作得到了国家自然科学基金的资助。

论文链接：

A program logic for concurrent objects under fair scheduling

消息来源：

并发程序验证研究取得重要进展

梁红瑾副研究员简介：

中国科学技术大学计算机科学与技术学院副教授，Email：lhj1018@ustc.edu.cn

个人主页：http://staff.ustc.edu.cn/~lhj1018/

主要研究方向： 程序验证、并发理论、程序设计语言理论

冯新宇教授简介：

中国科学技术大学计算机科学与技术学院教授，博士生导师

Email：xyfeng@ustc.edu.cn 

个人主页：http://staff.ustc.edu.cn/~xyfeng/

主要研究方向：程序验证、并发理论、程序设计语言理论。

个人简介：

冯新宇，男，1978年生；教授，博士生导师。分别于1999年和2002年在南京大学获学士和硕士学位；2007年于耶鲁大学获博士学位。2001年7月至2002年1月于香港理工大学担任研究助理。2007年9月至2010年5月于Toyota Technological Institute at Chicago (TTIC)任研究助理教授（Research Assistant Professor）。2010年5月加入中国科学技术大学计算机科学与技术学院任教授。主要从事程序验证、并发理论、程序设计语言理论方面的研究，在POPL、PLDI、ESOP、ICFP和CONCUR等知名国际会议和期刊上发表论文10余篇。曾担任APLAS’08和TASE’09的程序委员会成员。

(本文资料来源：中国科技大学）

如若转载，请注明e科网。

如果你有好文章想发表or科研成果想展示推广，可以联系我们或免费注册拥有自己的主页