PA:Lock Analysis

From Trusted Cloud Group
Jump to: navigation, search

Contents

Team Members

Shiqiu Huang, Hao Liu, Jiabin Xia, Di Zhang

Motivation

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.

Introduction

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.

Status

Publication

Technical Documents

Slice for LLVM binary code
KLEE错误种类
KLEE错误处理方式
为KLEE增加自动初始化与符号化功能
Personal tools
Namespaces
Variants
Actions
Navigation
Upload file
Toolbox