TY - GEN
T1 - Finding schedule-sensitive branches
AU - Huang, Jeff
AU - Rauchwerger, Lawrence
PY - 2015/8/30
Y1 - 2015/8/30
N2 - This paper presents an automated, precise technique, TAME, for identifying schedule-sensitive branches (SSBs) in con- current 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 bench- marks 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.
AB - This paper presents an automated, precise technique, TAME, for identifying schedule-sensitive branches (SSBs) in con- current 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 bench- marks 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.
KW - Schedule-sensitive branches
KW - Symbolic constraint analysis
UR - http://www.scopus.com/inward/record.url?scp=84960346154&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84960346154&partnerID=8YFLogxK
U2 - 10.1145/2786805.2786840
DO - 10.1145/2786805.2786840
M3 - Conference contribution
AN - SCOPUS:84960346154
T3 - 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015 - Proceedings
SP - 439
EP - 449
BT - 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015 - Proceedings
PB - Association for Computing Machinery, Inc
T2 - 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015
Y2 - 30 August 2015 through 4 September 2015
ER -