Progress as Compositional Lock-Freedom

Marco Carbone, Ornela Dardha, Fabrizio Montesi

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

A session-based process satisfies the progress property if its sessions never get stuck when it is executed in an adequate context. Previous work studied how to define progress by introducing the notion of catalysers, execution contexts generated from the type of a process. In this paper, we refine such definition to capture a more intuitive notion of context adequacy for checking progress. Interestingly, our new catalysers lead to a novel characterisation of progress in terms of the standard notion of lock-freedom. Guided by this discovery, we also develop a conservative extension of catalysers that does not depend on types, generalising the notion of progress to untyped session-based processes. We combine our results with existing techniques for lock-freedom, obtaining a new methodology for proving progress. Our methodology captures new processes wrt previous progress analysis based on session types.

Original languageEnglish
Title of host publicationCoordination Models and Languages : 16th IFIP WG 6.1 International Conference, COORDINATION 2014, Held as Part of the 9th International Federated Conferences on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings
EditorsEva Kühn, Rosario Pugliese
PublisherSpringer
Publication date2014
Pages49-64
ISBN (Print)978-3-662-43375-1
ISBN (Electronic)978-3-662-43376-8
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event17th IFIP WG 6.1 International Conference: Held as Part of the 10th International Federated Conference on Distributed Computing Techniques - Grenoble, France
Duration: 2. Jun 20154. Jun 2015

Conference

Conference17th IFIP WG 6.1 International Conference
Country/TerritoryFrance
CityGrenoble
Period02/06/201504/06/2015

Fingerprint

Dive into the research topics of 'Progress as Compositional Lock-Freedom'. Together they form a unique fingerprint.

Cite this