Correctness of concurrent objects Lineariza bility (herlihy &Wing 90) O Slin S: correctness w.r.t. functionality Spec s: abstract object atomic methods Hard to understand/use Equivalent to contextual refinement (Filipovic et al. J -o Ctx s iff VC. clo] cc[s
Correctness of Concurrent Objects • Linearizability [Herlihy&Wing’90] – O lin S : correctness w.r.t. functionality – Spec S : abstract object (atomic methods) – Hard to understand/use • Equivalent to contextual refinement [Filipovic et al.] – O ctxt S iff C. C[O] C[S]
O Ctx s iff VC. clo]c cs Concrete void push(int v) obj. O Client C int popo t X y: pop( push(x);‖pint; push Abstract pop obi. S
… x := 7; push( x ); … … y := pop(); print(y); … Client C Concrete obj. O Abstract obj. S void push(int v) { … } int pop() { … } push pop O ctxt S iff C. C[O] C[S]
Concurrent Program Refinement Compilers for concurrent programs Linearizability of concurrent objects(libraries) Impl. of software transactional memory stm) Atomic block(transaction )> fine-grained impl
Concurrent Program Refinement • Compilers for concurrent programs • Linearizability of concurrent objects (libraries) • Impl. of software transactional memory (STM) – Atomic block (transaction) → fine-grained impl
Concurrent Program Refinement Compilers for concurrent programs Linearizability of concurrent objects(libraries) Impl. of software transactional memory stm) Impl of concurrent garbage collectors (Gc) Impl of operating system(OS) kernels Is such a refinement T c s general enough easy to verify?
Concurrent Program Refinement • Compilers for concurrent programs • Linearizability of concurrent objects (libraries) • Impl. of software transactional memory (STM) • Impl. of concurrent garbage collectors (GC) • Impl. of operating system (OS) kernels Is such a refinement T S general enough & easy to verify?
Problems withtcs T1 S1 T2 S2 (Compositionality) T1 T2 9 S1 $2 Existing work on verifying TCS: either is not compositional, or limIts applications
(Compositionality) T1 || T2 S1 || S2 T1 S1 T2 S2 Problems with T S Existing work on verifying T S : either is not compositional, or limits applications