Rely-Guarantee-Based Simulation for Concurrent Program Transformations
A Rely-Guarantee-Based Simulation for
Verifying Concurrent Program Transformations
Hongjin Liang
, Xinyu Feng & Ming Fu
Univ. of Science and Technology of China
•
Compilers for concurrent programs
Concurrent program transformations:
Target
code
Source
code
T
Multithreaded
Java programs
Java bytecode
•
Compilers for concurrent programs
•
Fine-grained impl. of algorithms & objects
x++
;
T
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
?
Concurrent program transformations:
How to define correctness of
T
?
O
C
T
Print a
rectangle.
Print a
square.
Print a
triangle.
T
: Source
O
C
:
O
has no more observable behaviors
(e.g. I/O events by
print(…)
) than
C
.
O
C
refinement
Correct(T):
C, O. O =
T(C)
O
C
How to define correctness of
T
?
T
: Source
O
C
:
O
has no more observable behaviors
(e.g. I/O events by
print(…)
) than
C
.
(Compositionality)
O1
||
O2
Correct(T):
C, O. O =
T(C)
O
C
C1
||
C2
T(C)
C
for
trans. unit C
To verify a concurrent program transformation
T
:
is NOT
compositional
w.r.t. parallel composition:
O:
local t;
t = x;
x = t + 1;
print( x );
C:
x++;
print( x );
We have
O
C
, since
output
(O)
output
(C) ;
b
u
t
w
e
d
o
N
O
T
h
a
v
e
O
|
|
O
C
|
|
C
.
RGSim
=
R
ely/
G
uarantee +
Sim
ulation
•
Compositional w.r.t. parallel composition
•
A proof theory for verifying T
–
Stronger than O
C
–
Applications: optimizations, fine-grained obj.,
concurrent GC, …
Our contribution:
Background: simulation in CompCert
(O,
)
(C,
)
(C’,
’)
(C’’,
’’)
…
…
[Leroy et al.]
Source state
Target state
observable event (e.g. I/O)
O:
local t;
t = x;
x = t + 1;
print( x );
C:
x++;
print( x );
We have
O
C ,
but
not
O
||
O
C
||
C
Simulation in CompCert
[Leroy et al.]
Can verify T for sequential programs
NOT compositional w.r.t. parallel composition
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
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
•
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 !
[Boehm et al. PLDI’08]
Problems of existing simulations :
Our
RGSim
:
•
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
•
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
Nobody else would update x
I guarantee I would not touch y
Nobody else would update y
I guarantee I would not touch x
Compatibility (Interference Constraints):
g2
r1 and
g1
r2
(O,
)
(C,
)
(C’,
’)
(C’’,
’’’)
…
…
G
g
G
g
RGSim = Rely/Guarantee + Simulation
≲
(O,
r, g
)
≲
(C,
R, G
)
Soundness theorem
(O, r, g)
≲
(C, R, G)
If we can find r, g, R and G
such that
then we have:
O
C
Parallel compositionality
More on compositionality
(O
1
, r, g)
≲
(C
1
, R, G)
(O
2
, r, g)
≲
(C
2
, R, G)
(O
1
;
O
2
, r, g)
≲
(C
1
;
C
2
, 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
Real execution:
||
GC code
||
AbsGC
Turns garbage into
reusable memory
T
•
Concurrent GC impl. = Barriers + GC code
•
How to
define
C
orrect(GC) ?
C. T(C)
||
GC code
C
||
AbsGC
Reduce to Correct(T) !
A concurrent GC verification framework
T(C)
||
GC code
C
||
AbsGC
&
[Jones’83]
We have verified Hans Boehm’s
concurrent GC algo
[Boehm et al. 91]
(
T(C)
||
GC code, r’’, g’’)
≲
(C
||
AbsGC, R’’, G’’)
(T(C), r’, g’)
≲
(C, R’, G’)
(GC code, r, g)
≲
(AbsGC, R, 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
’
)
r, g
⊦
{p} GC code{q}Compositionality
Compositionality
C.
g
≲
G
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
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
