Automatic program analysis for overlaid data structures

Add to your list(s) Download to your calendar using vCal

• Hongseok Yang, Queen Mary, University of London
• Friday 11 March 2011, 16:00-17:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

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 joint work with Oukseh Lee and Rasmus Petersen.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.