kirancodes.me
To Proof Maintenance & Beyond!

Path-Sensitive Inference of Function Precedence Protocols

Murali Krishna Ramanathan, Ananth Grama, Suresh Jagannathan

Abstract

Function precedence protocols define ordering relations among function calls in a program. In some instances, precedence protocols are well-understood (e.g., a call to pthread_mutex_init must always be present on all program paths before a call to pthread_mutex_lock). Oftentimes, however, these protocols are neither well- documented, nor easily derived. As a result, protocol violations can lead to subtle errors that are difficult to identify and correct. In this paper, we present CHRONICLER, a tool that applies scalable inter-procedural path-sensitive static analysis to automatically infer accurate function precedence protocols. Chronicler computes precedence relations based on a program's control-flow structure, integrates these relations into a repository, and analyzes them using sequence mining techniques to generate a collection of feasible precedence protocols. Deviations from these protocols found in the program are tagged as violations, and represent potential sources of bugs. We demonstrate CHRONICLER's effectiveness by deriving protocols for a collection of benchmarks ranging in size from 66 K to 2 M lines of code. Our results not only confirm the existence of bugs in these programs due to precedence protocol violations, but also highlight the importance of path sensitivity on accuracy and scalability.

BibTeX
@inproceedings{Ramanathan-al:ICSE07,
  author    = {Murali Krishna Ramanathan and
               Ananth Grama and
               Suresh Jagannathan},
  title     = {{Path-Sensitive} Inference of Function Precedence Protocols},
  booktitle = {ICSE},
  pages     = {240--250},
  publisher = {{IEEE} Computer Society},
  year      = {2007},
}

Related papers