MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Scalable Session Programming for Heterogeneous High-Performance Systems
Nicholas NG, Nobuko YOSHIDA, Wayne LUK
Software Engineering and Formal Methods - SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD and OpenCert (SEFM Workshops 2013). p. 82 - 98

This paper introduces a programming framework based on the theory of session types for safe and scalable parallel designs. Session-based languages can offer a clear and tractable framework to describe communications between parallel components and guarantee communication-safety and deadlock-freedom by compile-time type checking and parallel MPI code generation. Many representative communication topologies such as ring or scatter-gather can be programmed and verified in session-based programming languages.

We use a case study involving N-body simulation to illustrate the session-based programming style. Finally, we outline a proposal to integrate session programming with heterogeneous systems for efficient and communication-safe parallel applications by a combination of code generation and type checking.

@inproceedings{NYL2013,
  author = {Nicholas Ng and Nobuko Yoshida and Wayne Luk},
  title = {{Scalable Session Programming for Heterogeneous High-Performance Systems}},
  booktitle = {Software Engineering and Formal Methods - SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD and OpenCert},
  series = {LNCS},
  volume = {8368},
  pages = {82--98},
  publisher = {Springer},
  year = 2013
}
@inproceedings{NYL2013,
  author = {Nicholas Ng and Nobuko Yoshida and Wayne Luk},
  title = {{Scalable Session Programming for Heterogeneous High-Performance Systems}},
  booktitle = {Software Engineering and Formal Methods - SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD and OpenCert},
  series = {LNCS},
  volume = {8368},
  pages = {82--98},
  publisher = {Springer},
  doi = "10.1007/978-3-319-05032-4_7",
  year = 2013
}