Event-Flow Graphs for Efficient Path-Sensitive Analyses
Ahmed Tamrawi, Suresh Kothari

Experimental Setup

We use the Linux kernel (v3.12) for our empirical evaluation. We consider the spin safe-synchronization property for defining the events of interest for our analysis. We have used Ensoft's C-Atlas platform to compute the events of interest, the CFGs, and EFGs. The C-Atlas first compiles the Linux kernel (v3.12) and pre-computes a database of relationships (i.e., call, control-flow, data-flow, etc.) between various program artifacts. This process took 34 minutes. Then, we query the C-Atlas database to find all the spin synchronization objects (P). This query identifies all the variables passed as parameters to the spin locking (spin_lock, spin_trylock) and unlocking (spin_unlock) functions.
We wrote a Java program using the C-Atlas APIs to determine the set of events for each object by identifying the events e1 and e2 that are defined on p in addition to the relevant data-flow events for (p), including those in which (p) are passed as parameters or return values to other functions. Based on these events, we determine all the Linux kernel functions, referred to as relevant functions, needing to be analyzed for the object (p). Afterward, we wrote the Java program using the C-Atlas APIs to construct the EFG for each relevant function from its corresponding CFG based on the set of events for (p).
In the Linux kernel (v3.12), there are 531 spin objects and in total 3,894 relevant functions for the analysis of all objects. The conversion from CFGs to EFGs using Algorithm II took 9 seconds for all relevant functions. All experiments were carried out on a Windows 8, Intel Core i7 2.40Ghz, 8GB RAM laptop computer.