Rely-Guarantee-Based Simulation for Concurrent Program Transformations
Explore a rely-guarantee-based simulation approach for verifying concurrent program transformations, including compilers for concurrent programs, fine-grained implementations, and software transactional memory. Learn about defining correctness, compositionality, and verification aspects in the context of concurrent program transformations.
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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations Hongjin Liang, Xinyu Feng & Ming Fu Univ. of Science and Technology of China
Concurrent program transformations: Compilers for concurrent programs Source code Multithreaded Java programs T Target code Java bytecode
Concurrent program transformations: Compilers for concurrent programs Fine-grained impl. of algorithms & objects local d,t; d = 0; T while(d==0){ x++; t = x; d = cas(&x, t, t+1); } Impl. of x++;
Concurrent program transformations: Compilers for concurrent programs Fine-grained impl. of algorithms & objects Impl. of software transactional memory (STM) Atomic block (transaction) fine-grained impl.
Concurrent program transformations: Compilers for concurrent programs Fine-grained impl. of algorithms & objects Impl. of software transactional memory (STM) Impl. of concurrent garbage collectors (GC) How to verify such a transformation T ?
How to define correctness of T ? T: Source Target Print a rectangle. C O C T Print a square. Print a triangle. O refinement O C: O has no more observable behaviors (e.g. I/O events by print( )) than C.
How to define correctness of T ? T: Source Target Correct(T): C, O. O = T(C) O C O C: O has no more observable behaviors (e.g. I/O events by print( )) than C.
To verify a concurrent program transformation T : O1 C1 O2 C2 (Compositionality) O1 || O2 C1 || C2 Correct(T): T(C) C for trans. unit C C, O. O = T(C) O C
O1 C1 O1 || O2 C1 || C2 O2 C2 is NOT compositional w.r.t. parallel composition: O: C: local t; x++; t = x; print( x ); x = t + 1; print( x ); We have O C, since output(O) output(C) ; but we do NOT have O||O C||C .
Our contribution: RGSim = Rely/Guarantee + Simulation Compositional w.r.t. parallel composition A proof theory for verifying T Stronger than O C Applications: optimizations, fine-grained obj., concurrent GC,
Background: simulation in CompCert [Leroy et al.] Source state e* * (C, ) (C , ) (C , ) observable event (e.g. I/O) Target state e (O, ) (O , ) (O , )
Simulation in CompCert [Leroy et al.] Can verify T for sequential programs NOT compositional w.r.t. parallel composition O: C: local t; x++; t = x; print( x ); x = t + 1; We have O C , but not O||O C||C print( x );
Simulation in CompCert [Leroy et al.] Can verify T for 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 * *(C , ) (C, ) (C , ) env (C , ) e (O, ) (O , ) env (O , ) (O , ) Too strong to be satisfied, since env. can be arbitrarily bad. In practice, T has assumptions about C & env.
T has assumptions about source code 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 paper 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
What is 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 * * (C, ) (C , ) (C , ) (C , ) G R e (O, ) (O , ) (O , ) (O , ) g r g (O, r, g) (C, R, G)
Soundness theorem If we can find r, g, R and G such that (O, r, g) (C, R, G) O C then we have:
Parallel compositionality (O1, r1, g1) (C1, R1, G1) (O2, r2, g2) (C2, R2, G2) g1 r2 g2 r1 G1 R2 G2 R1 (PAR) (O1||O2, r1 r2, g1 g2) (C1||C2, R1 R2, G1 G2)
More on compositionality (O1, r, g) (C1, R, G) (O2, r, g) (C2, R, G) (O1; O2, r, g) (C1; C2, R, G) (O, r, g) (C, R, G) b B (while b do O, r, g) (while B do C, R, G) An axiomatic proof system for verifying T
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, impl. of x++, 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]
Application: concurrent GC verification Programmer s view of execution: || AbsGC read x write x, v alloc Turns garbage into reusable memory T Real execution: || GC code rB(x) wB(x, v) aB() Concurrent GC impl. = Barriers + GC code How to define Correct(GC) ? Reduce to Correct(T) ! C. T(C) || GC code C || AbsGC
A concurrent GC verification framework C. T(C) || GC code C || AbsGC (T(C) || GC code, r , g ) (C || AbsGC, R , G ) (GC code, r, g) (AbsGC, R, G) Compositionality (T(C), r , g ) (C, R , G ) & Compositionality r, g {p} GC code{q} g G (rB(x), r , g ) (read x, R , G ) (wB(x, v), r , g ) ((write x, v), R , G ) (aB(), r , g ) (alloc, R , G ) [Jones 83] We have verified Hans Boehm s concurrent GC algo [Boehm et al. 91]
Conclusion RGSim = Rely/Guarantee + Simulation Idea: parameterized with interference with env. Compositional! A proof theory for verifying T Optimizations, fine-grained obj., concurrent GC, http://kyhcs.ustcsz.edu.cn/relconcur/rgsim
