专利详情

专利名称	基于确定性重放的并行系统弱一致性的验证方法和系统
申请号	CN201310269957.1	专利类型	发明专利
公开（公告）号	CN103365776A	公开（授权）日	2013.10.23
申请（专利权）人	中国科学院计算技术研究所	发明（设计）人	冯晓雪;陈云霁;李磊;李梦竹
主分类号	G06F11/36(2006.01)I	IPC主分类号	G06F11/36(2006.01)I;G06F9/46(2006.01)I
专利有效期	基于确定性重放的并行系统弱一致性的验证方法和系统至基于确定性重放的并行系统弱一致性的验证方法和系统	法律状态	实质审查的生效
说明书摘要	本发明公开了一种基于确定性重放的并行系统弱一致性的验证方法和系统。包括：数据竞争检测步骤，检测并行测试程序中存在的数据竞争操作，识别所有全局共享变量，对并行测试程序进行两次编译生成第一、二可执行文件,分别注入记录序信息函数和重放序信息函数；记录执行步骤，在待验证的并行系统上，执行第一可执行文件，调用记录序信息函数，记录所有同步操作和数据竞争操作的执行信息生成记录文件，获得全局共享变量值；重放执行步骤，在弱一致性正确的并行系统上，调用重放序信息函数约束执行第二可执行文件，再次获得全局共享变量值；状态比较步骤，如果两次全局共享变量的值相同，此次执行满足弱一致性，否则待验证的并行系统不满足弱一致性。