POP Seminar, 02-07-03

A central problem in concurrent programming is how to discipline programs so that different threads of control can only interfere in ways that are predictable and thus easy to reason about. In this talk, we will discuss a type-based approach for statically enforcing safe concurrency, partially inspired by spatial and separation logics. Our type system assigns to each runtime entity (resource) a dynamic spatial-behavioral type, that specifies how such entity may be safely manipulated by one or more threads of control. This contrasts with most other approaches, that focus on identifying structural constraints to the code that manipulates the resources. We will also show how flexible disciplines for control of interference, able to deal with expressive imperative reference-passing higher-order programming languages, such as object-oriented programming, may be compositionally expressed in the framework.