近日，我校计算机科学与技术学院、中国科大－耶鲁高可信软件联合研究中心梁红瑾特任副研究员和冯新宇教授在并发程序验证领域取得重要进展，首次设计出了一种验证并发对象无饥饿性与无死锁性的程序逻辑。该研究成果以“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日在美国佛罗里达州圣彼德斯堡召开，梁红瑾应邀报告了该研究成果，与会专家给与了很高评价。
该研究工作得到了国家自然科学基金的资助。
论文链接：http://dl.acm.org/citation.cfm?id=2837635
（计算机学院、中国科大－耶鲁高可信软件联合研究中心）
