Pattern-Based Synthesis of Synchronization for C++ Memory Model

Examining the pattern-based synthesis of synchronization for the C++ memory model, this study delves into concepts like Dekker's Algorithm and achieving mutual exclusion in parallel programming. It discusses the automatic inference of efficient and correct synchronization under the C++ memory model, emphasizing the challenge of adding minimal and correct synchronization while ensuring sequential consistency. The process involves setting maximally relaxed parameters and iteratively removing behaviors until the specification is satisfied.

• Parallel Programming
• Synchronization
• C++ Memory Model
• Dekkers Algorithm
• Sequential Consistency

tatelynn Follow

Uploaded on Oct 10, 2024 | 0 Views

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.

Presentation Transcript

1. Pattern-based Synthesis of Synchronization for the C++ Memory Model Yuri Meshman, Noam Rinetzky, Eran Yahav 1

2. Goal Verified P SynSynCpp S ,?? ?? ,?? C++ ? , {?? } Note: Assuming: ??? ???? Asking: ??++ ????? 2

3. Dekkers Algorithm store(flag0, 0); store(flag1, 0); store(turn, 0); Thread 0: Thread 1: store(flag0, 1); while(load(flag1) = 1 ){ if(load(turn) =1 ){ store (flag0, 0); while(load(turn) = 1 ) yield(); store(flag0, 1); } } ... // critical section store(turn, 1); store(flag0, 0); store(flag1, 1); while(load(flag0) = 1 ){ if(load(turn) = 0 ){ store(flag1, 0); while(load(turn) = 0 )yield(); store(flag1, 1); } } ... // critical section store(turn, 0); store(flag1, 0); spec: mutual exclusion over critical section sequential consistency Yes 3

4. Dekkers Algorithm store(flag0, 0); store(flag1, 0); store(turn, 0); Thread 0: Thread 1: store(flag0, 1); while(load(flag1) = 1 ){ if(load(turn) =1 ){ store (flag0, 0); while(load(turn) = 1 ) yield(); store(flag0, 1); } } ... // critical section store(turn, 1); store(flag0, 0); store(flag1, 1); while(load(flag0) = 1 ){ if(load(turn) = 0 ){ store(flag1, 0); while(load(turn) = 0 )yield(); store(flag1, 1); } } ... // critical section store(turn, 0); store(flag1, 0); rf rf spec: mutual exclusion over critical section sequential consistency Yes No C++ relaxed model 4

5. Dekkers Algorithm storeSC (flag0, 0); storeSC (flag1, 0); storeSC (turn, 0); Thread 0: Thread 1: storeSC(flag0, 1); while(loadSC (flag1) = 1 ){ if(loadSC (turn) =1 ){ storeRLX (flag0, 0); while(loadRLX (turn) = 1 ) yield(); storeRLX (flag0, 1); } } ... // critical section storeSC (turn, 1); storeREL (flag0, 0); storeSC (flag1, 1); while(loadSC (flag0) = 1 ){ if(loadSC (turn) = 0 ){ storeRLX (flag1, 0); while(loadRLX (turn) = 0 )yield(); storeRLX (flag1, 1); } } ... // critical section storeSC (turn, 0); storeREL(flag1, 0); spec: mutual exclusion over critical section sequential consistency Yes Yes No C++ relaxed model 5

6. In a nutshell Goal Automatic inference of efficient and correct synchronization under C++ memory model. finite-state programs with bounded executions. Challenge Adding minimal and correct synchronization. Solution 1. 2. Assume maximally relaxed parameters setting and Iteratively remove behaviors until specification satisfied. 6

7. Dekkers Algorithm storeRLX (flag0, 0); storeRLX(flag1, 0); storeRLX(turn, 0); store flag0, 0 sb Thread 0: Thread 1: store flag1, 0 storeRLX (flag0, 1); while(loadRLX (flag1) = 1 ){ if(loadRLX (turn) =1 ){ storeRLX (flag0, 0); while(loadRLX (turn) = 1 ) yield(); storeRLX (flag0, 1); } } ... // critical section storeRLX (turn, 1); storeRLX (flag0, 0); storeRLX (flag1, 1); while(loadRLX (flag0) = 1 ){ if(loadRLX (turn) = 0 ){ storeRLX (flag1, 0); while(loadRLX (turn) = 0 )yield(); storeRLX (flag1, 1); } } ... // critical section storeRLX (turn, 0); storeREL(flag1, 0); critical section sb store turn, 0 asw asw store flag0, 1 store flag1, 1 sb sb load flag1 load flag0 rf critical section sb sb rf store turn, 0 store turn, 1 sb sb store flag0, 0 store flag1, 0 7

8. What is an execution store flag0, 0 sb Execution trace is: Instructions store flag1, 0 sb store turn, 0 asw asw store flag0, 1 store flag1, 1 relations: total/partial orders sb sb load flag1 load flag0 rf critical section critical section Axioms on those relations sb sb rf store turn, 0 store turn, 1 sb sb *rf read from sb sequence before asw additionally synchronize with sw synchronize with store flag0, 0 store flag1, 0 8

9. Error trace 1 find pattern LB store flag0, 0 sb store flag1, 0 load buffering sb store turn, 0 asw asw store flag0, 1 store flag1, 1 sb sb load flag1 load flag0 rf critical section critical section sb sb rf store turn, 0 store turn, 1 sb sb *rf read from sb sequence before asw additionally synchronize with sw synchronize with store flag0, 0 store flag1, 0 9

10. Error trace 1 prevented store flag0, 0 sb store flag1, 0 sb store turn, 0 asw asw store flag0, 1 store flag1, 1 sb sb loadACQ flag1 load flag0 rf critical section critical section sw sb sb rf store turn, 0 store turn, 1 sb sb *rf read from sb sequence before asw additionally synchronize with sw synchronize with store flag0, 0 storeREL flag1, 0 10

11. Dekkers Algorithm storeRLX (flag0, 0); storeRLX(flag1, 0); storeRLX(turn, 0); Thread 0: Thread 1: storeRLX (flag0, 1); while(loadACQ (flag1) = 1 ){ if(loadRLX (turn) =1 ){ storeRLX (flag0, 0); while(loadRLX (turn) = 1 ) yield(); storeRLX (flag0, 1); } } ... // critical section storeRLX (turn, 1); storeRLX (flag0, 0); storeRLX (flag1, 1); while(loadRLX (flag0) = 1 ){ if(loadRLX (turn) = 0 ){ storeRLX (flag1, 0); while(loadRLX (turn) = 0 )yield(); storeRLX (flag1, 1); } } ... // critical section storeRLX (turn, 0); storeREL(flag1, 0); spec: mutual exclusion over critical section sequential consistency Yes No C++ relaxed model 11

12. Dekkers Algorithm storeSC (flag0, 0); storeSC (flag1, 0); storeSC (turn, 0); Thread 0: Thread 1: storeSC(flag0, 1); while(loadSC (flag1) = 1 ){ if(loadSC (turn) =1 ){ storeRLX (flag0, 0); while(loadRLX (turn) = 1 ) yield(); storeRLX (flag0, 1); } } ... // critical section storeSC (turn, 1); storeREL (flag0, 0); storeSC (flag1, 1); while(loadSC (flag0) = 1 ){ if(loadSC (turn) = 0 ){ storeRLX (flag1, 0); while(loadRLX (turn) = 0 )yield(); storeRLX (flag1, 1); } } ... // critical section storeSC (turn, 0); storeREL(flag1, 0); spec: mutual exclusion over critical section sequential consistency Yes Yes No C++ relaxed model 12

13. Goal Verified P SynSynCpp ,?? ?? ,?? C++ ? , S {?? } Note: Assuming: ??? ?pec Asking: ??++ ????? 13

14. Synthesis of Synchronization for the C++ Memory Model S Model Checker Verified P {?1,?2,?3, ?? errorTraces(P,S)} ??? ? All solutions to ? Detect patterns and avoid traces ,?? ?? ,?? C++ ? , {?? implement SynSynCpp } Note: Assuming: ??? ? Asking: ??++ ?? 14

15. Challenges 1. ModelChecker: Enumerate error traces? 2. How to detect patterns and avoid traces? 3. How to collect all blocked bad traces and produce a solution? CDSchecker 15

16. Step 1: Get an error trace store flag0, 0 sb store flag1, 0 sb store turn, 0 asw asw store flag0, 1 store flag1, 1 sb sb load flag1 load flag0 rf critical section critical section sb sb rf store turn, 0 store turn, 1 sb sb store flag0, 0 store flag1, 0 16

17. Step 2: Find a pattern Load Buffering pattern load flag1 load flag0 sb sb rf store flag0, 0 store flag1, 0 17

18. Step 3: block the pattern Load Buffering pattern ACQ -- load flag0 ACQ -- load flag1 REL -- store flag1, 1 REL -- store flag0, 1 repeat 1-3 for all error traces 18

19. Step 4: construct ? ?1 ?3 ACQ -- load flag0 ACQ -- load flag1 ?4 REL -- store flag1, 1 ?2 REL -- store flag0, 1 ???1 ?? ??????? ????????1= ?1 ?4 ???2 ?? ??????? ????????1= ?3 ?2 ???????? ????????1= ???1 ?? ??????? ????????1 ???2 ?? ??????? ????????1 ? = ???????? ????????1 ???????? ????????2 19

20. Step 5: Constructing Program Solution ?1 ?3 ACQ -- load flag0 ACQ -- load flag1 ?4 REL -- store flag1, 1 ?2 REL -- store flag0, 1 ??? avoidance = ?0 ?1 ?7 ,?2 ?7 , ? All solutions to ? sol2 sol1 ????????? 20

21. Litmus test patterns First approach: From litmus tests to patterns (Message Passing) (Store Buffering) (Write Read Causality) (Independent Reads Independent Writes) (Load Buffering) 21

22. Patterns relaxation Abstraction Abstraction Generalization Unwinding the cycle (Load Buffering) 22

23. Abstract patterns based on C++RMM RD property RD_CL Cycle RD_MS Missed Store R one of two: 1. R = hb U rf --- preventable with Rel-Acq synchronization 2. R = possible order of instruction preventable with SC 23

24. Benchmarks 9 concurrent algorithms Mutual exclusion algorithms RCU where an update waits only for the reads whose consistency it affects Safety specifications mutual exclusion and reachability invariants stack/RCU coherence invariants 24

25. Results # mini mal soluti ons 5 Time (s) 20s.89 Inferred synchronization (SC, REL, ACQ, RLX) (5, 0, 0, 1), (4, 0, 0, 2), Algorithm abp Memory access patterns hierarchy dekker 3m:22 13 (10, 1, 0, 8), (13, 0, 1, 5), d-prcu-v1 3m:14 7 (7, 2, 1, 0), (7, 1, 0, 2), RLX d-prcu-v2 3h:53m 17 (9, 2, 1, 4), (12, 1, 1, 2), ... Kessel 57m:16 2 (13, 1, 0, 0), (14, 0, 0, 0) REL ACQ peterson 26m:41 2 (11, 1, 0, 1), *(12, 1, 0, 0), (13, 0, 0, 0) bakery 10m:21 6 (16, 1, 1, 0), (17, 0, 1, 0), SC ticket 1m:08 4 (9, 0, 0, 1), (8, 0, 0, 2), treiber stack 1h:05 1 (0, 5, 3, 4) 25

26. Synthesis of Synchronization for the C++ Memory Model S Model Checker Verified P {?1,?2,?3, ?? errorTraces(P,S)} ??? ? avoidance Detect patterns and avoid traces ,?? ?? ,?? C++ ? , {?? implement SynSynCpp } Note: Assuming: ??? ? Asking: ??++ ?? 26

27. Summary Tool: http://www.cs.technion.ac.il/~yurime/SynSynCpp/SynSynCppTool_v1stat.htm Synthesis procedure for inferring memory order synchronizations for C++ RMM Searching for violation patterns Generalized concrete patterns to abstract ones Successfully synthesized nontrivial memory order synchronization for challenging algorithms Future Work: Violation patterns and avoidance templates are not complete Finite-state programs with bounded executions. 27