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

3718 Journal of Software 软件学报 Vol.32, No.12, December 2021

op iv ,则定义 Happens-before 关系为 op iu ≥op iv .依据 Happens-before 关系的传递性,如果 op iu ≥op iv 并且 op iv ≥op iw ,
则 op iu ≥op iw .
Happens-before 关系的定义是建立在 Java 内存模型基础上的读写操作发生序关系,是 Java 语言内存一致性
的重要准则.该关系建立的方式之一是通过程序中的同步关系,解锁操作之前的操作先发生于解锁之后获取该
锁的操作.
基于如上的定义,下面给出了重构的一致性检测规则.
规则 1. 对于重构前,∀c i ∈C(1≤i≤n),∃s e ∈S(1≤e≤m),使得 s e ⊙ {c i };重构后,c i ={c i1 ,c i2 ,…,c ik },对于∀c ij (1≤
i≤n,1≤j≤k),∃l a ∈L(1≤a≤t),使得 l a ⊙ {c ij }.
规则 1 说明了重构之前处于锁保护的临界区,在重构之后仍处于锁的保护中.
规则 2. 对于重构前,∀c i ∈C(1≤i≤n),∃s e ∈S(1≤e≤m),使得 s e ⊙ {c i };重构后,c i ={c i1 ,c i2 ,…,c ik },对于∀c ij (1≤
i≤n,1≤j≤k),∃l a ∈L(1≤a≤t),如果有 l a ⊙ {c ij },则 s e ≡l a .
规则 2 说明:如果重构前临界区 c i 在 s e 的保护中,即使重构后 c i 被分割为多个临界区,保护这些临界区的锁
l a 和 s e 之间存在一一对应的关系.如果所有的锁都可以被重构,那么重构前后的锁集合应满足|S|=|L|.需要说明的
是:对于 FLock 重构前后锁的一一对应关系,通常表现在同步锁的监视器对象和读写锁对象的一一对应关系上.
规则 1 和规则 2 从重构前后代码结构上进行了一致性说明,保证了代码结构的完整性.
由于 FLock 在进行面向细粒度锁重构时主要采用了降级锁和锁分解两种方式,下面主要针对这两种方式
进行规则定义.
规则 3. 重构前,对于∀c i ∈C(1≤i≤n),∃s e ∈S(1≤e≤m),使得 s e ⊙ {c i };重构后,c i ={c i1 ,c i2 ,…,c ik },如果∃l a ∈L(1≤
a≤t),使得 s e ≡l a ,对于∀c ij (1≤i≤n,1≤j≤k),有(l a ⊙ {c ij })∧( l a )成立,则锁降级重构前后可以保证一致性.
规则 3 主要针对降级锁的重构进行了约束.虽然锁降级过程中会由写锁降级为读锁,但该过程是在锁的内
部进行转换的,期间并没有释放锁,可以保证锁的原子性,所以锁降级重构前后是一致的.
规则 4. 重构前,对于∀c i ∈C(1≤i≤n),∃s e ∈S(1≤e≤m),使得 s e ⊙ {c i };重构后,c i ={c i1 ,c i2 ,…,c ik },如果∃l a ∈L(1≤
a≤t),使得 s e ≡l a ,且对于∀c ij (1≤i≤n,1≤j≤k),有(l a ⊙ {c ij })∧( l a ).当{op i1 ,op i2 ,…,op ir }⊆c i 时,对于∀op ip ,op iq (1≤
p≤r,1≤q≤r),如果在 C before 中 op ip ≥op iq ,则在 C after 中仍有 op ip ≥op iq .
规则 5. 重构前,对于∀c i ∈C(1≤i≤n),{op i1 ,op i2 ,…,op ir }⊆c i ,∃s e ∈S(1≤e≤m),使得 s e ⊙ {c i };重构后,c i ={c i1 ,
c i2 ,…,c ik },如果∃l a ∈L(1≤a≤t),有 s e ≡l a ,且对于∀c ix ,c iy (1≤i≤n,1≤x≤k,1≤y≤k,x≠y),有(l a ⊙ {c ix ,c iy })∧( l a ).对于

∀op ip ,op iq (1≤p≤r,1≤q≤r),如果{op ip }⊆c ix ,{op iq }⊆c iy ,op ip 和 op iq 访问同一内存位置并且 op ip 或 op iq 是写操作,
则不能进行锁分解.
规则 4 和规则 5 共同保证了锁分解重构的一致性.规则 4 对锁分解的重构进行了约束,该规则通过检查临
界区读写语句的 Happens-before 关系,确保该关系在重构前后没有改变.在 FLock 工具的重构对象中,重构前后
代码都涉及同步关系,可以在同步关系的基础上建立 Happens-before 关系,进而进行规则判定.规则 5 从保持原
有临界区的原子性角度对锁分解进行了约束,确保原有临界区的原子性没有被破坏.如果存在 op ip 和 op iq 访问同
一内存位置,有可能因为线程交互而改变原有操作语义,在这种情况下,FLock 只推断一个写锁而不进行锁分解.

4 重构工具实现

FLock 是在 Eclipse JDT 框架下设计并以 Eclipse 插件的形式实现的,对 Eclipse 中的基础类 Refactoring 和
UserInputWizardPage 等进行扩展,实现相关的重构逻辑设计和可视化的重构工具界面设计.FLock 重构界面截
图如图 4 所示,展示了重构前后的代码之间的对比,其中,左侧为重构前的代码,右侧为重构后代码的预览.