Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913580456083456 |
|---|---|
| author | Heuvel, Bas van den Pérez, Jorge A. |
| author_facet | Heuvel, Bas van den Pérez, Jorge A. |
| contents | We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $λ$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2111_13091 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks Heuvel, Bas van den Pérez, Jorge A. Logic in Computer Science We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $λ$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence. |
| title | Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2111.13091 |