Sequentializing Concurrent Programs for Efficient Analysis
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
