Resource Usage Analysis for the Pi-Calculus

Naoki Kobayashi; Kohei Suenaga; Lucian Wischik

doi:10.2168/LMCS-2(3:4)2006

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

lmcs:2246 - Logical Methods in Computer Science, September 13, 2006, Volume 2, Issue 3 - https://doi.org/10.2168/LMCS-2(3:4)2006

Resource Usage Analysis for the Pi-CalculusArticle

Authors: Naoki Kobayashi ; Kohei Suenaga ; Lucian Wischik

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.

https://doi.org/10.2168/LMCS-2(3:4)2006

Source: arXiv.org:cs/0608035

Volume: Volume 2, Issue 3

Published on: September 13, 2006

Imported on: January 25, 2006

Keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.1, D.3.1

Licence: arXiv.org - Assumed non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Bio-based solvent identification and evaluation for use in polyurethane resin binders for the roofing industry; Code: 98052

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

17 Documents citing this article

Einar Broch Johnsen;Martin Steffen;Johanna Beate Stumpf, 2020, Assumption-Commitment Types for Resource Management in Virtually Timed Ambients, arXiv (Cornell University), pp. 103-121, 10.1007/978-3-030-61362-4_6, http://arxiv.org/abs/1806.08653.

Ivan Prokić;Jovanka Pantović;Hugo Torres Vieira, 2019, A calculus for modeling floating authorizations, Journal of Logical and Algebraic Methods in Programming, 107, pp. 136-174, 10.1016/j.jlamp.2019.06.002.

Jovanka Pantović;Ivan Prokić;Hugo Torres Vieira, 2018, A Calculus for Modeling Floating Authorizations, arXiv (Cornell University), pp. 101-120, 10.1007/978-3-319-92612-4_6, http://arxiv.org/abs/1802.05863.

Julien Lange;Nicholas Ng;Bernardo Toninho;Nobuko Yoshida, 2017, Fencing off go: liveness and safety for channel-based programming, ACM SIGPLAN Notices, 52, 1, pp. 748-761, 10.1145/3093333.3009847.

Chiara Bodei;Viet Dung Dinh;Gian-Luigi Ferrari, 2016, Checking global usage of resources handled with local policies, CINECA IRIS Institutial research information system (University of Pisa), 133, pp. 20-50, 10.1016/j.scico.2016.06.005, http://www.sciencedirect.com/science/article/pii/S0167642316300727.

Julien Lange;Nicholas Ng;Bernardo Toninho;Nobuko Yoshida, 2016, Fencing off go: liveness and safety for channel-based programming, Kent Academic Repository (University of Kent), pp. 748-761, 10.1145/3009837.3009847.

Aurelien Deharbe;Frederic Peschanski, 2014, The Omniscient Garbage Collector: A Resource Analysis Framework, 122, pp. 102-111, 10.1109/acsd.2014.18, https://hal.science/hal-00973747.

Elena Giachino;Cosimo Laneve, 2014, Towards the Typing of Resource Deployment, SPIRE - Sciences Po Institutional REpository, pp. 88-103, 10.1007/978-3-662-45231-8_7, https://inria.hal.science/hal-01091748.

Marc Bezem;Dag Hovland;Hoang Truong, 2012, A type system for counting instances of software components, Theoretical Computer Science, 458, pp. 29-48, 10.1016/j.tcs.2012.07.032.

Chiara Bodei;Viet Dung Dinh;Gian Luigi Ferrari, 2011, Predicting global usages of resources endowed with local policies, Electronic Proceedings in Theoretical Computer Science, 58, pp. 49-64, 10.4204/eptcs.58.4, https://doi.org/10.4204/eptcs.58.4.

Lucia Acciai;Michele Boreale, 2010, Spatial and behavioral types in the pi-calculus, Information and Computation, 208, 10, pp. 1118-1153, 10.1016/j.ic.2009.10.011.

Shuvendu K. Lahiri;Alexander Malkis;Shaz Qadeer, 2010, Abstract Threads, Lecture notes in computer science, pp. 231-246, 10.1007/978-3-642-11319-2_18.

Simon J. Gay;Vasco T. Vasconcelos;António Ravara;Nils Gesbert;Alexandre Z. Caldeira, 2010, Modular session types for distributed object-oriented programming, ACM SIGPLAN Notices, 45, 1, pp. 299-312, 10.1145/1707801.1706335.

Dag Hovland, 2009, A Type System for Usage of Software Components, Lecture notes in computer science, pp. 186-202, 10.1007/978-3-642-02444-3_12.

Lucia Acciai;Michele Boreale, 2008, Spatial and Behavioral Types in the Pi-Calculus, Lecture notes in computer science, pp. 372-386, 10.1007/978-3-540-85361-9_30.

Naoki Kobayashi;Davide Sangiorgi, 2008, A hybrid type system for lock-freedom of mobile processes, ACM Transactions on Programming Languages and Systems, 32, 5, pp. 1-49, 10.1145/1745312.1745313, https://doi.org/10.1145/1745312.1745313.

Naoki Kobayashi;Kohei Suenaga;Lucian Wischik, 2005, Resource Usage Analysis for the π-Calculus, Lecture notes in computer science, pp. 298-312, 10.1007/11609773_20.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3097 times.

This article's PDF has been downloaded 580 times.