Journal article
A type discipline for message passing parallel programs
- Abstract:
- We present ParTypes, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes a protocol to be followed by each processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable (up to decidability of semantic entailment) and that well-typed programs do not deadlock and always terminate. The article is accompanied by a large number of examples drawn from the literature on parallel programming.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 2.7MB, Terms of use)
-
- Publisher copy:
- 10.1145/3552519
Authors
+ Engineering and Physical Sciences Research Council
More from this funder
- Grant:
- EP/X015955/1 - 316931
- EP/N028201/1 - 72043/2
- EP/T014709/1
- EP/T006544/1
- EP/N027833/1
- 309899
- Publisher:
- Association for Computing Machinery
- Journal:
- ACM Transactions on Programming Languages and Systems More from this journal
- Volume:
- 44
- Issue:
- 4
- Pages:
- 1–55
- Article number:
- 26
- Publication date:
- 2022-12-21
- Acceptance date:
- 2022-07-05
- DOI:
- EISSN:
-
1558-4593
- ISSN:
-
0164-0925
- Language:
-
English
- Keywords:
- Pubs id:
-
1317374
- Local pid:
-
pubs:1317374
- Deposit date:
-
2024-01-17
Terms of use
- Copyright holder:
- Vasconcelos et al.
- Copyright date:
- 2022
- Rights statement:
- © 2022 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License.
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record