Kobayashi, Naoki and Suenaga, Kohei and Wischik, Lucian - Resource Usage Analysis for the Pi-Calculus

lmcs:2246 - Logical Methods in Computer Science, September 13, 2006, Volume 2, Issue 3
Resource Usage Analysis for the Pi-Calculus

Authors: Kobayashi, Naoki and Suenaga, Kohei and Wischik, Lucian

We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and memory in a valid manner. Our type system is an extension of previous behavioral type systems for the π-calculus, and can guarantee the safety property that no invalid access is performed, as well as the property that necessary accesses (such as the close operation for a file) are eventually performed unless the program diverges. A sound type inference algorithm for the type system is also developed to free the programmer from the burden of writing complex type annotations. Based on the algorithm, we have implemented a prototype resource usage analyzer for the π-calculus. To the authors' knowledge, ours is the first type-based resource usage analysis that deals with an expressive concurrent language like the pi-calculus.

Source : oai:arXiv.org:cs/0608035
DOI : 10.2168/LMCS-2(3:4)2006
Volume: Volume 2, Issue 3
Published on: September 13, 2006
Submitted on: January 25, 2006
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,F.3.1,D.3.1


Consultation statistics

This page has been seen 48 times.
This article's PDF has been downloaded 18 times.