Final year individual project, The Detica Prize for Technical Innovation, 2010
Session programming is a programming model based on the theory of session types, a typing system for pi-calculus. Session types is developed to model structured interaction between processes and correctly typed process will have the property of communication safety. Session Java (SJ) is a full implementation of session types in Java. In this project, we aim to introduce the session programming model to Axel, a heterogeneous cluster with both FPGAs and GPUs as hardware accelerators to design communication safe parallel algorithms.
We give an implementation of a parallel algorithm, n-body simulation, on the Axel cluster, using SJ and FPGAs. We also give a translation of our SJ n-body simulation into C to get a higher performance. We find good performance improvements in both implementations, without compromising safety property of our program.
Finally, we present a formalisation of two new multichannel SJ primitives for parallel programming. We use the formalisation to prove the correctness of our n-body implementation and generalise the proof to a ring topology used by parallel algorithms in SJ.