View Full Document

CONTEXT-SENSITIVE CORRELATION ANALYSIS FOR DETECTING RACES



View the full content.
View Full Document
View Full Document

5 views

Unformatted text preview:

C ONTEXT SENSITIVE C ORRELATION A NALYSIS FOR D ETECTING R ACES Polyvios Pratikakis Jeff Foster Michael Hicks University of Maryland College Park Context sensitive Correlation Analysis for Detecting Races p 1 Data Races are Bad Race two threads access memory without synchronization and at least one is a write Races are bad August 14th 2004 Northeastern Blackout 1985 1987 Therac 25 medical accelerator Programs with races are difficult to understand Context sensitive Correlation Analysis for Detecting Races p 2 A way to prevent races Shared locations Locks Correlation B Lock is correlated with pointer if f is held while is accessed Consistent correlation A given pointer is only correlated with one lock Assert that every shared location is consistently correlated with a single lock Context sensitive Correlation Analysis for Detecting Races p 3 Contribution Inference of correlation between locks and pointers for C Universal and Existential context sensitivity in correlation propagation Sound race detection using assertion of consistent correlation It works we found races Context sensitive Correlation Analysis for Detecting Races p 4 This presentation Correlation Inference Universal and Existential context sensitivity Linearity of locks Lock State which locks are held at every program point Experimental Results Context sensitive Correlation Analysis for Detecting Races p 5 Type Based Analysis Annotate types with labels pthread mutex t pthread mutex th i h i Create constraints among labels to capture data flow and correlation Dereferencing while is held B Aliasing to 0 0 Aliasing to 0 0 Solve constraints to close the relation B Verify consistent correlation of every shared with a single lock for all dereferences of Context sensitive Correlation Analysis for Detecting Races p 6 Correlation pthread mutex t L1 int x x int l int void munge pthread mutex t pthread mutex lock l p 3 pthread mutex unlock l munge L1 x p Context sensitive Correlation Analysis for Detecting Races p



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view CONTEXT-SENSITIVE CORRELATION ANALYSIS FOR DETECTING RACES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CONTEXT-SENSITIVE CORRELATION ANALYSIS FOR DETECTING RACES and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?