000212546 001__ 212546
000212546 005__ 20181203024022.0
000212546 0247_ $$2doi$$a10.1145/2734118
000212546 022__ $$a0164-0925
000212546 02470 $$2ISI$$a000356699500001
000212546 037__ $$aARTICLE
000212546 245__ $$aAutomated Classification of Data Races Under Both Strong and Weak Memory Models
000212546 260__ $$bAssoc Computing Machinery$$c2015$$aNew York
000212546 269__ $$a2015
000212546 300__ $$a44
000212546 336__ $$aJournal Articles
000212546 520__ $$aData races are one of the main causes of concurrency problems in multithreaded programs. Whether all data races are bad, or some are harmful and others are harmless, is still the subject of vigorous scientific debate [Narayanasamy et al. 2007; Boehm 2012]. What is clear, however, is that today's code has many data races [Kasikci et al. 2012; Jin et al. 2012; Erickson et al. 2010], and fixing data races without introducing bugs is time consuming [Godefroid and Nagappan 2008]. Therefore, it is important to efficiently identify data races in code and understand their consequences to prioritize their resolution. We present Portend+, a tool that not only detects races but also automatically classifies them based on their potential consequences: Could they lead to crashes or hangs? Could their effects be visible outside the program? Do they appear to be harmless? How do their effects change under weak memory models? Our proposed technique achieves high accuracy by efficiently analyzing multiple paths and multiple thread schedules in combination, and by performing symbolic comparison between program outputs. We ran Portend+ on seven real-world applications: it detected 93 true data races and correctly classified 92 of them, with no human effort. Six of them were harmful races. Portend+'s classification accuracy is up to 89% higher than that of existing tools, and it produces easy-to-understand evidence of the consequences of "harmful" races, thus both proving their harmfulness and making debugging easier. We envision Portend+ being used for testing and debugging, as well as for automatically triaging bug reports.
000212546 6531_ $$aReliability
000212546 6531_ $$aVerification
000212546 6531_ $$aSecurity
000212546 6531_ $$aData races
000212546 6531_ $$aconcurrency
000212546 6531_ $$atriage
000212546 6531_ $$asymbolic execution
000212546 700__ $$uEcole Polytech Fed Lausanne, IC, DSLAB, INN 321, CH-1015 Lausanne, Switzerland$$aKasikci, Baris
000212546 700__ $$0243536$$g183199$$uEcole Polytech Fed Lausanne, IC, DSLAB, INN 319, CH-1015 Lausanne, Switzerland$$aZamfir, Cristian
000212546 700__ $$aCandea, George$$g172241$$0241982
000212546 773__ $$j37$$tAcm Transactions On Programming Languages And Systems$$k3$$q8
000212546 909C0 $$xU11275$$0252225$$pDSLAB
000212546 909CO $$pIC$$particle$$ooai:infoscience.tind.io:212546
000212546 917Z8 $$x172241
000212546 937__ $$aEPFL-ARTICLE-212546
000212546 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000212546 980__ $$aARTICLE