RECOVERING RESOURCES IN THE π-CALCULUS (DRAFT)

摘要

Although limits of resources such as memory or disk usage are one of the key problems of many communicating applications, most process algebras fail to take this aspect of mobile and concurrent systems into account. In order to study this problem, we introduce the Controlled π-calculus, an extension of the π-calculus with a notion of recovery of unused resources with an explicit (parametrized) garbage-collection and dead-process elimination. We discuss the definition of garbage-collection and deadrprocess elimination for concurrent, communicating applications, and provide a type-based technique for statically proving resource bounds. Selected examples are presented and show the potential of the Controlled π-calculus.