Progress as Compositional Lock-Freedom

Marco Carbone, Ornela Dardha, Fabrizio Montesi [2014].
In proceedings of COORDINATION 2014, pp. 49-64.

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.

Links

wikidata.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/coordination/CarboneDM14,
  author       = {Marco Carbone and
                  Ornela Dardha and
                  Fabrizio Montesi},
  editor       = {Eva K{\"{u}}hn and
                  Rosario Pugliese},
  title        = {Progress as Compositional Lock-Freedom},
  booktitle    = {Coordination 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},
  series       = {Lecture Notes in Computer Science},
  volume       = {8459},
  pages        = {49--64},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43376-8\_4},
  doi          = {10.1007/978-3-662-43376-8\_4},
  timestamp    = {Tue, 15 Nov 2022 15:22:35 +0100},
  biburl       = {https://dblp.org/rec/conf/coordination/CarboneDM14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Some data from DBLP and Crossref.