基于预测性分析的安卓应用程序数据竞争检测

摘要

本发明方法是基于安卓开发框架和其多线程模型，插桩安卓应用程序并动态运行提取单个执行轨迹，再使用预测性分析方法对执行轨迹进行分析，构造其活动间的发生序关系(Happens-Before)并预测生成多个执行轨迹，在此基础上结合变量松弛和路径松弛对执行轨迹中的所有活动进行约束编码，最终放入约束求解器中进行求解来完成数据竞争的检测。本发明能有效降低数据竞争的误报率，扩展性好，效率高，只需收集单个运行轨迹，大大降低了人工成本。

说明书

技术领域

本发明属于计算机技术领域，尤其是软件技术领域。本发明提供了一种使用 预测性分析方法检测安卓应用程序中的数据竞争问题，用于软件质量保障。

背景技术

网络时代中，移动手机携带方便，其上应用程序(MobileApp)得到了广泛用 户的青睐。由于安卓的开放性以及无缝结合的众多Google应用，使得厂商可以 低成本地推出丰富多彩、各具特色的多种产品。安卓所占市场份额从2013年第 二季度的79.6％增长到了2014年第二季度的84.7％。但由于安卓平台的开放性 和自由性，安卓应用程序具有种类繁多、异构自治的特点，且开发门槛低、开源 代码的盛行使得应用程序在软件质量上先天不足，如何保证安卓应用的质量对开 发人员来说是一个巨大的难题。

安卓应用程序是事件驱动的，且安卓系统具有独特的线程机制、回调方法和 多入口等特性。安卓系统为开发人员提供4大组件：

(1)活动，Activity，为用户提供了可以与之进行交互的界面，每一个用户交 互的界面都是一个Activity并且整个应用程序中有一个mainActivity，即 最初用户启动时候所进入的界面；

(2)服务，Service，在后台执行长时间运行的任务，其他的组件可以开启并 且绑定一个Service；

(3)内容提供者，ContentProviders，提供了在安卓系统中的一种数据存储管 理机制，其它组件可以把必要的数据存取在ContentProviders中用于和 用户之间信息的交流；

(4)广播，Broadcast，用来监听安卓系统所产生的一些活动，比如接受信息、 接受电话等，App会通过BroadcastReceiver接受此类活动，并通过它可 以做出相应处理。

安卓系统通过调用一系列的组件的生命周期方法来管理组件的运行。创建一 个新的组件，必须要继承一个安卓系统已经提供的组件类。在子类中，也必须要 实现一些固定的回调方法，用于在组件进行状态转换时能很好地管理组件的运行。

在Activity中有以下几种生命周期的回调方法：

1.onCreate()：创建；

2.onStart()：在onCreate()回调方法后立即调用启动；

3.onResume()：所处状态用户可以与界面进行交互；

4.onPause：暂停当前组件；

5.onStop()：停止并释放一些资源；

6.onDestory()：摧毁组件；

7.onRestart()：重启组件。

Service则是以下回调方法：

启动Service：onCreate()，onStartCommand()，onDestroy()；

绑定Service：onCreate()，onBind()，onUnBind()，onDestroy()。

默认情况下，安卓系统中一个应用的所有组件运行在相同的处理器和相同的 线程上面。当然也可以通过设置组件的Android：process属性来指定所运行的处 理器。在组件运行当中，考虑到运行的效率，开发人员经常使用不同的线程执行 不同的任务，以提高应用的性能。从应用启动开始，系统会维持一个主线程，贯 穿应用的整个生命周期，用于分配活动、管理界面、处理相应逻辑操作。同时开 发者会创建额外的异步线程来并发进行相应工作，也称之为工作线程，包括：直 接继承Thread类或实现Runnable接口；开启或绑定一个额外的Service在后台 执行任务；使用AsyncTask开启一个工作线程执行异步任务。

由于安卓系统的多线程机制和其特有的回调方法，开发人员很容易会写出导 致流程中存在诸如死锁、执行不可达活动、数据竞争等问题的代码，其中数据竞 争现象最为普遍。数据竞争是指：在多线程程序中，不同线程的两个操作对相同 的共享变量的访问没有特定的顺序，且其中至少有一个是写操作的情况。一旦数 据竞争发生，则可能导致应用程序奔溃、数据不一致等情况，带来严重危害。

传统并发程序领域对数据竞争进行了比较深入的研究，常用的方法有基于发 生序和基于锁集的检测方法。在安卓应用程序数据竞争检测方面，现有方法局限 于发生序。本发明将提供一种新的、基于预测性分析的方法来检测安卓应用程序 中的数据竞争问题，以提高检测的精度和效率。

发明内容

本发明要解决的问题是：模拟安卓应用程序运行环境，制定安卓并发语义规 则，并使用新的、基于预测性分析的检测技术来检测安卓应用程序的数据竞争， 以保障其质量。

本发明的技术方案为：基于预测性分析的安卓应用程序数据竞争检测，其特 征是基于安卓开发框架和其多线程模型，插桩安卓应用程序并动态运行提取单个 执行轨迹，再使用预测性分析方法对执行轨迹进行分析，构造其活动间的发生序 关系(Happens-Before)并预测生成多个执行轨迹，在此基础上结合变量松弛和 路径松弛对执行轨迹中的所有活动进行约束编码，最终放入约束求解器中进行求 解，来完成数据竞争的检测。

发明具体包括以下步骤：

1)根据安卓开发框架和其多线程模型，设计插桩点和所要记录的活动，插 桩安卓应用源程序，并动态执行获得单个执行轨迹。

2)根据安卓应用程序的并发语义规则，构造执行轨迹的Happens-Before关 系集。

3)分析执行轨迹的Happens-Before关系集，使用预测性分析方法合理改变 活动之间的调度，以生成多个执行轨迹。

4)对执行轨迹中的所有活动进行约束编码，并结合变量松弛和路径松弛降 低误报率。

5)通过约束求解器求解约束条件，完成数据竞争的检测。

步骤1)中，分析安卓开发框架，结合其特有的多线程模型，插桩原安卓应 用程序，动态运行以获取安卓应用执行轨迹。

其中，执行轨迹T＝<e₁，e₂，…，e_n>是一个活动流，对于源程序SourceAPK， 我们认为其内的每一个语句都进行了不同的操作，称其为活动。我们记录其中与 并发相关、可能会导致数据竞争的活动，包括：线程的初始化、开启一个线程等 线程操作；共享变量的读写操作；锁集的申请释放操作；与任务相关的授权、开 始、结束任务等操作。

步骤2)中，基于安卓的并发语义规则，构造活动间的Happens-Before关系 集。安卓的并发语义规则包括线程内规则(Intra-ThreadHappens-Before)、线程间 规则(Inter-ThreadHappens-Before)、回调方法规则(CallBackHappens-Before)。

线程内规则包括：线程内序列(Order-Intra)、线程内授权分配(PowerPost-Intra)、 线程内分配开始(PostBegin-Intra)、任务原子性(TaskAtomic-Intra)、活动传递 (Trans-Intra)。

线程间规则包括：线程间授权分配(PowerPost-Inter)、线程间分配开始 (PostBegin-Inter)、线程间活动传递性(Trans-Inter)、Fork、Join、锁规则(Lock)。

回调方法规则包括：活动回调(activitycallback)、服务回调(servicecallback)。

Happens-Before关系集＝<E，R>，其中E是执行轨迹中的活动<e₁，e₂，…，e_n>， R＝{<e_j＜e_k|j，k∈[1，n]∧j≠k>}，e_j＜e_k表示活动对(e_j，e_k)符合安卓并发 语义且活动e_j先于活动e_k发生。

步骤3)中，使用预测性分析合理改变活动之间的调度来生成多个执行轨迹。

执行轨迹T＝<e₁，e₂，…，e_n>是活动的一次调度，由于多线程执行的不确定 性，每次执行的活动调度均不同。在单个执行轨迹中，某些活动必须遵循特定的 先后序关系，但有些读写活动间可改变调度方式，即：在满足不变的安卓并发语 义规则基础上，对可变活动操作重新排列，以获取新的活动调度，从而从单个执 行轨迹预测生成多个执行轨迹，由此可以探测更广泛的解空间。

步骤4)中，应用变量松弛以及路径松弛，以获得若干约束条件的表达。

在传统的预测性方法中，要求同一变量的读取值一定等于最近一次对该变量 写入的值，由于这一约束存在，隐含地对读“同一线程之后的活动”和写“同一 线程之前的活动”施加了约束，但实际上这样的约束条件过于严格，会导致结果 的漏报。我们放松了对这个变量读写的约束，称之为变量松弛。

在程序的一次执行中，若遇到分支情况，则只能执行其中一条分支。传统的 预测性分析方法要求原样执行，无法覆盖到其他分支中隐藏的缺陷。我们通过对 控制语句分支条件值取反来强制执行其他分支，称之为路径松弛。

完成上述操作后，获得多个预测性的执行轨迹，据此生成若干约束条件，如 下所示。

变量约束(ValueConstraints)：对变量具体的赋值进行约束；

控制约束(ControlConstraints)：对分支语句的控制条件进行约束；

序列约束(OrderConstraints)：对安卓并发语义进行约束；

数据竞争约束(RaceConstraints)：对可能发生数据竞争的活动进行约束；

线程间活动调度约束(Inter-threadActConstraints)：通过重新安排同一变量之 间的读写排列约束，可获得多种调度方式，从而预测生成多个执行轨迹。

步骤5)中，把所有约束放入约束求解器中进行求解，从而完成数据竞争的 检测。其中，约束求解器采用微软公司的Z3求解器，如果有解，则表明被测安 卓应用程序中存在数据竞争问题。

本发明通过采用以上技术方案，具有以下优点：

1.可扩展性好：本发明基于预测性分析方法，保留了动态分析方法的优点， 对于大规模应用程序来说，扩展性强。

2.没有误报：因为执行轨迹是通过实际运行得到的，并且是基于实际的单 个执行轨迹来进行预测分析的，因而可以避免误报。

3.准确率高：本发明使用了变量松弛和路径松弛等优化技术，减少了漏报， 提高了检测结果的精度。

附图说明

图1为本发明的流程图。

图2为被测安卓应用程序MusicPlayer的部分源码。

图3为MusicPlayer的部分运行轨迹。

具体实施方式

本发明方法首先基于安卓开发框架和其多线程模型，插桩安卓应用程序并动 态运行提取单个执行轨迹，再使用预测性分析方法对执行轨迹进行分析，构造其 活动间的发生序关系(Happens-Before)并预测生成多个执行轨迹，在此基础上 结合变量松弛和路径松弛对执行轨迹中的所有活动进行约束编码，最终放入约束 求解器中进行求解，从而完成数据竞争的检测。

本发明的流程如图1所示，具体包括如下五个步骤。

第一步：分析安卓开发框架，结合其特有的多线程模型，插桩原安卓应用程 序，动态运行获取安卓执行轨迹，执行轨迹T＝<e₁，e₂，…，e_n>是一个活动流， 对于源程序SourceAPK，我们认为其内的每一个语句都进行了不同的操作，称其 为活动。我们记录其中与并发相关、可能会导致数据竞争的活动，包括：线程的 初始化、开启一个线程等线程操作；共享变量的读写操作；锁集的申请释放操作； 与任务相关的授权、开始、结束任务等操作。

根据程序中每条活动具体的情况，我们归纳出我们所要记录的相关活动，并 在源程序中一一识别并记录。

定义1：记录的基本活动

1).threadinit(t)：当前线程初始化；

2).threadexit(t)：当前的线程执行完毕；

3).fork(t，s，t′)：在t线程中创建新的t′线程，s为线程的类型；

4).join(t，s，t′)：线程执行完毕，返回结果；

5).wait(t)：使当前线程阻塞等待；

6).notify(t)或notifyAll(t)：通知wait()线程可以继续执行；

7).beginTask(t，p)：在线程t中执行任务p；

8).endTask(t，p)：在线程t中结束执行任务p；

9).touchEvent(t，e)：线程t响应事件，包括如下事件：launch：发起app；home： home键使用；click：点击；Rotate：旋转；sliding：滑动；back：回退，每一个活动 的触发都会造成安卓组件生命周期的变化；

10).acq(t，1)：进程t申请锁I；

11).reI(t，I)：进程t释放锁I；

12).read(t，m)：进程t对m进行内存读取；

13).write(t，m，value)：进程t对m进行内存写入；

14).post(t，p，t′)：传递执行任务p给线程t′；

15).hasRunPower(t，p)：任务p有权利执行。

第二步：基于安卓的并发语义规则，构造活动间的Happens-Before关系集。

定义2：Happens-Before关系

Happens-Before最初是由LesileLamport引入的用来描述程序活动的一种偏 序关系。如果程序中AHBB，那么B就能看到A的操作(无论A和B是否是同 一个线程)。

这里我们将多线程的执行看作是活动E的轨迹，这里的活动是指JMM动作， 也即Java内存模型动作(JavaMemoryModelAction)。根据定义2和安卓的多线程 模型，我们可以得到定义3，安卓并发语义规则。

定义3：安卓的并发语义规则

(1)线程间Happens-Before关系(intra-thread)

i.线程内序列关系(Order-Intra)：如果活动e_i，e_i属于同一个线程t，并且 e_j控制依赖于e_i，则有e_i＜intrae_j；

ii.线程内授权分配(PowerPost-Intra)：如果活动e_i拥有执行某个任务的 权限即e_i＝hasRunPower(t，p)，活动e_j分配该任务(e_j＝Post(t，p，_))，且e_i， e_j属于同一个线程，则e_i＜intrae_j；

iii.线程内分配开始(PostBegin-Intra)：一个任务的分配在该任务开始之前 发生，即若e_i＝Post(t，p，t)，e_j＝beginTask(t，p)且e_i，e_j属于同一个线程， 则e_i＜intrae_i；

任务原子性(TaskAtomic-Intra)：若一个任务开始于另一个任务之前， 则该任务也会在另一个任务开始之前结束，即：若e_k＝beginTask(t，p1)， e_i＝endTask(t，p1)，e_j＝beginTask(t，p2)，e_k＜e_j，则e_i＜intrae_j；

iv.线程内传递关系(Trans-Intra)：如果e_i，e_k满足线程内Happens-Before 关系，且e_k，e_j满足线程内Happens-Before关系，则e_i，e_j满足线程内 Happens-Before关系。

(2)线程间Happens-Before关系(inter-thread)

i.线程间授权分配(PowerPost-Inter)：若活动e_i拥有执行某个任务的权 限，即e_i＝hasRunPower(t，p)，活动e_j分配该任务(e_j＝Post(t，_p，_))，且e_i， e_j不属于同一个线程，则e_i＜intere_j；

ii.线程间分配开始(PostBegin-Intra)：一个任务的分配在该任务开始之 前发生，即如果e_i＝Post(t，p，t)，e_j＝beginTask(t，p)且e_i，e_j不属于同 一个线程，则e_i＜intere_j；

iii.线程间传递关系Trans-Intra：如果e_i，e_k满足线程间Happens-Before 关系，且e_k，e_j满足线程间Happens-Before关系，则e_i，e_j满足线程 间Happens-Before关系；

iv.Fork：若活动e_i，e_j不属于同一个线程，且有e_i＝fork(t，t’)， e_j＝threadinit(t’)，则：e_i＜intere_j；

v.Join：若活动e_i，e_j不属于同一个线程，且有e_i＝threadexit(t’)，e_j＝join(t， t’)，则：e_i＜intere_j；

vi.锁(Lock)：若活动e_i，e_i不属于同一个线程且e_i＝release(t，1) e_j＝acquire(t’，1)，则：e_i＜intere_j。

(3)生命周期回调Happens-Before关系(callbackmethod)

Activity：

i.onCreate()＜cbonStart()＜cbonResume()；

ii.onResume()＜cbonPause()[＜cbonStop()]；

iii.onStop()＜cbonDestory()；

iv.onStop()＜cbonRestart()＜cbonStart()；

v.onPause()＜cbonResume()；

vi.onStop()＜cbonCreate()。

Service

i.onCreate()＜cbonStartCommand()＜cbonDestory()；

ii.onCreate()＜cbonBind()＜cbonUnbind()＜cbonDestory()。

根据定义1和定义3，我们分析执行轨迹并构造其内活动必须满足的不可改 变的Happens-Before关系集＜E，R＞。

定义4：<E，R>关系

表征安卓活动间的Happens-Before关系，其中E是执行轨迹中的活动 <e₁，e₂，…，e_n>，R＝{<e_j＜e_k|j，k∈[1，n]∧j≠k>}，e_j＜e_k表示活动对 (e_j，e_k)符合安卓并发语义且活动e_j先于活动e_k发生。

第三步：使用预测性分析方法合理改变活动之间的调度来生成多个执行轨迹。

执行轨迹T＝<e₁，e₂，…，e_n>是活动的一次调度，由于多线程执行的不确定 性，每次执行的活动调度均不同。在单个执行轨迹中，某些活动必须遵循特定的 先后序关系，但有些读写活动间可改变调度方式，即：在满足不变的安卓并发语 义规则基础上，对可变活动操作重新排列，以获取新的活动调度，从而从单个执 行轨迹预测生成多个执行轨迹，由此可以探测更广泛的解空间。

例如，对一个变量v，线程1对它先进行了读操作，再进行了写操作(记为 W1，R1)；线程2同样也对它进行了读操作和写操作(记为W2，R2)。在一次执行 中，我们可能对线程1和2之间的交互只获得一种调度方式(记为调度1：W1，W2， R1，R2)。然而由于多线程交互间的不确定性，还可能存在调度2：W1，W2，R2，R1； 调度3：W1，R1，W2，R2；调度4....等等。

预测性分析方法，就是基于不变的安卓并发语义规则，在一次执行所获得的 调度1的基础上，合理改变可变的活动间交互顺序，来预测生成多个执行轨迹。

第四步：依据安卓的并发语义规则(定义3)和Happens-Before关系集(定义4)， 应用变量松弛以及路径松弛对执行轨迹中的所有活动进行约束编码。

在传统的预测性方法中，要求对同一变量的读取值一定等于最近一次对该变 量写入的值，由于这一约束存在，隐含地对读“同一线程之后的活动”和写“同 一线程之前的活动”施加了约束，但实际上这样的约束条件过于严格，会导致结 果的漏报。变量松弛放松了对变量操作活动间的这类约束，提高了准确性。

用O_j，O_j代表活动e_i，e_j的出现次序，用符号执行技术来替换程序内变量的可 能取值。对一变量的一种调度R1，W1，R2，W2，若使用传统的预测性方法，则 W1，R2要满足线程间Happens-Before关系，又根据线程内Happens-Before规则： (R1，W1)、(R2，W2)和传递性规则，可以得到R1，W2活动之间存在Happens-Before 关系。但真实情况下由于多线程交互之间的不确定性，R1，W2之间可能会存在 数据竞争，原有方法就会造成漏报。在本发明中，我们通过变量松弛来提高检测 的准确性，具体实现是通过各种约束条件来保证。

在程序的一次执行中，若遇到分支情况，则只能执行其中一条分支。传统的 预测性分析方法要求原样执行，无法覆盖到其它分支中隐藏的缺陷。我们通过对 控制语句分支条件值取反来强制执行其它分支，称之为路径松弛。由于安卓应用 程序是事件驱动程序，不同的事件会造成不同的回调方法的执行，为了全方面探 测安卓应用源程序，我们也进行了路径松弛。

完成上述变量松弛和路径松弛后，可以得到多个预测性的执行轨迹，相应的 约束条件表示如下。

变量约束(ValueConstraints)：例如：代表在程序中的某个变量， 其中行号1表示位置，下标y表示程序中的变量名，W代表写操作，则该约束表 示：在程序的第一行，y变量被明确赋值为3。变量约束用于记录程序中变量被 明确赋值的操作活动。

控制约束(ControlConstraints)：例如：代表程序中的某个变量， 其中行号1表示位置，下标x表示变量名，R表示读操作，则该约束表示：在程 序的第一行，所读取的x变量的值要大于3。控制约束约束了程序的走向，说明 了程序运行时需要遵循的控制条件。

序列约束(OrderConstraints)：对安卓多线程程序中活动间次序关系的一种约 束。例如，2个活动e_j，e_j若符合在定义4中的先后序关系R，则用O_i＜O_j来表示。

数据竞争约束(RaceConstraints)：表现形式为O_i＝O_j，其中活动i，j分别属于2 个不同的线程，并且对同一变量进行操作(至少有一个写操作)，两个活动的序列 约束相等，就表示它们可以并发执行，符合数据竞争的定义。

线程间交互约束(Inter-threadConstraints)：例如：表示程序活动不同的调度情况，表示在第二行对变量x读取的值等于在第一行对该变量写入的值，并且相应的活 动O₁先于活动O₂发生，多个这样的约束之间用或操作链接。线程间交互约束是 对程序中可变活动调度的一种约束。

第五步：把所有约束放入约束求解器进行求解，从而完成数据竞争的检测。

约束求解器求解可行执行轨迹的过程为：将执行轨迹中所有的约束条件进行 编码后代入约束求解器中，得到可行解空间，解空间即为满足约束条件的所有可 行执行轨迹。编码过程即将条件表达式转换成求解器可识别的形式，不同求解器 需要的条件表达式形式略有不同。

本发明采用Z3求解器。Z3求解器是由微软研究院开发的一款统计模型理论 (SatisfiabilityModuloTheories)求解器，可以用来对数值型、布尔型表达式进行 约束求解。

下面结合一个实际案例MusicPlayer来做具体实施说明，本发明不仅限适用 于该例。

MusicPlayer是一个安卓应用程序，它的功能是从网站上下载音乐并且播放音 乐。图2展示了其代码片段，包括两个类：DwFileAct类和FileDwTask类。DwFileAct 继承了Activity，是一个Activity组件，提供了与用户交互的界面，其中onPlayClick 方法使用户可以点击Play按钮播放音乐。FileDwTask继承了AsyncTask类， AsyncTask提供了一种执行异步任务的框架，使FileDwTask可以在后台执行长时 间下载音乐的任务。

对该应用程序进行数据竞争检测的具体过程如下：

1.分析安卓开发框架，结合其特有的多线程模型，插桩原安卓应用程序， 动态运行获取安卓执行轨迹。

所要记录的活动有：threadinit(t)，threadexit(t)，fork(t，s，t′)，join(t，s，t′)，wait(t)、 notify(t)或notifyAll(t)，beginTask(t，p)，endTask(t，p)，touchEvent(t，e)，acq(t，I)，reI(t， I)，read(t，m)，write(t，m，value)，post(t，p，t′)，hasRuPower(t，p)，详细描述可参看定 义1。

图3展现了MusicPlayer的执行轨迹片段，图中有3个线程，线程t0表示系 统ActivityManagerService，用于管理安卓应用程序的组件；线程t1是主线程main， 即源代码中的DwFileAct；线程t2代表执行异步任务的工作线程，即源代码中的 FileDwTask类。在执行轨迹中，首先主线程初始化，之后活动执行 LAUNCH_ACTIVITY权限，经过线程t0的通知后，执行LAUNCH_ACTIVITY任务， 接着初始化对象，进行了写入操作，随后通过fork操作开启了异步线程执行相 关任务；异步线程在处理任务中读取了DwFileAct-obj，随后通知主线程执行 onPostExecute任务；主线程接到post后执行onPostExecute任务；在此期间，由 于执行LAUNCH_ACTIVITY，主线程已经拥有了执行onDestroy任务的权限，在随 后的任何时刻都可能执行onDestroy任务。

2.构造活动间的Happens-Before关系集。

安卓的并发语义规则如下：

1)线程内Happens-Before规则

线程内序列规则(Order-Intra)、线程内授权分配规则(PowerPost-Intra)、线 程内分配开始规则(PostBegin-Intra)、任务原子性规则(TaskAtomic-Intra)、线 程内传递关系规则(Trans-Intra)。

2)线程间Happens-Before规则

线程间权限分配规则(PowerPost-Inter)、线程间分配开始规则 (PostBegin-Inter)、线程间传递规则(Trans-Inter)、Fork、Join、锁规则(Lock)。

3)生命周期回调Happens-Before规则

活动规则(Activity)

服务规则(Service)

详细的描述可参看定义3。构造MusicPlayer的Happens-Before关系，简要记 录如下(直接用行号代表活动)。

i.Order-Intra：

1＜2＜4＜5＜6＜7＜8

9＜10＜11＜12

13＜14＜15＜16

18＜19＜20

ii.PowerPost-Inter

2＜3；7＜17

iii.PostBegin-Inter

3＜4；11＜13；17＜18

iv.Fork

6＜9

v.Activitycallback

4＜18

vi.TaskAtomic-Intra

8＜18

3.分析执行轨迹的Happens-Before关系集，使用预测性方法合理改变活动 之间的调度来生成多个执行轨迹。如图3，在这里我们可以看到第5行、第10 行、第14行、第19行对变量进行了获取操作，分别为应 用变量松弛，重新排列这些活动，生成新的调度方式，中间用“或”操作进行连 接。因此线程间交互约束如下：

4.应用变量松弛和路径松弛对图3执行轨迹中的所有活动进行约束编码

ValueConstraints：$W_{\mathrm{dw}}^5=\mathrm{false},W_{\mathrm{dw}}^{19}=\mathrm{true}.$

OrderConstraints：见第2步。

InterThreadConstraints：见第3步。

ControlConstraints：空。

RaceConstraints：5＝10，5＝14，10＝19，14＝19，5＝19。由于对共 享变量DwFileAct-obj进行写操作的活动集合为{5，19}，进行读操作集合为{10，14}， 根据数据竞争的定义，我们可以得到5个可能产生数据竞争的活动对：<5，10>、 <5，14>、<10，19>、<14，19>、<5，19>。

5.通过约束求解器求解约束编码，完成数据竞争的检测。

把第4步的所有约束放入z3求解器中进行求解，在14＝19和10＝19数据竞 争约束下，我们得到可行解，其它的数据竞争约束在解空间中无可行解。

分析：

1.由于<5，6>、<6，9>、<9，10>为Happens-Before关系，根据传递性可知<5，10> 也属于Happens-Before关系，所以<5，10>不会导致数据竞争。

2.由于<5，10>、<10，11<、<11，13>、<13，14>为Happens-Before关系，可知<5， 14>属于Happens-Before关系，所以<5，14>不会导致数据竞争。

3.由于<5，7>、<7，17>、<17，18>、<18，19>为Happens-Before关系，可知<5，19> 属于Happens-Before关系，所以<5，19>不会导致数据竞争。

综上可见，本发明方法通过单个执行轨迹，使用预测性分析得到多个执行轨 迹并进行分析，效率高。同时应用变量松弛和路径松弛对执行路径活动进行编码 约束，降低了误报率。从而本发明方法能够高效精确地检测到安卓应用程序中的 数据竞争错误。