A Type Discipline for Message Passing Parallel Programs

Vasco T. Vasconcelos; Francisco Martins; Hugo Andrés López; Nobuko Yoshida

doi:10.1145/3552519

A Type Discipline for Message Passing Parallel Programs

Vasco T. Vasconcelos, Francisco Martins, Hugo Andrés López, Nobuko Yoshida

Software, Data, People & Society

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer review

5 Citationer (Scopus)

31 Downloads (Pure)

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.

Originalsprog	Engelsk
Artikelnummer	26
Tidsskrift	ACM Transactions on Programming Languages and Systems
Vol/bind	44
Udgave nummer	4
Antal sider	55
ISSN	0164-0925
DOI	https://doi.org/10.1145/3552519
Status	Udgivet - 2022

Bibliografisk note

Funding Information:
This work was supported by FCT through project Advanced Type Systems for Multicore Programming (PTDC/EIA-CCO/122547) and the LASIGE Research Unit (UID/CEC/00408/2019), EC Cost Action EUTypes (CA15123), EPSRC (EPSRC (EP/T006544/1, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T006544/1, EP/T014709/1, EP/V000462/1, and EP/X015955/1), NCSS/EPSRC VeTSS, the Innovation Fund Denmark project EcoKnow.org (7050-00034A), and the European Union Marie Sklodowska-Curie grant agreement BehAPI (778233).

Publisher Copyright:
© 2022 Copyright held by the owner/author(s).

Adgang til dokumentet

10.1145/3552519Licens: CC BY

FulltextForlagets udgivne version, 2,71 MBLicens: CC BY

Biblioteksadgang?

Tjek tilgængelighed hos det Kgl. Bibliotek

Andre filer og links

Link to publication in Scopus

Citationsformater

@article{6a9ba7ff01c7439eb12b21d494acae94,

title = "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.",

keywords = "dependent types, message passing computation, Parallel programs, termination",

author = "Vasconcelos, {Vasco T.} and Francisco Martins and L{\'o}pez, {Hugo Andr{\'e}s} and Nobuko Yoshida",

note = "Publisher Copyright: {\textcopyright} 2022 Copyright held by the owner/author(s).",

year = "2022",

doi = "10.1145/3552519",

language = "English",

volume = "44",

journal = "ACM Transactions on Programming Languages and Systems",

issn = "0164-0925",

publisher = "Association for Computing Machinery, Inc.",

number = "4",

}

TY - JOUR

T1 - A Type Discipline for Message Passing Parallel Programs

AU - Vasconcelos, Vasco T.

AU - Martins, Francisco

AU - López, Hugo Andrés

AU - Yoshida, Nobuko

PY - 2022

Y1 - 2022

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

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

KW - dependent types

KW - message passing computation

KW - Parallel programs

KW - termination

UR - http://www.scopus.com/inward/record.url?scp=85146418248&partnerID=8YFLogxK

U2 - 10.1145/3552519

DO - 10.1145/3552519

M3 - Journal article

AN - SCOPUS:85146418248

SN - 0164-0925

VL - 44

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

IS - 4

M1 - 26

ER -