Sequentializing Concurrent Programs for Efficient Analysis
On Sequentializing Concurrent
On Sequentializing Concurrent
Programs
Programs
Ahmed Bouajjani
Ahmed Bouajjani
LIAFA, University of Paris 7, France
LIAFA, University of Paris 7, France
Michael Emmi
Michael Emmi
LIAFA, University of Paris 7, France
LIAFA, University of Paris 7, France
Gennaro Parlato
Gennaro Parlato
✓
✓
University of Southampton, UK
University of Southampton, UK
What is this talk about?
What is this talk about?
Use of verification tools for sequential programs
Use of verification tools for sequential programs
to analyze concurrent programs
to analyze concurrent programs
Write a sequential program that simulates the concurrent program
Write a sequential program that simulates the concurrent program
Kiss: Keep It Simple and Sequential [Qadeer, Wu—
Kiss: Keep It Simple and Sequential [Qadeer, Wu—
PLDI’04]
PLDI’04]
Many efficient solutions have been developed for sequential programs:
Many efficient solutions have been developed for sequential programs:
SMT-based Bounded Model-Checkers, BDD-based model-checkers,
SMT-based Bounded Model-Checkers, BDD-based model-checkers,
approximation techniques, deductive verification, …
approximation techniques, deductive verification, …
Why don’t we exploit them?
Why don’t we exploit them?
code-to-code translation as a plug-in for sequential tools
code-to-code translation as a plug-in for sequential tools
A convenient way to get new tools for conc. programs …
SC tools:
SC tools:
•
Bounded model checking:
Bounded model checking:
•
ESBMC (FSE’11)
ESBMC (FSE’11)
•
Poirot (by MSR)
Poirot (by MSR)
•
Storm (CAV’09)
Storm (CAV’09)
•
…
…
•
Boolean Programs:
Boolean Programs:
•
Boom, Boppo
Boom, Boppo
•
G
G
ETAFIX
ETAFIX
(PLDI’09)
(PLDI’09)
•
jMoped [SPIN’08]
jMoped [SPIN’08]
•
…
…
•
CHESS (MSR)
CHESS (MSR)
•
Sequentialization + sequ. tools
Sequentialization + sequ. tools
T
1
T
2
T
n
shared vars
(SC semantics)
…
What would it be a good sequential
What would it be a good sequential
simulation?
simulation?
First attempt
First attempt
:
:
Tracking state
Tracking state
: C
: C
1
1
X
X
C
C
2
2
X
X
… C
… C
i
i
…
…
X
X
C
C
n
n
X
X
Shared
Shared
Simulation
Simulation
: at each step simulate one move of a thread
: at each step simulate one move of a thread
State space explosion !
State space explosion !
Q: Can we avoid such an explosion (cross product of locals)?
Q: Can we avoid such an explosion (cross product of locals)?
Yes, if we consider at most 2 context-switches
Yes, if we consider at most 2 context-switches
[Qadeer, Wu—PLDI’04]
[Qadeer, Wu—PLDI’04]
1
3
2
1
3
2
Q: Can we avoid such an explosion (cross product of locals)?
Q: Can we avoid such an explosion (cross product of locals)?
A: YES, for certain under-approximation
A: YES, for certain under-approximation
Q: What about complete simulations ?
Q: What about complete simulations ?
A:
A:
NO!
NO!
(for theoretical reasons)
(for theoretical reasons)
Related works
Related works
•
Up 2 context-switches
Up 2 context-switches
[Qadeer, Wu—PLDI’04]
[Qadeer, Wu—PLDI’04]
•
Many concurrency errors manifest themselves within few context-
Many concurrency errors manifest themselves within few context-
switches
switches
[Musuvathi, Qadeer
[Musuvathi, Qadeer
—PLDI`07
—PLDI`07
]
]
•
Any fixed # context-switches (finite # of threads)
Any fixed # context-switches (finite # of threads)
•
Eager
Eager
[Lal, Reps—CAV`08]
[Lal, Reps—CAV`08]
•
Lazy
Lazy
[La Torre, Parlato, Madhusudan—CAV`09]
[La Torre, Parlato, Madhusudan—CAV`09]
•
Round-Robin schedules & parametrized programs
Round-Robin schedules & parametrized programs
•
Lazy
Lazy
[La Torre, Parlato, Madhusudan—CAV`10]
[La Torre, Parlato, Madhusudan—CAV`10]
•
Delay-bounded schedules (thread creation)
Delay-bounded schedules (thread creation)
[Emmi, Qadeer, Rakamaric—POPL`11]
[Emmi, Qadeer, Rakamaric—POPL`11]
•
Over-approximation
Over-approximation
[Garg, Madhusudan, TACAS`11]
[Garg, Madhusudan, TACAS`11]
Proposed sequentializations
Proposed sequentializations
common characteristics
common characteristics
Avoid cross product (compositional)
Avoid cross product (compositional)
•
1 stack for the simulation
1 stack for the simulation
•
1 local state, fixed # of shared states
1 local state, fixed # of shared states
Conc. & Sequ. Programs are in the same class
Conc. & Sequ. Programs are in the same class
•
i.e. no additional data structures to simulate parallelism
i.e. no additional data structures to simulate parallelism
•
Example: Boolean conc. programs
Example: Boolean conc. programs
Boolean (sequential) program
Boolean (sequential) program
Parametrized:
Parametrized:
increasing the parameter
increasing the parameter
•
more and more behaviors are captured
more and more behaviors are captured
•
at the expense of more computational resources
at the expense of more computational resources
Explore as many behaviors as possible
Explore as many behaviors as possible
•
Goal
Goal
Our contribution
Our contribution
General mechanism
General mechanism
enabling
enabling
compositional sequentializations
compositional sequentializations
•
Under-approximations
Under-approximations
Captures at least or more behaviors than existing
Captures at least or more behaviors than existing
sequentializations
sequentializations
Existing sequentializations can be seen as a restrictions of ours
Existing sequentializations can be seen as a restrictions of ours
Our
Our
Concurrent
Concurrent
Sequential
Sequential
Translation
Translation
- Compositional semantics
- Compositional semantics
- Thread interfaces
- Thread interfaces
- Bounded semantics (restricted compositional semantics)
- Bounded semantics (restricted compositional semantics)
Compositional Semantics
Compositional Semantics
(code-to-code translation to sequ. programs)
(code-to-code translation to sequ. programs)
P
P
::=
::=
var
var
g:T H
g:T H
H
H
::=
::=
proc
proc
p (
p (
var
var
l:T ) s
l:T ) s
s ::= s; s | x := e | skip |
s ::= s; s | x := e | skip |
assume
assume
e
e
|
|
if
if
e
e
then
then
s
s
else
else
s |
s |
while
while
e
e
do
do
s
s
|
|
call
call
x := p e |
x := p e |
return
return
e
e
|
|
post
post
p e |
p e |
yield
yield
//Concurrent
//Concurrent
stmt
stmt
x ::= g | l
x ::= g | l
Key concept: Thread interface
Key concept: Thread interface
An
An
interface
interface
of a thread T in an
of a thread T in an
execution
execution
captures the interactions (shared
captures the interactions (shared
states)
states)
of
of
T and all its sub-threads
T and all its sub-threads
with
with
the remaining threads involved
the remaining threads involved
in the execution
in the execution
Thread interface
s
1
s
1
’
s
2
s
3
s
4
s
5
s
2
’
s
3
’
s
4
’
s
5
’
How to compute Thread interface
How to compute Thread interface
•
Every thread creation is transformed into a procedure call
Every thread creation is transformed into a procedure call
•
A thread procedure
A thread procedure
•
computes an interface of the thread by simulating its code
computes an interface of the thread by simulating its code
•
The thread procedure keeps the following data structure to
The thread procedure keeps the following data structure to
compute the interface
compute the interface
EXP
:
Interface to export
BAG
:
Interfaces imported from posted threads
Updating the interface data-structure:
Updating the interface data-structure:
initialization
initialization
The procedure that simulates a thread first
The procedure that simulates a thread first
initializes
initializes
the interface data-
the interface data-
structure:
structure:
•
interface to export
interface to export
is initialized with one round ( s
is initialized with one round ( s
1
1
, s
, s
1
1
)
)
( s
( s
1
1
is a guessed shared state)
is a guessed shared state)
•
bag of
bag of
imported interfaces
imported interfaces
is empty
is empty
∅
EXP
:
Interface to export
BAG
:
Interfaces imported from posted threads
Updating the interface data-structure:
Updating the interface data-structure:
thread creation (post)
thread creation (post)
At any
At any
thread creation
thread creation
:
:
post
post
p e
p e
transformed
transformed
interface :=
interface :=
call
call
thread-p e;
thread-p e;
Add( BAG, interface );
Add( BAG, interface );
EXP
:
Interface to export
BAG
:
Interfaces imported from posted threads
Updating the interface data-structure
Updating the interface data-structure
context-switch (yield)
context-switch (yield)
At any
At any
yield point
yield point
non deterministically either
non deterministically either
1.
interact at least once with internal threads, or
interact at least once with internal threads, or
2.
interact with an external thread
interact with an external thread
EXP
:
Interface to export
BAG
:
Interfaces imported from posted threads
Updating the interface data-structure
Updating the interface data-structure
context-switch (yield)
context-switch (yield)
At any
At any
yield point
yield point
non deterministically either
non deterministically either
1.
interact at least once with internal threads, or
interact at least once with internal threads, or
2.
interact with an external thread
interact with an external thread
•
Add a new round (
Add a new round (
a
a
,
,
a
a
) to the interface to export (
) to the interface to export (
a
a
is guessed )
is guessed )
EXP
:
Interface to export
BAG
:
Interfaces imported from posted threads
Sequential semantics for conc. programs
Sequential semantics for conc. programs
We’ve obtained a sequential program that
We’ve obtained a sequential program that
simulates the conc. program by computing
simulates the conc. program by computing
interfaces
interfaces
Each Thread code
Each Thread code
p
p
is replaced by the procedure
is replaced by the procedure
thread-p
thread-p
:
:
•
Variables: Locals + Interface data-structure
Variables: Locals + Interface data-structure
•
Initialize the interface data-structure
Initialize the interface data-structure
•
The code of the original thread is attached
The code of the original thread is attached
•
Only post, and yield statement are replaced with new code
Only post, and yield statement are replaced with new code
(simulating the operations presented previously)
(simulating the operations presented previously)
•
At yield a yield statement (or return) return the exported
At yield a yield statement (or return) return the exported
interface
interface
interface data-structure is unbounded
interface data-structure is unbounded
•
An interface as a list:
Bounding & Compressing
Bounding & Compressing
Bounding & Compressing
Bounding & Compressing
•
Bound
Bound
the # nodes in the interface data structure
the # nodes in the interface data structure
•
Compress
Compress
the bag of exported interface a
the bag of exported interface a
s a DAG
s a DAG
We merge two node (
We merge two node (
x
x
,
,
y
y
) and (
) and (
y
y
,
,
z
z
) into (x,z)
) into (x,z)
Our Sequentialization
Our Sequentialization
Compositional Semantics
+
Bounding & Compressing
All existing sequentializations
All existing sequentializations
can be simulated
can be simulated
- Up 2 context-switches
[Qadeer, Wu—PLDI’04]
- Any fixed # context-switches (finite # of threads)
- Eager
[Lal, Reps—CAV`08]
- Lazy
[La Torre, Parlato, Madhusudan—CAV`09]
- Round-Robin schedules & parametrized programs
- Lazy
[La Torre, Parlato, Madhusudan—CAV`10]
- Delay bounded schedules (thread creation)
[Emmi, Qadeer, Rakamaric—POPL`11]
initial
shared
state
Sequ. for any fixed # context-switches
Sequ. for any fixed # context-switches
(finite # of threads)
(finite # of threads)
[Lal, Reps—CAV`08]
[Lal, Reps—CAV`08]
1
2
3
Conclusions
Conclusions
Conclusions
Conclusions
:
:
We have presented a general mechanism
We have presented a general mechanism
enabling
enabling
compositional
compositional
sequentializations of concurrent programs (under SC)
sequentializations of concurrent programs (under SC)
-
parameterized (bounding & compressing the # of nodes in the interfaces)
parameterized (bounding & compressing the # of nodes in the interfaces)
-
more behaviors than existing sequentializations
more behaviors than existing sequentializations
-
Thread creation, parameterized programs, finite # threads
Thread creation, parameterized programs, finite # threads
-
All existing sequentializations can be explained within our framework
All existing sequentializations can be explained within our framework
Weak Memory models:
Weak Memory models:
-
Translation TSO
Translation TSO
SC
SC
[Atig, Bouajjani, Parlato—CAV`11]
[Atig, Bouajjani, Parlato—CAV`11]
-
TSO
TSO
SC
SC
sequential
sequential
Future works
Future works
:
:
-
Experimental evaluation
Experimental evaluation
-
Sequentializations for
Sequentializations for
distributed programs
distributed programs
(FIFO channels) ?
(FIFO channels) ?
-
The Tree-width of Auxiliary Storage
The Tree-width of Auxiliary Storage
[Madhusudan, Parlato—
[Madhusudan, Parlato—
POPL`11]
POPL`11]
-
Lazy transformation of our sequentialization
Lazy transformation of our sequentialization
[La Torre, Madhusudan, Parlato—CAV`09, CAV`10]
[La Torre, Madhusudan, Parlato—CAV`09, CAV`10]
Thanks!
This talk discusses the use of verification tools meant for sequential programs to analyze concurrent programs. It explores the idea of simulating concurrent programs using sequential programs and highlights the efficiency of various solutions developed for sequential programs. The talk also delves into code-to-code translation techniques and the challenges of sequential simulations in the context of concurrent programs.
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
On Sequentializing Concurrent Programs Ahmed Bouajjani LIAFA, University of Paris 7, France Michael Emmi LIAFA, University of Paris 7, France Gennaro Parlato University of Southampton, UK
What is this talk about? Use of verification tools for sequential programs to analyze concurrent programs Write a sequential program that simulates the concurrent program Kiss: Keep It Simple and Sequential [Qadeer, Wu PLDI 04] Many efficient solutions have been developed for sequential programs: SMT-based Bounded Model-Checkers, BDD-based model-checkers, approximation techniques, deductive verification, Why don t we exploit them?
code-to-code translation as a plug-in for sequential tools shared vars (SC semantics) Concurrent Program T1 T2 Tn A convenient way to get new tools for conc. programs
What would it be a good sequential simulation? First attempt: Tracking state: C1X C2X Ci X Cn X Shared Simulation: at each step simulate one move of a thread State space explosion ! Q: Can we avoid such an explosion (cross product of locals)? Q: Can we avoid such an explosion (cross product of locals)? Yes, if we consider at most 2 context-switches A: YES, for certain under-approximation [Qadeer, Wu PLDI 04] 2 Q: What about complete simulations ? 3 3 2 1 A: NO! (for theoretical reasons) 1
Related works Up 2 context-switches [Qadeer, Wu PLDI 04] Many concurrency errors manifest themselves within few context- switches [Musuvathi, Qadeer PLDI`07] Any fixed # context-switches (finite # of threads) Eager [Lal, Reps CAV`08] Lazy [La Torre, Parlato, Madhusudan CAV`09] Round-Robin schedules & parametrized programs Lazy [La Torre, Parlato, Madhusudan CAV`10] Delay-bounded schedules (thread creation) [Emmi, Qadeer, Rakamaric POPL`11] Over-approximation [Garg, Madhusudan, TACAS`11]
Proposed sequentializations common characteristics Avoid cross product (compositional) 1 stack for the simulation 1 local state, fixed # of shared states Conc. & Sequ. Programs are in the same class i.e. no additional data structures to simulate parallelism Example: Boolean conc. programs Boolean (sequential) program Parametrized:increasing the parameter more and more behaviors are captured at the expense of more computational resources Explore as many behaviors as possible Goal
Our contribution General mechanism enabling compositional sequentializations Under-approximations Captures at least or more behaviors than existing sequentializations Existing sequentializations can be seen as a restrictions of ours
Our Concurrent Sequential Translation - Compositional semantics - Thread interfaces - Bounded semantics (restricted compositional semantics)
Compositional Semantics (code-to-code translation to sequ. programs) P ::= var g:T H shared vars (SC semantics) H ::= proc p (var l:T ) s s ::= s; s | x := e | skip | assume e | if e then s else s | while e do s | call x := p e | return e T1 T2 Tn | post p e | yield//Concurrent stmt Main idea of the sequentialization Transform each thread creation into a procedure call: post p e call g:=p e x ::= g | l Only one interaction Solution (return all possible interactions) post p e call INTERFACE:=p e
Key concept: Thread interface s1 s1 An interface of a thread T in an execution s2 s2 captures the interactions (shared states) s3 s3 of s4 s4 T and all its sub-threads with s5 s5 the remaining threads involved in the execution Thread interface
How to compute Thread interface Every thread creation is transformed into a procedure call A thread procedure computes an interface of the thread by simulating its code The thread procedure keeps the following data structure to compute the interface BAG: Interfaces imported from posted threads EXP: Interface to export
Updating the interface data-structure: initialization BAG: Interfaces imported from posted threads EXP: Interface to export s1 s1 The procedure that simulates a thread first initializes the interface data- structure: interface to export is initialized with one round ( s1, s1 ) bag of imported interfaces is empty ( s1 is a guessed shared state)
Updating the interface data-structure: thread creation (post) BAG: Interfaces imported from posted threads EXP: Interface to export At any thread creation: post p e transformed interface := call thread-p e; Add( BAG, interface );
Updating the interface data-structure context-switch (yield) BAG: Interfaces imported from posted threads EXP: Interface to export a b a b At any yield point non deterministically either 1. interact at least once with internal threads, or 2. interact with an external thread
Updating the interface data-structure context-switch (yield) BAG: Interfaces imported from posted threads EXP: Interface to export a a At any yield point non deterministically either 1. interact at least once with internal threads, or 2. interact with an external thread Add a new round (a,a) to the interface to export ( a is guessed )
Sequential semantics for conc. programs We ve obtained a sequential program that simulates the conc. program by computing interfaces Each Thread code p is replaced by the procedure thread-p: Variables: Locals + Interface data-structure Initialize the interface data-structure The code of the original thread is attached Only post, and yield statement are replaced with new code (simulating the operations presented previously) At yield a yield statement (or return) return the exported interface interface data-structure is unbounded
Bounding & Compressing An interface as a list: b a d c b d f h a c e g f e h g
Bounding & Compressing Bound the # nodes in the interface data structure Compress the bag of exported interface as a DAG We merge two node (x, y) and (y,z) into (x,z) - Ex 2. - Ex 1. y z y x y x y z
Our Sequentialization Compositional Semantics + Bounding & Compressing
All existing sequentializations can be simulated - Up 2 context-switches [Qadeer, Wu PLDI 04] - Any fixed # context-switches (finite # of threads) - Eager - Lazy [La Torre, Parlato, Madhusudan CAV`09] [Lal, Reps CAV`08] - Round-Robin schedules & parametrized programs - Lazy - Delay bounded schedules (thread creation) [La Torre, Parlato, Madhusudan CAV`10] [Emmi, Qadeer, Rakamaric POPL`11]
Sequ. for any fixed # context-switches (finite # of threads) [Lal, Reps CAV`08] initial shared state round 1 round 2 T1 T2 Tn round k 3 1 2
Conclusions: We have presented a general mechanism enabling compositional sequentializations of concurrent programs (under SC) - parameterized (bounding & compressing the # of nodes in the interfaces) - more behaviors than existing sequentializations - Thread creation, parameterized programs, finite # threads - All existing sequentializations can be explained within our framework Thanks! Weak Memory models: - Translation TSO SC [Atig, Bouajjani, Parlato CAV`11] - TSO SC sequential Future works: - Experimental evaluation - Sequentializations for distributed programs (FIFO channels) ? - The Tree-width of Auxiliary Storage POPL`11] - Lazy transformation of our sequentialization [La Torre, Madhusudan, Parlato CAV`09, CAV`10] [Madhusudan, Parlato
