Data Races are BadA way to prevent racesContributionThis presentationType Based AnalysisCorrelationCorrelationContext SensitivityExistential Context SensitivityExistential Context SensitivityLinearity of locksLinearity EffectsLinearity ExampleLock StateLock StateLock State ExampleLock State ExampleImplementation exttt {void *}Lazy exttt {struct} fieldsUniquenessExperimentsExperimentsConclusions - Future WorkFormal languageTypesType rulesType rulesPolymorphic Type RulesPolymorphic Type RulesInstSubConstraint ResolutionConstraint ResolutionConstraint ResolutionConstraint Resolution exttt {void *} resultsLazy exttt {struct} fields resultsCONTEXT-SENSITIVECORRELATION ANALYSIS FORDETECTING RACESPolyvios PratikakisJeff FosterMichael HicksUniversity of Maryland, College ParkContext-sensitive Correlation Analysis for Detecting Races – p.1/??Data Races are BadRace: two threads access memory without synchronizationand at least one is a writeRaces are bad:August 14th 2004, Northeastern Blackout1985-1987, Therac-25 medical acceleratorPrograms with races are difficult to understandContext-sensitive Correlation Analysis for Detecting Races – p.2/??A way to prevent racesShared locations ρLocks `Correlation ρB `:Lock` is correlated with pointer ρ if-f ` is held while ρ isaccessedConsistent correlation:A given pointerρ is only correlated with one lock `Assert that every shared location ρ is consistently correlatedwith a single lock`Context-sensitive Correlation Analysis for Detecting Races – p.3/??ContributionInference of correlation between locks and pointers for C:Universal and Existential context sensitivity in correlationpropagationSound race detection using assertion of consistent correlationIt works: we found races!Context-sensitive Correlation Analysis for Detecting Races – p.4/??This presentationCorrelation InferenceUniversal and Existential context sensitivityLinearity of locksLock State (which locks are held at every program point?)Experimental ResultsContext-sensitive Correlation Analysis for Detecting Races – p.5/??Type Based AnalysisAnnotate types with labels:pthread_mutex_t→pthread_mutex_th`iτ*→ τ*hρiCreate constraints among labels to capture data flow andcorrelationDereferencing ρ while ` is held: ρB `Aliasing ρ to ρ0: ρ ≤ ρ0Aliasing ` to `0: ` = `0Solve constraints to close the relation ρB `Verify consistent correlation of every shared ρ with a singlelock` for all dereferences of ρContext-sensitive Correlation Analysis for Detecting Races – p.6/??Correlationpthread mutex t L1 = ...;int x; // &x: int*void munge(pthreadmutex t *l, int * p){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);Context-sensitive Correlation Analysis for Detecting Races – p.7/??Correlationpthread mutex th`1iL1 = ...;int x; // &x: int*hρxivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);ρx`1ρ `mungeContext-sensitive Correlation Analysis for Detecting Races – p.8/??Correlationpthread mutex th`1iL1 = ...;int x; // &x: int*hρxivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);ρx`1ρ `mungeContext-sensitive Correlation Analysis for Detecting Races – p.8/??Correlationpthread mutex th`1iL1 = ...;int x; // &x: int*hρxivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);ρx`1ρ `mungeContext-sensitive Correlation Analysis for Detecting Races – p.8/??Correlationpthread mutex th`1iL1 = ...;int x; // &x: int*hρxivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthread mutex unlock(l);}...munge(&L1, &x);ρx`1ρ `mungeBContext-sensitive Correlation Analysis for Detecting Races – p.8/??Correlationpthread mutex th`1iL1 = ...;int x; // &x: int*hρxivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);ρx`1ρ `mungeBBContext-sensitive Correlation Analysis for Detecting Races – p.8/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);munge(&L2, &y);munge(&L2, &z);ρxρyρz`1`2ρ `mungeBContext-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);munge(&L2, &y);munge(&L2, &z);ρxρyρz`1`2ρ `mungeBContext-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);munge(&L2, &y);munge(&L2, &z);ρxρyρz`1`2ρ `mungeBContext-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge(&L1, &x);munge(&L2, &y);munge(&L2, &z);ρxρyρz`1`2ρ `mungeBBBContext-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge1(&L1, &x);munge2(&L2, &y);munge3(&L2, &z);ρxρyρz`1`2ρ `mungeB(1(1)1(1(1)1Context-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge1(&L1, &x);munge2(&L2, &y);munge3(&L2, &z);ρxρyρz`1`2ρ `mungeB(1(1)1BContext-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 = ...,h`2iL2 = ...;int x, y, z; //hρxi,ρy,hρzivoid munge(pthread mutex th`i*l, int *hρip){pthread mutex lock(l);*p = 3;pthreadmutex unlock(l);}...munge1(&L1, &x);munge2(&L2, &y);munge3(&L2, &z);ρxρyρz`1`2ρ `mungeB(2(2)2(2(2)2Context-sensitive Correlation Analysis for Detecting Races – p.9/??Context Sensitivitypthread mutex th`1iL1 =