Concurrent Program Refinement and Verification Overview

Refinement Verification of Concurrent Programs and Its Applications Hongjin Liang Univ. of Science and Technology of China Advisors: Xinyu Feng and Zhong Shao

Refinement void main() { print a square; } void main() { print a rectangle; } T S: T has no more observable behaviors (e.g. I/O events by print) than S.

Concurrent Program Refinement Compilers for concurrent programs Multithreaded Java programs S Correct(Compiler): S, T. T = Compiler(S) Compiler T S Java bytecode T

Concurrent Program Refinement Compilers for concurrent programs Fine-grained impl. of concurrent objects (libraries) E.g. java.util.concurrent

Concurrent object O Client code C push(7); x = pop(); push(6); void push(int v) { local b:=false, x, t; x := new Node(v); while (!b) { t := top; x.next = t; b = cas(&top, t, x); } } int pop() { } Whole program C[O] How to specify/prove correctness?

Correctness of Concurrent Objects Linearizability [Herlihy&Wing 90] O linS : correctness w.r.t. functionality Spec S : abstract object (atomic methods) Hard to understand/use Equivalent to contextual refinement [Filipovic et al.] O ctxtS C. C[O] C[S] iff

O ctxtS C. C[O] C[S] iff Concrete obj. O void push(int v) { } int pop() { } Client C x := 7; push( x ); y := pop(); print(y); push Abstract obj. S pop

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 S general enough & easy to verify?

Problems with T S T1 S1 T2 S2 (Compositionality) T1 || T2 S1 || S2 Existing work on verifying T S : either is not compositional, or limits applications.

Long-Standing Problems in Verifying Linearizability Objects with Non-Fixed Linearization Points (LPs) Future-dependent LPs (e.g. lazy set, pair snapshot) Helping (e.g. HSY elimination-backoff stack) Most existing work : either not supports them, or lacks formal soundness.

Refinement vs. Progress Properties ? Linearizability Correctness w.r.t. functionality Not talk about termination/liveness properties Progress properties Lock-freedom (LF) Wait-freedom (WF) Obstruction-freedom (OF) Deadlock-freedom (DF) Starvation-freedom (SF) Non-blocking impl. Lock-based impl.

Our Contributions (Part 1) RGSim = Rely/Guarantee + Simulation Compositional w.r.t. parallel composition Flexible & applicable optimizations in concurrent contexts concurrent GC fine-grained concurrent obj.

Our Contributions (Part 2) RGSim = Rely/Guarantee + Simulation A program logic for linearizability Support non-fixed LPs Verified 12 well-known algorithms (some are used in java.util.concurrent) Light instrumentation mechanism to help verification Formal meta-theory: simulation (extends RGSim) Establish a contextual refinement

Our Contributions (Part 3) RGSim = Rely/Guarantee + Simulation A program logic for linearizability A framework to characterize progress properties via contextual refinement (CR) Propose different termination-sensitive CR Equivalent to linearizability + progress Unify all five progress properties (LF, WF, OF, DF, SF) Make modular verification of whole program C[O] easier Potential to have a generic verification framework for linearizability + progress

Outline Rely-Guarantee-based simulation for modular verification of concurrent refinement Logic for linearizability Progress properties and contextual refinement

Modular Verification of T S T1 S1 T2 S2 (Compositionality) T1 || T2 S1 || S2

T1 S1 T1 || T2 S1 || S2 T2 S2 is NOT compositional w.r.t. parallel composition: T: S: local t; x++; t = x; print( x ); x = t + 1; print( x ); We have T S, since output(T) output(S) ; but we do not have T||T S||S .

Existing Proof Methods: Simulation in CompCert [Leroy et al.] Source state e* * (S, ) (S , ) (S , ) observable event (e.g. I/O) Target state e (T, ) (T , ) (T , )

Simulation in CompCert [Leroy et al.] Can verify refinement of sequential programs NOT compositional w.r.t. parallel composition T: S: local t; x++; t = x; print( x ); x = t + 1; We have T S , but not T||T S||S print( x );

Simulation in CompCert [Leroy et al.] Can verify refinement of sequential programs NOT compositional w.r.t. parallel composition Consider NO environments Simulation in process calculus (e.g. CCS [Milner et al.]) Assume arbitrary environments Compositional Too strong: limited applications

Assuming Arbitrary Environments e * *(S , ) (S, ) (S , ) env (S , ) e (T, ) (T , ) env (T , ) (T , ) Too strong to be satisfied, since env. can be arbitrarily bad. Refinement applications have assumptions about S & env.

Refinements Assumptions Compilers for concurrent programs Prog. with data races has no semantics (e.g. concurrent C++) Not guarantee correctness for racy programs [Boehm et al. PLDI 08] Fine-grained objects Accesses use same primitives (e.g. stack: push & pop) Not guarantee correctness when env. can destroy obj. More examples are in the thesis Env. of a thread cannot be arbitrarily bad !

Problems of existing simulations : Considers no env. in CompCert [Leroy et al.] NOT compositional w.r.t. parallel composition Assumes arbitrary env. in process calculus (e.g. [Milner et al.]) Too strong: limited applications Our RGSim : Parameterized with the interference with env. Compositional More applications Use rely/guarantee to specify the interference

Overview of Rely/Guarantee [Jones'83] r: acceptable environment transitions g: state transitions made by the thread Thread1 Thread2 x = x y = y r1: r2: Nobody else would update y y = y Nobody else would update x g1: x = x g2: I guarantee I would not touch x I guarantee I would not touch y Compatibility (Interference Constraints): g2 r1 and g1 r2

RGSim = Rely/Guarantee + Simulation e* G * * (S, ) (S , ) (S , ) (S , ) G R e (T, ) (T , ) (T , ) (T , ) g r g (T, r, g) (S, R, G)

Soundness Theorem If we can find r, g, R and G such that (T, r, g) (S, R, G) T S then we have:

Parallel Compositionality (T1, r1, g1) (S1, R1, G1) (T2, r2, g2) (S2, R2, G2) g1 r2 g2 r1 G1 R2 G2 R1 (PAR) (T1||T2, r1 r2, g1 g2) (S1||S2, R1 R2, G1 G2)

More on Compositionality (T1, r, g) (S1, R, G) (T2, r, g) (S2, R, G) (T1; T2, r, g) (S1; S2, R, G) (T, r, g) (S, R, G) b B (while b do T, r, g) (while B do S, R, G) An axiomatic proof system for refinement

We have applied RGSim to verify Optimizations in parallel contexts Loop invariant hoisting, strength reduction and induction variable elimination, dead code elimination, Fine-grained impl. & concurrent objects Lock-coupling list, counters, Treiber s non-blocking stack, concurrent GCD algorithm, Concurrent garbage collectors A general GC verification framework Hans Boehm s concurrent GC [Boehm et al. 91]

Outline Rely-Guarantee-based simulation for modular verification of concurrent refinement Logic for linearizability Progress properties and contextual refinement

Linearizability of Concurrent Objects [Herlihy&Wing 90] Correctness w.r.t. functionality O linS : Every concurrent execution of object O is equivalent to some sequential execution of spec S

Linearizability of Object O A concurrent execution of O: push(7) ret pop() ret (7) Thread 1: push(6) ret Linearization point (LP) Thread 2: Sequential execution of S time push(6), ret, push(7), ret, pop(), ret(7)

Example: Treibers Non-Blocking Stack [Treiber 86] Top v1 next next vk t Is it linearizable? v next x 4 while(!b){ push(int v): 5 t := Top; 1 local b:=false, x, t; 6 x.next := t; 2 x := new Node(); 7 b := cas(&Top, t, x); 3 x.data := v; 8 }

lin ? Treiber s stack O Abstract stack S Top next next Stk = v1 :: v2 :: :: vk v1 vk push(v): PUSH(v): Stk := v::Stk; 1 local b:=false, x, t; 2 x := new Node(v); Not update the shared list 3 while (!b) { Fixed : statically located in impl code 4 t := top; 5 x.next = t; Line 6: the only command that changes the list LP 6 b = cas(&top, t, x); 7 }

lin ? Treiber s stack O Abstract stack S Top next next Stk = v :: v1 :: v2 :: :: vk v1 vk v Abstract opr PUSH(v) not done Proved it s LP LP 6 b := cas(&Top, t, x); < push(v): if (b) - { [PUSH(v)] } opr simultaneously Execute abstract 1 local b:=false, x, t; Atomic block 2 x := new Node(v); linself; - { [ ] } 3 while (!b) { > 4 t := Top; Abstract opr is done 7 } 5 x.next := t;

Basic Approach to Verify O linS Inspired by [Vafeiadis Thesis] Instrument(O) = D with linself at LPs Verify D in program logic with rules for linself New assertions [S] and [ ] Ensure O s LP step corresp. to S s single step Not support non-fixed LPs Future-dependent LPs Helping

Challenge 1: Future-Dependent LP Example: Pair Snapshot [Qadeer et al. MSR-TR-2009-142] t2: write(i, d) t1: readPair(i, j) m 0 1 k write(i, d) updates m[i] to a new value d readPair(i, j) intends to return snapshot of m[i] and m[j]

Pair Snapshot [Qadeer et al. MSR-TR-2009-142] readPair(int i, j){ 1 local s:=false, a, b, v, w; 2 while (!s) { 3 <a := m[i].d; v := m[i].v>; 4 <b := m[j].d; w := m[j].v>; 5 <if (v = m[i].v) s := true>; 6 } 7 return (a, b); } write(int i, d){ 8 <m[i].d := d; m[i].v++>; } LP if line 5 succeeds m 0 1 k Future-dependent LP Not supported by linself d know: m[i] = (a,v) at line 4 v version number Where is the LP ? Line 4? But line 5 may fail, m[i] and m[j] may be re-read

Solution: Try-Commit readPair(int i, j){ 1 local s:=false, a, b, v, w; 2 while (!s) { 3 <a := m[i].d; v := m[i].v;> - { m[i] = (a, v) [RP, (i,j)] } speculate at potential LP, keep both result and original [RP, (i,j)] 4 <b := m[j].d; w := m[j].v; - { m[i] = (a, v) ( [ , (a,b)] ) } >trylinself; } > commit( [ , (a,b)] ); 5 <if (v = m[i].v) { s:= true; - { s [ , (a,b)] s } 6 } 7 return (a, b); }

Challenge 2: Helping Example: elimination-backoff stack [Hendler et al. SPAA 04] t1 finishes t2 s opr t2 s LP is in the code of t1 Need to linearize a thread other than self New auxiliary command: lin(t) New assertions: t S | t Details are in the thesis

Our Approach to Verify O linS Instrument(O) = D with auxiliary cmds at LPs linself for fixed LPs try-commit for future-dependent LPs lin(t) for helping Assertions to describe abstract code & states p, q ::= | t S | t | p q | p q Verify D in our program logic Extend an existing logic with rules for aux cmds

Our Logic for O linS {p} S {q} {p (cid S)} trylinself {( p * (cid S) ) ( q * (cid ) )} {p q} commit(p) {p} {p} S {q} {p (t S)} lin(t) {q * (t )} More rules and soundness are in the thesis

Verified Algorithms Java Pkg (JUC) Objects Fut. LP Helping Treiber stack HSY stack MS two-lock queue MS lock-free queue DGLM queue Lock-coupling list Optimistic list Heller et al lazy list Harris-Michael lock-free list Pair snapshot CCAS RDCSS

Soundness via Contextual Refinement Theorem (equivalence): O linS O ctxtS Proof follows [Filipovic et al., 2009] Extensional Intentional : all proof methods for ctxtcan verify lin ctxtis a well-studied concept in PL community (still challenging though) : modular verification (view C[O] as C[S]) C[S] is simpler to understand/verify

Outline Rely-Guarantee-based simulation for modular verification of concurrent refinement Logic for linearizability Progress properties and contextual refinement

Progress Properties Describe whether methods eventually return Defined similarly to linearizablity Describe objects behaviors instead of clients Intentional instead of extensional E.g. there always exists a method call that ll return Can we use contextual refinement to define progress properties?

Our Results Linearizability O linS Progress P(O) Termination-sensitive contextual refinement O P S ( iff C. ObsBeh(C[O]) ObsBeh(C[S])) P LF div WF t-div OF i-div DF f-div SF ObsBeh(C[O]) f-t-div ObsBeh(C[S]) div t-div div div t-div

Relationships between Progress Properties WF Wait- freedom LF SF Lock- freedom Starvation- freedom equiv. to OF DF Obstruction- freedom Deadlock- freedom + Linearizability

Conclusion RGSim = Rely/Guarantee + Simulation Idea: parameterized with interference with env. Compositional! Applications: optimizations, concurrent GC, Program logic for linearizability Light instrumentation to help verification linself for fixed LPs lin(t) for helping try-commit for future-dependent LPs Verified 12 well-known algorithms