Practical Lock/Unlock Pairing for Concurrent Programs

The research discusses the challenges of concurrency in parallel programming and the importance of proper lock/unlock pairing to avoid bugs and non-determinism. Tools for bug detection and automated bug fixing are explored, along with examples illustrating the process. The issue of unpaired locks and unlocks due to infeasible paths is also highlighted, emphasizing the need for careful synchronization in concurrent programs.

• Concurrency
• Parallel Programming
• Lock/Unlock Pairing
• Bug Detection
• Synchronization

koplin_j Follow

Uploaded on Oct 11, 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. Practical Lock/Unlock Pairing for Concurrent Programs Hyoun Kyu Cho1, Yin Wang2, Hongwei Liao1, Terence Kelly2, St phane Lafortune1, Scott Mahlke1 1University of Michigan 2Hewlett-Packard Labs University of Michigan 1 Electrical Engineering and Computer Science

2. Parallel Programming Industry wide move to multicores forces parallel programming Inherently difficult Concurrency bugs Non-determinism Intel 4 Core Nehalem AMD 4 Core Shanghai Sun Niagara 2 IBM Cell 2 University of Michigan Electrical Engineering and Computer Science

3. Tools for Parallel Programs Concurrency bug detection tools To statically infer concurrency ex) RacerX[Engler`03] Automated bug fix tools To avoid deadlocks ex) AFix[Jin`11], Gadara[Wang`08] Optimizing compilers Accurate synchronization information can enable more aggressive optimizations University of Michigan 3 Electrical Engineering and Computer Science

4. Examples 1 : int work_on_tree( ) 2 : { 3 : Node *ptr1, *ptr2; 4 : 5 : lock( ptr->mutex ); 6 : while( ptr != NULL ) { 7 : 8 : ptr2 = iterate_next( ptr1 ); 9 : ptr1 = ptr1; 10: } 11: unlock( ptr->mutex ); 12: } 13: Node* iterate_next(Node *current) 14: { 15: Node *next = find(current); 16: 17: lock(next->mutex); 18: unlock(current->mutex); 19: 20: return next; 21: } public class Counter { public void increment() { synchronized (this) { ++count; } } } University of Michigan 4 Electrical Engineering and Computer Science

5. Unpaired Locks and Unlocks Challenges Infeasible paths University of Michigan 5 Electrical Engineering and Computer Science

6. Unpaired Locks Due To Infeasible Paths Example if (x) true void foo(x, A) { if (x) lock(A); if (x) unlock(A); } false lock(A); if(x) true unlock(A); false Feasible Infeasible University of Michigan 6 Electrical Engineering and Computer Science

7. Unpaired Locks and Unlocks Challenges Infeasible paths Spanning function boundaries Pointers Impacts False positives Need programmers annotation Conservative, less efficient University of Michigan 7 Electrical Engineering and Computer Science

8. Practical Lock/Unlock Pairing For a lock, give a set of pairing unlocks and check if the mutex would be released by them for all feasible paths Path-sensitive analysis using a SAT solver Use heuristics based on likely assumptions Instrument code for dynamic checking University of Michigan 8 Electrical Engineering and Computer Science

9. Static Analysis Mapping Lock to Set of Corresponding Unlocks Path Condition Calculation Checking Lock/Unlock Pairing University of Michigan 9 Electrical Engineering and Computer Science

10. Lock/Unlock Pairing Example 01: int foo(struct Task *job) { 02: 03: if(job->hasMutex) 04: lock(job->mutex); //(1) 05: if(job->isSpecial) { 06: // Do some special work 07: if(job->hasMutex) 08: unlock(job->mutex); //(2) 09: return result; 10: } 11: // Do normal work 12: if(job->hasMutex) 13: unlock(job->mutex); //(3) 14: return result; 15: } 1. Map set of corresponding unlocks (1) { (2), (3) } University of Michigan 10 Electrical Engineering and Computer Science

11. Lock/Unlock Pairing Example 01: int foo(struct Task *job) { 02: 03: if(job->hasMutex) 04: lock(job->mutex); //(1) 05: if(job->isSpecial) { 06: // Do some special work 07: if(job->hasMutex) 08: unlock(job->mutex); //(2) 09: return result; 10: } 11: // Do normal work 12: if(job->hasMutex) 13: unlock(job->mutex); //(3) 14: return result; 15: } 2. Calculate Boolean expressions (1): (2): (3): (1): (2): (3): University of Michigan 11 Electrical Engineering and Computer Science

12. Path Condition Calculation Recursively calculate path conditions that decide execution of each lock and unlock Join Point Disjunction (OR) Consecutive conditions in a path Conjunction (AND) src x=true x=false child1 child2 dest Assign same Boolean variable to Branch conditions that should have same value University of Michigan 12 Electrical Engineering and Computer Science

13. Lock/Unlock Pairing Example 3. Examine pairing 01: int foo(struct Task *job) { 02: 03: if(job->hasMutex) 04: lock(job->mutex); //(1) 05: if(job->isSpecial) { 06: // Do some special work 07: if(job->hasMutex) 08: unlock(job->mutex); //(2) 09: return result; 10: } 11: // Do normal work 12: if(job->hasMutex) 13: unlock(job->mutex); //(3) 14: return result; 15: } (1) is paired up with { (2), (3) }. If (1) is executed, (2) or (3) is executed. University of Michigan 13 Electrical Engineering and Computer Science

14. CFG Pruning 1 1 2 3 3,5,6 5 6 4 7 7 8 9 9 10 2,4,8,10,11 11 University of Michigan 14 Electrical Engineering and Computer Science

15. Inter-procedural Analysis Observations Corresponding unlocks share lowest common ancestor (LCA) in the callgraph Depths from locks and unlocks to LCA relatively small Proximity-based Callgraph Partitioning Extend pairing analysis with context University of Michigan 15 Electrical Engineering and Computer Science

16. Dynamic Checking Checking Lock-to-Unlocks Mapping Keeps a map structure from mutex to acquired LOCK_ID When released, check if UNLOCK_ID is in corresponding unlock set of LOCK_ID Checking Semiflow Property Keeps a map structure from function to mutex When function returns, check if holding a mutex that should not be held University of Michigan 16 Electrical Engineering and Computer Science

17. Experimental Setup Implemented pairing in LLVM compiler infrastructure Benchmarks Apache 2.2.11 web server MySQL 5.0.91 database server OpenLDAP 2.4.19 lightweight directory access protocol server pbzip2 1.1.4 pfscan 1.0 aget 0.4 On an Intel Core 2 Quad Q8300 @2.50GHz w/ 8GB MEM University of Michigan 17 Electrical Engineering and Computer Science

18. Effectiveness of Static Analysis Our Approach Speculatively Paired 34 26 0 1 1 0 Benchmarks LOC Locks Trivial DFT Statically Paired 319 463 17 2 10 2 Total Paired 353 489 17 3 11 2 Unpaired 271K 926K 224K 4011 752 835 357 499 19 3 11 2 110 147 0 0 8 2 267 428 0 1 10 2 4 10 2 0 0 0 OpenLDAP MySQL Apache pbzip2 pfscan aget University of Michigan 18 Electrical Engineering and Computer Science

19. Runtime Overhead 4.00% 3.50% Runtime Overhead 3.00% 2.50% 2.00% 1.50% 1.00% 0.50% 0.00% University of Michigan 19 Electrical Engineering and Computer Science

20. Conclusion Practical Lock/Unlock Pairing Combines static analysis and dynamic checking Infeasible path analysis using path conditions Makes likely assumptions and check at runtime Overall, pairs up 98.2% of all locks including 7.1% of them paired speculatively Negligible runtime overhead of 3.4% at most University of Michigan 20 Electrical Engineering and Computer Science