University of Birmingham > Talks@bham > Theoretical computer science seminar > Automatic program analysis for overlaid data structures

Automatic program analysis for overlaid data structures

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

  • UserHongseok Yang, Queen Mary, University of London
  • ClockFriday 11 March 2011, 16:00-17:00
  • HouseUG40 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.