Authors: Jeff Huang, Lawrence Rauchwerger

Venue: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, (ESEC/FSE)
DOI: 10.1145/2786805.2786840
Link to Publication

Abstract:
This paper presents an automated, precise technique, TAME, for identifying schedule-sensitive branches (SSBs) in concurrent programs, i.e., branches whose decision may vary depending on the actual scheduling of concurrent threads. The technique consists of 1) tracing events at fine-grained level; 2) deriving the constraints for each branch; and 3) invoking an SMT solver to find possible SSB, by trying to solve the negated branch condition. To handle the infeasibly huge number of computations that would be generated by the fine-grained tracing, TAME leverages concolic execution and implements several sound approximations to delimit the number of traces to analyse, yet without sacrificing precision. In addition, TAME implements a novel distributed trace partition approach distributing the analysis into smaller chunks. Evaluation on both popular benchmarks and real applications shows that TAME is effective in finding SSBs and has good scalability. TAME found a total of 34 SSBs, among which 17 are related to concurrency errors, and 9 are ad hoc synchronizations. 

@inproceedings{Huang-fsb-2015, 
 author = {Jeff Huang and 
Lawrence Rauchwerger}, 
 bibsource = {dblp computer science bibliography, https://dblp.org}, 
 biburl = {https://dblp.org/rec/conf/sigsoft/HuangR15.bib}, 
 booktitle = {Proceedings of the 2015 10th Joint Meeting on Foundations of Software 
Engineering, {ESEC/FSE} 2015, Bergamo, Italy, August 30 - September 
4, 2015}, 
 doi = {10.1145/2786805.2786840}, 
 editor = {Elisabetta Di Nitto and 
Mark Harman and 
Patrick Heymans}, 
 pages = {439--449}, 
 publisher = {{ACM}}, 
 timestamp = {Tue, 06 Nov 2018 16:59:22 +0100}, 
 title = {Finding schedule-sensitive branches}, 
 url = {https://doi.org/10.1145/2786805.2786840}, 
 year = {2015} 
}