随着多线程技术在现代编程中的广泛使用，比如C中的pthread库、Java中的Thread类，人们对多线程程序的安全性越来越重视。原子性错误是并发程序错误的主要类型之一，如何检测和查找复杂并发程序的中的原子性错误具有重要的研究意义。同时，现今大量商业软件是以二进制代码的形式进行发布，这使得针对源代码为分析对象的分析技术无能为力。因此，有必要对二进制多线程程序的原子性错误检测方法进行研究。

对二进制多线程程序做原子性错误检测主要面临三个难点：一是如何区分违反原子性的真正和良性两种情况；二是如何处理多线程程序运行时线程序列不确定的问题；三是如何对二进制代码进行分析，因为对二进制代码比对源代码更难分析。为了解决以上问题，本文提出了基于模型检测的原子性错误检测方法MC-AVIO。该方法包含两个阶段：训练阶段和分析阶段。在训练阶段通过提取原子性迁移对集合的方法来识别真正违反原子性的情况，在分析阶段检测原子性错误时用动态模型检测的方法搜索程序所有可能的线程序列，解决了分析多线程程序时线程序列不确定的问题。另外，在实现MC-AVIO时采用诸如保守分析策略、多次动态分析等轻量级的方法来分析二进制程序。

Today concurrent technology is widely used in programming area, such as pthread library in C, Thread class in Java, etc. Community pays more and more attention on the security of multithreaded programs. Atomicity error is one of main concurrent program errors, it is necessary to propose the checking and testing method to find such errors in complex concurrent programs. Besides, there are many business software whose source code is closed，so source code analysis technologies lose its power in this situation. Based on above facts, it is meaningful to do research on atomicity bug detection on multithreaded binary program.

The difficulty of detecting atomicity bugs in multithreaded binary program lies in three points: One is how to differentiate between true violation and benign violation. Another problem is how to deal with the indetermination of thread running sequence in multithreaded program. Last one is how to analyze binary program, because analyzing binary program is much difficult than program with source code. To address these problems, in this paper a new method, named MC-AVIO, is presented based on dynamic model checking. Our methods consist of two phases: train phase and analysis phase. In train phase, MC-AVIO extracts atomic transition pair to recognize true atomicity violation. In analysis phase, when MC-AVIO detects atomicity errors, it use dynamic model checking explores all possible interleaving to solve the indetermination of thread running sequence while analyzing multithreaded programs. While implementing MC-AVIO, some light weight methods are employed to analyze executable without source code, such as conservative analysis strategy, multiple dynamic analysis, etc.

Based on MC-AVIO method, an atomicity bug detection tool AtomFinder is implemented. Finally, AtomFinder is evaluated by some typical open source benchmark programs, and the result shows that it is effective to detect atomicity errors.