软件学院师生获第27届ACM并行程序设计原理与实践国际会议最佳论文

近日，第27届ACM并行程序设计原理与实践国际会议（Principles and Practice of Parallel Programming，PPoPP）在韩国首尔召开。清华大学软件学院贺飞课题组的论文《干扰关系制导的并发程序验证SMT问题求解》（Interference Relation-Guided SMT Solving for Multi-threaded Program Verification）获得会议“最佳论文奖” (best paper award)。该论文由清华大学软件学院独立完成，第一和第二作者分别为软件学院博士研究生范洪宇和硕士研究生刘威廷（已毕业）。

多线程程序被操作系统以时间片轮询的方式调度执行，在对多线程程序执行验证时需要考虑线程之间所有可能的交替执行方式，存在严重的路径空间爆炸问题。特别地，如果考虑多线程程序在多核平台的运行，还需要引入弱内存模型，此时程序执行空间更加复杂，验证难度更大。本论文采用偏序关系对多线程的内存操作进行建模。程序行为（包括控制流行为、数据流行为、对内存访问的偏序关系等）和程序规约都被编码为可满足性模理论（Satisfiability Modulo Theory，SMT）公式，程序是否满足规约的问题被归结为对应的SMT公式是否可满足的问题。论文创新的提出利用并发程序干扰关系，加速SMT的自动推理过程。该方法通过识别决定干扰关系的干扰变量，在约束求解过程中赋予干扰变量更高的优先级，制定变量决策的顺序，进而引导约束求解的搜索过程。该方法有效提高了并发程序验证SMT求解效率。

ACM PPoPP是并行程序领域的国际顶会，主要关注并行程序设计的原理与实践，为CCF推荐A类会议。本次大会共接收29篇论文，其中3篇被评为最佳论文。