
Concurrent Program Refinement and Verification Overview
Explore the world of refining and verifying concurrent programs and their applications, covering topics such as refinement techniques, compilers, linearizability, and more.
Download Presentation

Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
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