MobilityReadingGroup

A Type Discipline for Message Passing Parallel Programs

Vasco T. VASCONCELOS , Francisco MARTINS , Hugo-Andrés LÓPEZ , Nobuko YOSHIDA

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.

@article{VMLY2022,
  author = {Vasco T. Vasconcelos and Francisco Martins and Hugo-Andrés López and Nobuko Yoshida},
  title = {{A Type Discipline for Message Passing Parallel Programs}},
  journal = {ACM Trans. Program. Lang. Syst.},
  series = {4},
  volume = {44},
  pages = {1--55},
  publisher = {Association for Computing Machinery},
  year = 2022
}

@article{VMLY2022,
  author = {Vasco T. Vasconcelos and Francisco Martins and Hugo-Andrés López and Nobuko Yoshida},
  title = {{A Type Discipline for Message Passing Parallel Programs}},
  journal = {ACM Transactions Programming Languages and Systems},
  series = {4},
  volume = {44},
  pages = {1--55},
  publisher = {Association for Computing Machinery},
  doi = "10.1145/3552519",
  year = 2022
}