Towards static deadlock resolution in the π-calculus

Marco Giunti, António Ravara

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Citations (Scopus)

Abstract

Static analysis techniques based on session types discern concurrent programs that ensure the fidelity of protocol sessions - for each input (output) end point of a session there is exactly an output (input) end point available - being expressive enough to represent the standard -calculus and several typing disciplines. More advanced type systems, enforcing properties as deadlock-freedom or even progress, sensibly reduce the set of typed processes, thus mining the expressiveness of the analysis. Herein, we propose a first step towards a compromise solution to this problem: a session based type checking algorithm that releases some deadlocks (when co-actions on the same channel occur in sequence in a thread). This procedure may help the software development process: the typing algorithm detects a deadlock, but instead of rejecting the code, fixes it by looking into the session types and producing new safe code that obeys the protocols and is deadlock-free.

Original languageEnglish
Title of host publicationTrustworthy Global Computing - 8th International Symposium, TGC 2013, Revised Selected Papers
PublisherSpringer-Verlag
Pages136-155
Number of pages20
Volume8358 LNCS
ISBN (Print)9783319051185
DOIs
Publication statusPublished - 2014
Event8th International Symposium on Trustworthy Global Computing, TGC 2013 - Buenos Aires, Argentina
Duration: 30 Aug 201331 Aug 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8358 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference8th International Symposium on Trustworthy Global Computing, TGC 2013
CountryArgentina
CityBuenos Aires
Period30/08/1331/08/13

Fingerprint Dive into the research topics of 'Towards static deadlock resolution in the π-calculus'. Together they form a unique fingerprint.

Cite this