ITU

Progress as Compositional Lock-Freedom

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Standard

Progress as Compositional Lock-Freedom. / Carbone, Marco; Dardha, Ornela; Montesi, Fabrizio.

In: Lecture Notes in Computer Science, 2014, p. 49-64.

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@inproceedings{0329c3b7392043329d0706ee80b16596,
title = "Progress as Compositional Lock-Freedom",
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.",
author = "Marco Carbone and Ornela Dardha and Fabrizio Montesi",
year = "2014",
doi = "10.1007/978-3-662-43376-8_4",
language = "English",
pages = "49--64",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",

}

RIS

TY - GEN

T1 - Progress as Compositional Lock-Freedom

AU - Carbone, Marco

AU - Dardha, Ornela

AU - Montesi, Fabrizio

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-43376-8_4

DO - 10.1007/978-3-662-43376-8_4

M3 - Conference article

SP - 49

EP - 64

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -

ID: 79035570