Compositional Verification of Termination-Preserving Refinement in Concurrent Programs
This research explores the compositional verification of termination-preserving refinement in concurrent programs, focusing on correctness, optimizations, and the application of new simulation as meta-theory. Contributions include a rely-guarantee-based program logic and the verification of linearizability and lock-freedom. Examples and implications for compilers, program optimizations, and concurrent objects are discussed.
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
Compositional Verification of Termination-Preserving Refinement of Concurrent Programs Hongjin Liang Univ. of Science and Technology of China (USTC) Joint work with Xinyu Feng (USTC) and Zhong Shao (Yale)
Applications of Refinement of Concurrent Programs Correctness of program transformations Compilers, program optimizations, Multithreaded Java programs S Refinement T S : T has no more observable behaviors Compiler than S T Java bytecode
Applications of Refinement of Concurrent Programs Correctness of program transformations Compilers, program optimizations, Correctness of concurrent objects & libraries
Example Counter Impl. in concurrent setting Atomic spec. inc(){ local done, tmp; done = false; while (!done) { tmp = cnt; done = cas(cnt, tmp, tmp+1); } } atomic block INC(){ <CNT++> } Correctness: impl refines atomic spec in any context e.g. inc || while(true) inc INC || while(true) INC
Applications of Refinement of Concurrent Programs Correctness of program transformations Compilers, program optimizations, Correctness of concurrent objects & libraries Correctness of runtime systems & OS kernels Concurrent garbage collectors, STM algorithms,
Refinement needs to preserve termination! while (true) skip skip Compilers of concurrent programs Need to preserve termination Concurrent objects & libraries Must satisfy functionality correctness (e.g. linearizability) & termination properties (e.g. lock-freedom) No existing logics can verify such a refinement T S !
Our Contributions Rely-Guarantee-based program logic For termination-preserving refinement Compositional verification Applied to verify Linearizability + lock-freedom Correctness of optimizations of concurrent prog. New simulation as meta-theory
Termination-Preserving Refinement T S : More Examples while (true) skip skip while (true) skip; print(1); print(1); while (true) skip; cannot print out 1 always print out 1 We should avoid T looping infinitely without progress complete some abstract tasks of S
Verifying T S : How to avoid T looping infinitely without progress Assign tokens for loops Consume a token for each iteration One token to pay for one iteration local i = 0; while (i < 2) i++; print(1); print(1); i = 0 i = 1 i = 2
Verifying T S : How to avoid T looping infinitely without progress Assign tokens for loops Consume a token for each iteration local i = 0; while (true) i++; print(1); print(1); Never enough tokens!
How to compositionally verify T S in concurrent settings (Compositionality) T1 S1 S2 T2 T1 || T2 S1 || S2 In particular, termination-preservation of individual threads is not compositional
Challenge : termination-preservation of individual threads is not compositional || S1 || S2: print(1); print(1); T1 || T2 : while (i==0) { i--; } print(1); while (i==0) { i++; } print(1); || Both T1 & T2 terminate, but T1 || T2 may not terminate
Challenge : termination-preservation of individual threads is not compositional Consider NO environment To compositionally verify T S in concurrent settings, Need to take env interference into account! How will env affect termination-preservation? Which effects are acceptable? How to change tokens for acceptable env effects? Env may delay progress of the current thread. Is it always bad?
Env delays progress of current thread Sometimes acceptable INC(){ <CNT++> } inc(){ 1 local done, tmp; 2 done = false; 3 while (!done) { 4 tmp = cnt; 5 done = cas(cnt, tmp, tmp+1); 6 } } May never progress (complete abstract task INC) since its cas fails infinitely often Take a snapshot Compare and swap || while(true) inc;
Env delays progress of current thread Sometimes acceptable Because: The failure of one thread must be caused by the success of another. The system as a whole progresses. INC(){ <CNT++> } inc(){ 1 local done, tmp; 2 done = false; 3 while (!done) { 4 tmp = cnt; 5 done = cas(cnt, tmp, tmp+1); 6 } } Should allow current thread to loop more (i.e. reset tokens) if env progresses || while(true) inc;
Our Ideas Prove termination-preservation of individual threads under env interference Assign tokens for loops Consume a token for each iteration Avoid looping infinitely without progress Could reset tokens when env progresses The system as a whole progresses. So the current thread can loop more.
How tokens change : Example of counter inc || inc || inc INC || INC || INC pay for the next iteration failed failed succeeded Idea: if env progresses, reset the token. inc(){ 1 local done, tmp; 2 done = false; 3 while (!done) { 4 tmp = cnt; 5 done = cas(cnt, tmp, tmp+1); 6 } } cnt 0 1
Detailed Thread-Local Proof of Counter abstract tasks to be finished inc(){ INC(){ <CNT++> } rem(INC) } { cnt = CNT } 1 local done, tmp; 2 done = false; 3 while (!done) { 4 tmp = cnt; 5 done = cas(cnt, tmp, tmp+1); 6 } Embed hi-level code in assertions { cnt = CNT rem(skip) } }
inc(){ 1 local done, tmp; 2 done = false; { cnt = CNT rem(INC) } Assign tokens for loops } 3 while (!done) { { cnt = CNT rem(INC) } pay for one iteration env s progress reset tokens 4 tmp = cnt; { cnt = CNT rem(INC) ( cnt = tmp )} cnt tmp ) } execute hi-level code 5 done = cas(cnt, tmp, tmp+1); { cnt = CNT+1 (done rem(INC)) } { cnt = CNT (done rem(skip)) } pay for the next iteration ( done rem(INC) ) } 6 } }
NOT a total correctness logic! We ensure low-level preserves termination of high-level For loops: ensure progress before consuming all tokens Not ensure termination of low-level/high-level code For loops: not ensure termination before consuming all tokens Example loop a counter inc_loop(){ local tmp; while (true) { tmp = cnt; cas(cnt, tmp, tmp+1); } } INC_LOOP(){ while (true) { <CNT++>; } }
INC_LOOP(){ while (true) { INC; } } inc_loop(){ 1 local tmp; { cnt = CNT rem(INC_LOOP) } } 2 while (true) { Need one token only { cnt = CNT rem(INC_LOOP) } env s progress reset tokens 3 tmp = cnt; { cnt = CNT rem(INC_LOOP) (cnt = tmp cnt tmp )} if cas successful 4 cas(cnt, tmp, tmp+1); { cnt = CNT+1 rem(INC_LOOP) } rem(INC; INC_LOOP) } execute hi-level code { cnt = CNT rem(INC_LOOP) } reset tokens since the thrd progresses 5 } } pay for the next iteration
Summary of Our Informal Ideas Prove termination-preservation of individual threads under env interference Assign tokens for loops Consume a token for each iteration Could reset tokens when env progresses Could reset tokens when current thread progresses
Our Logic for Verifying T S Judgment R, G {p rem(S) } T {q rem(skip)} R, G: rely/guarantee to describe env interference and extended with effects on termination-preservation (i.e. whether current thrd is allowed to reset tokens)
{p rem(S)} T {q rem(skip)} {p} (T , S) {q} R, G R, G If we can find R, G and q such that R, G {p} (T , S) {q} T p S then we have:
Compositionality Rules Just like standard Rely/Guarantee rules, e.g. G2 R1 G1 R2 R1, G1 R2, G2 {p1} (T1 , S1) {q1} {p2} (T2 , S2) {q2} R1 R2, G1 G2 {p1 p2} (T1 T2 , S1 S2) {q1 q2} R, G {p} (T1 , S1) {r} R, G {r} (T2 , S2) {q} R, G {p} (T1;T2 , S1;S2) {q}
Soundness Theorem If we can find R, G and q such that R, G {p} (T , S) {q} T p S then we have:
Applications Linearizability & lock-freedom Counters and its variants Treiber stack Michael-Scott lock-free queue DGLM lock-free queue Correctness of non-atomic objects Synchronous queue (used in Java 6) Equivalence of optimized algo & original one Counters and its variants TAS lock and TTAS lock
Conclusion Logic for termination-preserving refinement of concurrent programs Use tokens for termination-preservation Reset tokens when current thrd or env progresses New rely/guarantee conditions for env interference Compositionality Meta-theory: a new simulation http://kyhcs.ustcsz.edu.cn/relconcur/rgsimt
Examples that we cannot verify Linearizability & lock-freedom Helping HSY elimination-backoff stack Speculation RDCSS algorithm Technically, we use a forward simulation as meta-theory Forward-backward simulation?
Lock-freedom vs. Obstruction-freedom vs. Wait-freedom How is progress of current thread affected by env? Lock-freedom Can be affected only if env progresses Obstruction-freedom Can be affected whatever env does But when the thread executes in isolation, it must progress Wait-freedom Cannot be affected
Modify our logic to verify obstruction-freedom and wait-freedom Our logic: distinguish whether env progresses Could reset tokens when env progresses Lock-freedom Obstruction-freedom Could reset tokens whenever env does But when no env, the thread must progress Wait-freedom Never reset tokens Should also modify definition of T S for obstruction-freedom and wait-freedom
Lock-Based Algorithms Refinement needs to take fairness into account INC(){ <CNT++> } inc(){ lock(l); cnt++; unlock(l); } inc || inc may not terminate in an unfair execution
Hoffmann et al.s logic for lock-freedom [LICS 13] Not prove termination-preservation Need to know the number of threads Token transfer failed failed succeeded loop: pay one token for one iteration cnt 0 1 cas: token transfer
