A type discipline for message passing parallel programs
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...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Association for Computing Machinery
2022
|
| _version_ | 1826312373578760192 |
|---|---|
| author | Vasconcelos, VT Martins, F López, H-A Yoshida, N |
| author_facet | Vasconcelos, VT Martins, F López, H-A Yoshida, N |
| author_sort | Vasconcelos, VT |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T08:28:00Z |
| format | Journal article |
| id | oxford-uuid:a88a570f-2b15-42e3-8839-abb468bd5f9e |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:28:00Z |
| publishDate | 2022 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:a88a570f-2b15-42e3-8839-abb468bd5f9e2024-02-27T15:16:02ZA type discipline for message passing parallel programsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:a88a570f-2b15-42e3-8839-abb468bd5f9eEnglishSymplectic ElementsAssociation for Computing Machinery2022Vasconcelos, VTMartins, FLópez, H-AYoshida, NWe 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. |
| spellingShingle | Vasconcelos, VT Martins, F López, H-A Yoshida, N A type discipline for message passing parallel programs |
| title | A type discipline for message passing parallel programs |
| title_full | A type discipline for message passing parallel programs |
| title_fullStr | A type discipline for message passing parallel programs |
| title_full_unstemmed | A type discipline for message passing parallel programs |
| title_short | A type discipline for message passing parallel programs |
| title_sort | type discipline for message passing parallel programs |
| work_keys_str_mv | AT vasconcelosvt atypedisciplineformessagepassingparallelprograms AT martinsf atypedisciplineformessagepassingparallelprograms AT lopezha atypedisciplineformessagepassingparallelprograms AT yoshidan atypedisciplineformessagepassingparallelprograms AT vasconcelosvt typedisciplineformessagepassingparallelprograms AT martinsf typedisciplineformessagepassingparallelprograms AT lopezha typedisciplineformessagepassingparallelprograms AT yoshidan typedisciplineformessagepassingparallelprograms |