234 H.Liang et al. TIW,S](T W,S'.(W,S)(W',S)v (W,S)abort} HIW,s]{get hist(T)I TE TIW,S]} OlW,S]get-obsv(T)I TE TIW,S]} Fig.5.Generation of Finite Event Traces states that the event e is either a silent client action,an output,or a client fault.We write is_inv(e)and is-ret(e)to denote that e is a method invocation and a return,respectively.The predicate is-abt(e)denotes a fault of the object or the client.Method invocations,returns and object faults are called history events,which will be used to define linearizability below.Outputs,client faults and object faults are called observable events. An event trace T is a finite or infinite sequence of events.We write T(i)for the i-th event of T.last(T)is the last event in a finite T.The trace T(1..i)is the sub-trace T(1),...,T(i)of T,and T is the length of T (IT]=w if T is infinite). The trace Tlt represents the sub-trace of T consisting of all events whose thread ID is t.We can use get-hist(T)to project T to the sub-trace consisting of all the history events,and get-obsv(T)for the sub-trace of all the observable events. Finite traces of history events are called histories. In Figure 5,we define TW,S]for the prefix-closed set of finite traces pro- duced by the executions of (W,S).We use (W,S)(W,S)for zero or multiple-step program transitions that generate the trace T.We also define HW,S]and OW,S]to get histories and finite observable traces produced by the executions of(W,S).The TR [14]contains more details about the language. Linearizability and Basic Contextual Refinement.We formulate lineariz- ability following its standard definition [11].Below we sketch the basic concepts. Detailed formal definitions can be found in the companion TR 14]. Linearizability is defined using histories.We say a return e2 matches an invo- cation e1,denoted as match(e1,e2),iff they have the same thread ID.An invo- cation is pending in T if no matching return follows it.We can use pend_inv(T) to get the set of pending invocations in T.We handle pending invocations in a history T in the standard way [11:we append zero or more return events to T,and drop the remaining pending invocations.The result is denoted by completions(T).It is a set of histories,and for each history in it,every invoca- tion has a matching return event. Definition 1 (Linearizable Histories).T Slin Tiff 1.Vt.Tt=Tt; 2.there erists a bijectionπ：{l,,lTl}→{1，，lT'}such that i.T()= T'(r()andi,j.i<jA is-ret(T(i)A is_inv(Ti)→π()<π(j) That is,T is linearizable w.r.t.T'if the latter is a permutation of the former, preserving the order of events in the same threads and the order of the non- overlapping method calls.Then an object is linearizable iff each of its concurrent histories after completions is linearizable w.r.t.some legal sequential history.234 H. Liang et al. T W, S def = {T | ∃W , S . (W, S) T −→∗ (W , S ) ∨ (W, S) T −→∗ abort} HW, S def = {get hist(T ) | T ∈ T W, S } OW, S def = {get obsv(T ) | T ∈ T W, S } Fig. 5. Generation of Finite Event Traces states that the event e is either a silent client action, an output, or a client fault. We write is inv(e) and is ret(e) to denote that e is a method invocation and a return, respectively. The predicate is abt(e) denotes a fault of the object or the client. Method invocations, returns and object faults are called history events, which will be used to define linearizability below. Outputs, client faults and object faults are called observable events. An event trace T is a finite or infinite sequence of events. We write T (i) for the i-th event of T . last(T ) is the last event in a finite T . The trace T (1..i) is the sub-trace T (1),...,T (i) of T , and |T | is the length of T (|T | = ω if T is infinite). The trace T |t represents the sub-trace of T consisting of all events whose thread ID is t. We can use get hist(T ) to project T to the sub-trace consisting of all the history events, and get obsv(T ) for the sub-trace of all the observable events. Finite traces of history events are called histories. In Figure 5, we define T W, S for the prefix-closed set of finite traces pro￾duced by the executions of (W, S). We use (W, S) T −→ ∗ (W , S ) for zero or multiple-step program transitions that generate the trace T . We also define HW, S and OW, S to get histories and finite observable traces produced by the executions of (W, S). The TR [14] contains more details about the language. Linearizability and Basic Contextual Refinement. We formulate lineariz￾ability following its standard definition [11]. Below we sketch the basic concepts. Detailed formal definitions can be found in the companion TR [14]. Linearizability is defined using histories. We say a return e2 matches an invo￾cation e1, denoted as match(e1, e2), iff they have the same thread ID. An invo￾cation is pending in T if no matching return follows it. We can use pend inv(T ) to get the set of pending invocations in T . We handle pending invocations in a history T in the standard way [11]: we append zero or more return events to T , and drop the remaining pending invocations. The result is denoted by completions(T ). It is a set of histories, and for each history in it, every invoca￾tion has a matching return event. Definition 1 (Linearizable Histories). T lin T iff 1. ∀t. T |t = T |t; 2. there exists a bijection π : {1,..., |T |} → {1,..., |T |} such that ∀i. T (i) = T (π(i)) and ∀i, j. i < j ∧ is ret(T (i)) ∧ is inv(T (j)) =⇒ π(i) < π(j). That is, T is linearizable w.r.t. T if the latter is a permutation of the former, preserving the order of events in the same threads and the order of the non￾overlapping method calls. Then an object is linearizable iff each of its concurrent histories after completions is linearizable w.r.t. some legal sequential history.