Resources, Concurrency and Local Reasoning

Speaker: Peter O'Hearn

24th November 2004 , 2pm , Room 519, Claremont Tower

Abstract

Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of {\em resource separation}\/ as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors.

In this talk we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.

----------
Peter O'Hearn
Department of Computer Science
Queen Mary, University of London