基于Pi演算的Android多线程程序的数据竞争检测  

Data Race Detection for Multi-threaded Programs in Android Based on Pi Calculus

作　　者：王涛 马川[2] WANG Tao;MA Chuan(College of Business Administration,Hebei Normal University of Science and Technology,Qinhuangdao Hebei 066004,China;College of Information Science and Engineering,Yanshan University,Qinhuangdao Hebei 066004,China)

机构地区：[1]河北科技师范学院工商管理学院,河北秦皇岛066004 [2]燕山大学信息科学与工程学院,河北秦皇岛066004

出　　处：《广西师范大学学报（自然科学版）》2020年第2期29-42,共14页Journal of Guangxi Normal University:Natural Science Edition

基　　金：河北省社会科学基金(HB18SH012)。

摘　　要：针对事件驱动机制下Android多线程程序的数据竞争问题,构造一个基于Pi演算的并发行为检测模型。利用扩展后的Pi演算对Android生命周期和多线程框架进行建模,得到形式化的行为模型;通过将安全约束抽象为形式化的IF-THEN规则,并利用Pi演算的性质进行进程演算和迁移,构建了检测模型;将动态检测与静态检测以相同的处理方式结合在检测模型中,并给出了并发行为检测算法和数据竞争检测的方法。理论分析和实验表明,本文所提出的方法具有线性的时间和空间复杂度,相比其他方法,在提高检测精确性的同时并没有牺牲检测的效率。To solve the data race problem in Android multi-threaded programs, a model of concurrent behavior detection based on Pi calculus is proposed in this paper. The extended Pi calculus is used to model Android life cycle and multi-threaded framework, and a formal behavior model is obtained. Moreover, the detection model is constructed by abstracting security constraints into formal IF-THEN rules and using the properties of Pi calculus to perform process calculus and migration. The dynamic detection and static detection are combined in the detection model by the same way, and concurrent behavior detection algorithm and data race detection method are given. The analysis and experiment results show that this method has linear time and space complexity. Compared with other methods, the detection accuracy is improved without sacrificing the detection efficiency.

关 键 词：ANDROID APPS 数据竞争 并发行为 进程代数 多线程 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]