期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

一种并发程序原子性错误的检测方法及工具 被引量：2

A METHOD OF DETECTING ATOMICITY BUGS FROM CONCURRENT PROGRAMS AND ITS TOOL
在线阅读 下载PDF
导出
摘要 原子性错误的检测对于多线程程序并发错误的分析有着重要意义,其检测难点在于从违反原子性的情况中识别出会导致程序出错的执行序列。为了解决这个问题,采用测试训练提取原子性迁移对集合以及模型检测方法,提出原子性错误自动检测算法MC-AVIO。基于MC-AVIO实现原子性错误检测工具AtomFinder,通过对多组开源软件的测试,证明MC-AVIO对原子性错误的检测是有效的。 Detection of atomicity bug is valuable for analysing the concurrent errors of multi-thread programs development.The main difficulty of the detection lies on how to recognise the execution sequence leading to program error from the cases of atomicity violations.To address this problem,we adopt a method of extracting atomic transition pairs by training test and a method of model detection,and present a new method named MC-AVIO which is an automatic atomicity bug detection method.Moreover,we implement a detecting tool AtomFinder for atomicity bug based on MC-AVIO.After testing several groups of open source software,it is proved that MC-AVIO is efficient in detecting atomicity bugs.
作者 李潇 刘剑 易秋萍
机构地区 中国科学院软件研究所
出处 《计算机应用与软件》 CSCD 北大核心 2012年第11期92-94,100,共4页 Computer Applications and Software
基金 国家"核高基"重大科技专项(2010ZX01036-001-002-2) 中国科学院知识创新工程重要方向性项目(KGCX2-YW-12)
关键词 多线程程序 原子性错误 线程序列的不确定 模型检测 Multi-thread program Atomicity bug Non-deterministic of thread sequence Model checking
分类号 TP312 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献14

  • 1Xu M, Bodik R, Hill M O. A serializability violation detector for shared-memory server programs [ C ]//Proc. of the 2005 ACM PLDI. New York, NY, USA : ACM Press ,2005.
  • 2Yang Y. Runtime Model Checking of Muhithreaded C/C + + Programs[M].
  • 3Ball T, Rajamani S. The SLAM Toolkit[C]//Proc. of 13th International Conf. CAV 2001. Paris, France : Springer,2001.
  • 4Henzinger T, Jhala R, Majumdar R, et al. Lazy Abstraction [ C ]// POPL'02 Proc. of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA : ACM Press, 2002.
  • 5Godefroid P. Model Checking for Programming Languages using VeriSoft[ C]//Proc. of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA : ACM Press, 1997.
  • 6Visser W, Havelund K, Brat G, et al. Model Checking Programs [ C ]// The Fifteenth IEEE International Conf. on ASE,2000.
  • 7Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem [ C ]//Lecture Notes in Computer Science. Paris : Springer-Verlag, 1996.
  • 8Flanagan C, Godefroid P. Dynamic Partial-Order Reduction for Model Checking Software POPL' 2005 [ M ]. New York : ACM press,2005.
  • 9http ://www. pihtool. org/.
  • 10Bradbury S,Cordy R,Dingel J. Mutation Operators for Concurrent Java [C]//Mutation Analysis, 2006, Second Workshop on. Washington : IEEE Computer Society,2006.

同被引文献19

  • 1Wang C, Yang Y, Gupta A, et al. Dynamic model checking with proper- ty driven pruning todetect race conditions[ C ]//Automated Technology for Verification and Analysis. Springer,2008.
  • 2Xu M, Bodik R, Hill M D. A serializability violation detector for shared- memory server programs [ C ]//Proc. of the 2005 ACM PLDI. New York, NY, USA : ACM Press ,2005.
  • 3Yang Y. Runtime Model Checking of Muhithreaded C/C + + Programs [ R]. School of Computing, University of Utah,2007.
  • 4Lu S,Tucek J, Qin F, et al. Detecting Atomicity Violations via Access Interleaving Invariants [ C ]//Proc. of the 12tb international cone on ASPLOS. New York, NY, USA : ACM press,2006.
  • 5Engler D,Ashcraft K. RacerX:effective, static detection of race condi- tions and deadlocks[ C]//ACM Symposium on Operating Systems Prin- ciples, ACM ,2003:237 - 252.
  • 6Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software [ C ]//Principles of programming languages, 2005 : 110 -121.
  • 7Visser W, Havelund K, Brat G, et al. Model Checking Programs [ C ]. The Fifteenth IEEE International Conf. on ASE 2000.
  • 8Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem [ C ]//Volume 1032 of Lecture Notes in Computer Science. Paris: Springer- Verlag, 1996.
  • 9Flanagan C, Godefroid P. Dynamic Partial-Order Reduction for Model Checking Software POPL2005 [ C ]//New York : ACM press ,2005.
  • 10http ://www. pintool. org/.

引证文献2

二级引证文献1

计算机应用与软件
2012年 第11期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部