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

Data & Results

An Excel sheet listing the compaison between the size of CFG and EFG for all relevant functions for the analysis of spin safe-synchronization property in the Linux kernel (v3.12). Download Now

All the CFGs and EFGs for all relevant functions can be downloaded from here Download Now (38MB). Please follow the instruction for correct viewing and interpretation of the data:
  1. Make sure to download Graphviz software to view all the graphs.
  2. The graph data are organized into three folders depending:
    1. mutex: for Mutex Objects
    2. spin: for Spin Objects
    3. down_read: For Read-Semaphore Objects
  3. In each of those folder, there are many folders in which each folder name correspond to the synchronization object passed to the either locking  or unlocking events. In other words, each folder contains the relevant functions needed to verify the synchronization object denoted by the folder name.
  4. The file (mpg.dot) correspond to a graph showing the relevant functions needed to analyze the synchronization object for that folder. Those graphs are computed via the Matching Pair Graph concept introduced in our previous research.
  5. For each function in (mpg.dot), we generate its corresponding CFG.
  6. Each function will have 3 files:
    1. CFG.* file corresponds to the CFG of the function.
    2. CFG-HL.* file corresponds to the CFG of the function with the event nodes highlighted.
    3. EFG.* file corresponds to the Event Flow Graph of the function.