Page 53 - 《软件学报》2021年第12期

张杨 等:基于下推自动机的细粒度锁自动重构方法 3717

4. else
5. lockfiled←new ReentrantReadWriteLock(⋅);
6. LockSet←〈m:lockfiled〉;
7. end if
8. str←getEffectAnalysis(c);
9. if c 为同步方法||c 为同步块 then
10. 移除 synchronized 相关锁;
11. Results←Pushdown(str);
12. 根据识别结果 Results 将 c 重构为 c_r;
13. end if
14. if Consistency(c,c_r) then
15. return c_r;
16. else
17. 使用写锁将 c 重构为 c_w;
18. return c_w;
19. end if
3 一致性检测

FlexSync [17] 是一个可以通过施加不同标记在不同同步机制之间进行重构转换的工具,FlexSync 中定义了
一致性检查规则,以此来检查在不同同步机制之间转换的一致性.为了尽可能地保证重构的正确性,本节参照
FlexSync 的一致性检测规则,给出了 FLock 重构前后的一致性检测规则.在给出规则之前,我们首先对相关的内
容进行了定义.
定义 7(临界区集合). 一个应用程序 P 中所有临界区的集合定义为 C={c 1 ,c 2 ,…,c n }.对于∀c i ∈C(1≤i≤n),
c i ={c i1 ,c i2 ,…,c ik }表示 c i 被划分为 k 个细粒度的临界区.
由于 P 中的代码是有限的,因此 C 是一个有限集合,对于∀c i ∈C(1≤i≤n),c i 表示某一个临界区.c i 中可以包
含若干读写操作 op i1 ,op i2 ,…,op ir ,表示为{op i1 ,op i2 ,…,op ir }⊆c i .
C before 和 C after 分别表示重构前和重构后的临界区集合,由于 FLock 在重构时需要分割临界区,因此|C before |<
|C after |,其中,|C|表示集合 C 元素个数.
定义 8(重构前锁集合). 一个应用程序 P 中所有用于保护临界区的锁集合定义为集合 S={s 1 ,s 2 ,…,s m }.
由于 C 是有限集合,所以 S 也是一个有限集合.由于一个锁可以保护多个临界区,故 m≤n.对于∀s e ∈S,s e 表示
既包含加锁操作又包含解锁操作.
定义 9(锁保护). 对于∀c i ∈C(1≤i≤n),∃s e ∈S(1≤e≤m),如果临界区 c i 处于锁 s e 的保护中,则定义保护关系
为 s e ⊙{c i }.进一步,一个锁可以保护多个临界区,定义为 s e ⊙C k ,其中,C k 是 C before 的子集,即 C k ⊆C before .
定义 10(重构后锁集合). 一个应用程序 P 中重构之后所有的锁集合定义为集合 L={l 1 ,l 2 ,…,l t }.对于∀l a ∈L
(1≤a≤t),l a ⊙C v ,C v 是 C after 的子集,即 C v ⊆C after .
定义 11(锁状态原子性保持). 对于∀l a ∈L,如果 l a 在没有释放锁的情况下完成锁状态切换,则说明锁状态原
子性没有被破坏,定义其为 l a ,否则定义为 l a .

定义 11 说明了锁状态的原子性问题,举例来说:读写锁在由写锁切换为读锁时,可以不用释放该锁,在该锁
的内部完成锁状态的切换.
定义 12(重构前后锁的对应关系). 重构前,对于∀c k ∈C(1≤k≤n),∃s e ∈S(1≤e≤m),s e ⊙C k ;重构后,对于
∀c v ∈C(1≤v≤n),∃l a ∈L(1≤a≤t),l a ⊙C v .如果 C v ⊆C k ,则 s e 和 l a 之间存在一一对应关系,记为 s e ≡l a .
定义 13(Happens-before 关系). 对于∀c i ∈C,{op i1 ,op i2 ,…,op ir }⊆c i ,∃u,v(1≤u≤r,1≤v≤r),如果 op iu 先发生于