ms list(Z,A) 兰(ms=中Ax=null AA=e）V(仔mg3u.3y.3A'.ms=m出{x(-u,)}AA=v:A'Amg卡list(,A) shared_map(ms,Ms)m.A.3r.ms =m Head~xA (m list(x,MIN_VAL::A::MAX_VAL))A sorted(A)A (elems(A)=Ms(S)) local_map(m,Mi)mi(e)=Mi(e)A 3mi.mi myu} a 兰{(r,ms),(L,Ms)|shared_map(ms,Ms)At∈dom().local_map(π(t),Π(t)} Shock(t) 兰{(r,ms,(m,mg)》|3c,u,.ms(x)=(0,u,)∧mg=ms{r一(t,,)} Gunlock(t) {((,ms),(n.ms))|3,v.y.ms(2)=(t.v,y)Ams ms{(0vy))} Cadd(t) e{(rw{tmu,ms),(π出{tm},ms》 3r,y,z,u,v,w.ms(x)=(t,u,2)八ms(z)=(-+,-) A m's=msi(t;u,y)}y(0,v,2))A(miiy(0,v,2))=m)Au<v<w Cmv(t) 兰{(r出{tm},ms),(π出{tm},ms) 3x,,z,u,.ms(x)=(t,u,yAms()=(化，u,) A msy(t,v,z)}=msx(t,u,z)}A m=miy(t,v,2)}Av<MAX_VAL} Cocal(t) 兰{(rw{tmu},ms),(r世{tm},ms)lr∈(ThrdID→Mem)Aml,mi,ms∈LMem g(t) Glock(t)UGulock(t)UGadd(t)UGrmv(t)UGhocal(t) R()兰U9(t) Gadd(t) ≌{(Iw{tMh,Ms),(I世{tM,Mg)|3e.Mg=M{s∽Ms(s)U{e} Grmv(t) {((tM),M),(nIM),M))e.M=M{sM.(s)-{e))} Glocal(t) {({t∽M},Ms),(I{tM},Ms)|∈(ThrdID→HMem)AM,M,Ms∈HMem} G(t) Gada(t)UGrmv(t)UGlocal(t) R(e≌UG(t) Figure 9.Useful Definitions for the Lock-Coupling List A in Figure 8,which are the same as the corresponding guarantees We give the detailed proofs in the technical report [201.which are in Figure 9,as we will explain below. done operationally based on the definition of RGSim. In Figure 8.the abstract set is implemented by an ordered By the compositionality and the soundness of RGSim,we know singly-linked list pointed to by a shared variable Head,with two that the fine-grained operations (under the parallel environment R) sentinel nodes at the two ends of the list containing the values are simulated by the corresponding atomic operations (under the MIN_VAL and MAX_VAL respectively.Each list node is associated high-level environment R),while R and R say all accesses to the with a lock.Traversing the list uses "hand-over-hand"locking: set must be done through the add and remove operations.This gives the lock on one node is not released until its successor is locked. us the atomicity of the concurrent implementation of the set object. add(e)inserts a new node with value e in the appropriate position while holding the lock of its predecessor.rmv(e)redirects the More examples.In the technical report[201,we also show the use predecessor's pointer while both the node to be removed and its of RGSim to prove the atomicity of other fine-grained algorithms predecessor are locked. including the non-blocking concurrent counter [27],Treiber's stack algorithm[26],and a concurrent GCD algorithm (calculating great- We define the a relation,the guarantees and the relies in Fig- est common divisors). ure 9.The predicate ms list(,A)represents a singly-linked list in the shared memory ms at the location whose values form 7. the sequence A.Then the mapping shared_map between the low- Verifying Concurrent Garbage Collectors level and the high-level shared memory is defined by only concern In this section,we explain in detail how to reduce the problem of ing about the value sequence on the list:the concrete list should verifying concurrent garbage collectors to transformation verifica- be sorted and its elements constitute the abstract set.For a thread tion,and use RGSim to develop a general GC verification frame- t's local memory of the two levels,we require that the values of work.We apply the framework to prove the correctness of the e are the same and enough local space is provided for add(e) Boehm et al.concurrent GC algorithm [7] and rmv(e).as defined in the mapping local_map.Then a relates the shared memory by shared_map and the local memory of each 7.1 Correctness of Concurrent GCs thread t by local_map A concurrent GC is executed by a dedicate thread and performs The atomic actions of the algorithm are specified by Soek. the collection work in parallel with user threads(mutators),which Guloek.Gadd.G and Socal respectively,which are all parame- access the shared heap via read,write and allocation operations.To terized with a thread identifier t.For example.(t)says that ensure that the GC and the mutators share a coherent view of the when holding the locks of the node y and its predecessor r,we can heap,the heap operations from mutators may be instrumented with transfer the node y from the shared memory to the thread's local extra operations,which provide an interaction mechanism to allow memory.This corresponds to the action performed by the code of arbitrary mutators to cooperate with the GC.These instrumented line 13 in rmv(e).Every thread t is executed in the environment heap operations are called barriers (e.g.,read barriers,write barriers that any other thread t'can only perform those five actions.as de- and allocation barriers). fined in R(t).Similarly,the high-level G(t)and R(t)are defined The GC thread and the barriers constitute a concurrent garbage according to the abstract ADD(e)and RMV(e).The relies and guar- collecting system,which provides a higher-level user-friendly pro- antees are almost the same as those in the proofs in RGSep [28]. gramming model for garbage-collected languages (e.g.,Java).In We can prove that for any thread t,the following hold: this high-level model,programmers feel they access the heap using regular memory operations,and are freed from manually disposing (t.add(e),R(t),G(t))a:axa (t.ADD(e),R(t),G(t)); objects that are no longer in use.They do not need to consider the (t.rmv(e),R(t),G(t))a:axa (t.RMV(e),R(t),G(t)) implementation details of the GC and the existence of barriers. 464ms |= list(x, A) (ms = φ ∧ x = null ∧ A = ) ∨ (∃m s.∃v.∃y.∃A . ms = m s  {x ( , v, y)} ∧ A = v ::A ∧ m s |= list(y, A )) shared map(ms, Ms) ∃m s.∃A.∃x. ms = m s  {Head x} ∧ (m s |= list(x, MIN VAL::A::MAX VAL)) ∧ sorted(A) ∧ (elems(A)=Ms(S)) local map(ml, Ml) ml(e) = Ml(e) ∧ ∃m l. ml = m l  {x , y , z , u , v } α {((π,ms), (Π, Ms)) | shared map(ms, Ms) ∧ ∀t ∈ dom(Π). local map(π(t), Π(t))} Glock(t) {((π,ms), (π,m s)) | ∃x, v, y. ms(x) = (0, v, y) ∧ m s = ms{x (t, v, y)}} Gunlock(t) {((π,ms), (π,m s)) | ∃x, v, y. ms(x)=(t, v, y) ∧ m s = ms{x (0, v, y)}} Gadd(t) {((π  {t ml}, ms), (π  {t m l}, m s)) | ∃x, y, z, u, v, w. ms(x)=(t, u, z) ∧ ms(z)=( , w, ) ∧ m s = ms{x (t, u, y)}{y (0, v, z)} ∧ (m l  {y (0, v, z)} = ml) ∧ u<v<w} Grmv(t) {((π  {t ml}, ms), (π  {t m l}, m s)) | ∃x, y, z, u, v. ms(x)=(t, u, y) ∧ ms(y)=(t, v, z) ∧ m s  {y (t, v, z)} = ms{x (t, u, z)} ∧ m l = ml  {y (t, v, z)} ∧ v < MAX VAL} Glocal(t) {((π  {t ml}, ms), (π  {t m l}, ms)) | π ∈ (ThrdID → LMem) ∧ ml, m l, ms ∈ LMem} G(t) Glock(t) ∪ Gunlock(t) ∪ Gadd(t) ∪ Grmv(t) ∪ Glocal(t) R(t) t=t G(t ) Gadd(t) {((Π  {t Ml}, Ms), (Π  {t M l }, M s)) | ∃e. M s = Ms{S Ms(S)∪{e}}} Grmv(t) {((Π  {t Ml}, Ms), (Π  {t M l }, M s)) | ∃e. M s = Ms{S Ms(S)−{e}}} Glocal(t) {((Π  {t Ml}, Ms), (Π  {t M l }, Ms)) | Π ∈ (ThrdID → HMem) ∧ Ml, M l , Ms ∈ HMem} G(t) Gadd(t) ∪ Grmv(t) ∪ Glocal(t) R(t) t=t G(t ) Figure 9. Useful Definitions for the Lock-Coupling List A in Figure 8, which are the same as the corresponding guarantees in Figure 9, as we will explain below. In Figure 8, the abstract set is implemented by an ordered singly-linked list pointed to by a shared variable Head, with two sentinel nodes at the two ends of the list containing the values MIN VAL and MAX VAL respectively. Each list node is associated with a lock. Traversing the list uses “hand-over-hand” locking: the lock on one node is not released until its successor is locked. add(e) inserts a new node with value e in the appropriate position while holding the lock of its predecessor. rmv(e) redirects the predecessor’s pointer while both the node to be removed and its predecessor are locked. We define the α relation, the guarantees and the relies in Fig￾ure 9. The predicate ms |= list(x, A) represents a singly-linked list in the shared memory ms at the location x, whose values form the sequence A. Then the mapping shared map between the low￾level and the high-level shared memory is defined by only concern￾ing about the value sequence on the list: the concrete list should be sorted and its elements constitute the abstract set. For a thread t’s local memory of the two levels, we require that the values of e are the same and enough local space is provided for add(e) and rmv(e), as defined in the mapping local map. Then α relates the shared memory by shared map and the local memory of each thread t by local map. The atomic actions of the algorithm are specified by Glock, Gunlock, Gadd, Grmv and Glocal respectively, which are all parame￾terized with a thread identifier t. For example, Grmv(t) says that when holding the locks of the node y and its predecessor x, we can transfer the node y from the shared memory to the thread’s local memory. This corresponds to the action performed by the code of line 13 in rmv(e). Every thread t is executed in the environment that any other thread t can only perform those five actions, as de- fined in R(t). Similarly, the high-level G(t) and R(t) are defined according to the abstract ADD(e) and RMV(e). The relies and guar￾antees are almost the same as those in the proofs in RGSep [28]. We can prove that for any thread t, the following hold: (t.add(e), R(t), G(t)) α;αα (t.ADD(e), R(t), G(t)) ; (t.rmv(e), R(t), G(t)) α;αα (t.RMV(e), R(t), G(t)). We give the detailed proofs in the technical report [20], which are done operationally based on the definition of RGSim. By the compositionality and the soundness of RGSim, we know that the fine-grained operations (under the parallel environment R) are simulated by the corresponding atomic operations (under the high-level environment R), while R and R say all accesses to the set must be done through the add and remove operations. This gives us the atomicity of the concurrent implementation of the set object. More examples. In the technical report [20], we also show the use of RGSim to prove the atomicity of other fine-grained algorithms, including the non-blocking concurrent counter [27], Treiber’s stack algorithm [26], and a concurrent GCD algorithm (calculating great￾est common divisors). 7. Verifying Concurrent Garbage Collectors In this section, we explain in detail how to reduce the problem of verifying concurrent garbage collectors to transformation verifica￾tion, and use RGSim to develop a general GC verification frame￾work. We apply the framework to prove the correctness of the Boehm et al. concurrent GC algorithm [7]. 7.1 Correctness of Concurrent GCs A concurrent GC is executed by a dedicate thread and performs the collection work in parallel with user threads (mutators), which access the shared heap via read, write and allocation operations. To ensure that the GC and the mutators share a coherent view of the heap, the heap operations from mutators may be instrumented with extra operations, which provide an interaction mechanism to allow arbitrary mutators to cooperate with the GC. These instrumented heap operations are called barriers (e.g., read barriers, write barriers and allocation barriers). The GC thread and the barriers constitute a concurrent garbage collecting system, which provides a higher-level user-friendly pro￾gramming model for garbage-collected languages (e.g., Java). In this high-level model, programmers feel they access the heap using regular memory operations, and are freed from manually disposing objects that are no longer in use. They do not need to consider the implementation details of the GC and the existence of barriers. 464