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
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.
|