公开(公告)号：CN103365776B

公开(公告)日：2016-04-13

申请号：CN201310269957.1

申请日：2013-06-28

Applicant: 中国科学院计算技术研究所

Inventor： 冯晓雪 ,  陈云霁 ,  李磊 ,  李梦竹

IPC: G06F11/36 ,  G06F9/46

Abstract: 本发明公开了一种基于确定性重放的并行系统弱一致性的验证方法和系统。包括：数据竞争检测步骤，检测并行测试程序中存在的数据竞争操作，识别所有全局共享变量，对并行测试程序进行两次编译生成第一、二可执行文件,分别注入记录序信息函数和重放序信息函数；记录执行步骤，在待验证的并行系统上，执行第一可执行文件，调用记录序信息函数，记录所有同步操作和数据竞争操作的执行信息生成记录文件，获得全局共享变量值；重放执行步骤，在弱一致性正确的并行系统上，调用重放序信息函数约束执行第二可执行文件，再次获得全局共享变量值；状态比较步骤，如果两次全局共享变量的值相同，此次执行满足弱一致性，否则待验证的并行系统不满足弱一致性。

公开(公告)号：CN103365776A

公开(公告)日：2013-10-23

申请号：CN201310269957.1

申请日：2013-06-28

Applicant: 中国科学院计算技术研究所

Inventor： 冯晓雪 ,  陈云霁 ,  李磊 ,  李梦竹

IPC: G06F11/36 ,  G06F9/46

Abstract: 本发明公开了一种基于确定性重放的并行系统弱一致性的验证方法和系统。包括：数据竞争检测步骤，检测并行测试程序中存在的数据竞争操作，识别所有全局共享变量，对并行测试程序进行两次编译生成第一、二可执行文件,分别注入记录序信息函数和重放序信息函数；记录执行步骤，在待验证的并行系统上，执行第一可执行文件，调用记录序信息函数，记录所有同步操作和数据竞争操作的执行信息生成记录文件，获得全局共享变量值；重放执行步骤，在弱一致性正确的并行系统上，调用重放序信息函数约束执行第二可执行文件，再次获得全局共享变量值；状态比较步骤，如果两次全局共享变量的值相同，此次执行满足弱一致性，否则待验证的并行系统不满足弱一致性。