Highly accurate and scalable critical section inference can reduce false positives for static concurrency bug detection, can reduce runtime overhead of dynamic tools by instrumenting less, and can benefit compiler optimization. However, existing program analysis techniques trade off between efficiency and precision, and are not optimized for critical section inference.
Our project propose to combine highly scalable lockset analysis, which identifies functions with ambiguous locksets, and highly accurate symbolic execution, which resolves the ambiguity of these functions locally, for better analysis results. We use KLEE for the symbolic execution. To improve the performance of our execution, we use program slicing to reduce the large scale of source code.