Automatic program analysis for overlaid data structures

We call a data structure overlaid, if a node in the structure includes links for multiple data structures and these links are intended to be used at the same time. These overlaid data structures are frequently used in systems code, in order to impose multiple types of indexing structures over the same set of nodes. For instance, the deadline IO scheduler of Linux has a queue whose node has links for a doubly-linked list as well as those for a red-black tree. The doubly-linked list here is used to record the order that nodes are inserted in the queue, and the red-black tree provides an efficient indexing structure on the sector fields of the nodes.

In this talk, I will describe an automatic program analysis for these overlaid data structures. I will focus on two main issues in designing such an analysis: how to represent overlaid data structures effectively and how to build an efficient program analyser, which is precise enough to prove the memory safety of realistic examples, such as the Linux deadline IO scheduler. During the talk, I will explain how we addressed the first issue by the combination of standard classical conjunction and separating conjunction from separation logic. Also, I will describe how we used a meta-analysis and the dynamic insertion of ghost instructions for solving the second issue.

This is a joint work with Oukseh Lee and Rasmus Petersen.