Finding schedule-sensitive branches Conference Paper uri icon

abstract

  • © 2015 ACM. 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.

name of conference

  • ESEC/FSE'15: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering

published proceedings

  • Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering

author list (cited authors)

  • Huang, J., & Rauchwerger, L

citation count

  • 14

complete list of authors

  • Huang, Jeff||Rauchwerger, Lawrence

editor list (cited editors)

  • Nitto, E. D., Harman, M., & Heymans, P.

publication date

  • August 2015