Home

Recovering resources in the pi-calculus

Recovering resources in the pi-calculus

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
pi-calculus, an extension of the pi-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 dead-process 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 pi-calculus.

By Andris Birkmanis at 2005-04-03 07:48 | Parallel/Distributed | Theory | other blogs | 10429 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Region analysis and a pi-calculus with groups

Region analysis and a pi-calculus with groups

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed pi-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our pi-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the pi-calculus with effects. We propose new equational laws for letregion, analogous to scope mobility laws in the pi-calculus, and show them sound in our semantics.

By Andris Birkmanis at Sun, 2005-04-03 09:22 | login or register to post comments

Computational Shape? FISh Pi?

I hadn't considered a link between region allocation and pi calculus before.

Is it possible there are deeper connections? What about computational shape as used by FISh, Nesl, and Sisal? Are those also connected?

--Shae Erisson - ScannedInAvian.com

By shapr at Sun, 2005-04-03 23:22 | login or register to post comments

More details ?

Well, if you tell me where I migh find out about FISh, Nesl and Sisal, I'll be glad to answer that question.

By David Teller at Tue, 2005-04-05 10:58 | login or register to post comments

Computational Shape? FISh Pi?

The whole gag with FiSh was that it didn't
generate garbage. All memory was either a
static global or stack-allocated. There were
no closures, because all beta-reductions occurred
a compile-time. And there were no lists.
--
Paul Steckler

By steck at Tue, 2005-04-05 21:54 | login or register to post comments

Fame and glory

This is the first time one of my works makes it into a forum. The emotion is near-overwhelming.

More to the point, I'm currently working on improving this study with a more flexible, readable and orthogonal notion of garbage-collection and with a more powerful (although hard-to-read) type system.

By David Teller at Tue, 2005-04-05 11:14 | login or register to post comments