π-calculus, Session Types research at Imperial College
In this paper, we outline a general picture of our ongoing work on a compilation and execution framework for a class of multicore CPUs [Gelsinger, P., P. Gargini, G. Parker and A. Yu, Microprocessors circa 2000, IEEE SPectrum (1989), pp. 43–47; Olukotun, K., B. A. Nayfeh, L. Hammond, K. G. Wilson and K. Chang, The case for a single-chip multiprocessor, in: ASPLOS, 1996, pp. 2–11; Pham, D. et al., The design and implementation of a first-generation cell processor, in: ISSCC Dig. Tech. Papers (2005), pp. 184–185]. Our focus is to harness the power of concurrency and asynchrony in one of the major forms of multicore CPUs based on distributed, noncoherent memory [Pham, D. et al., The design and implementation of a first-generation cell processor, in: ISSCC Dig. Tech. Papers (2005), pp. 184–185], using the well-known technology of type-directed compilation [Morrisett, G., D. Walker, K. Crary and N. Glew, From System F to typed assembly language, ACM Trans. Program. Lang. Syst. 21 (1999), pp. 527–568]. The key idea is to regard explicit asynchronous data transfer among local caches as typed communication among processes. By typing imperative processes with a variant of session types [Honda, K., V. T. Vasconcelos and M. Kubo, Language primitives and type disciplines for structured communication-based programming, in: ESOP'98, LNCS 1381 (1998), pp. 22–138; Takeuchi, K., K. Honda and M. Kubo, An interaction-based language and its typing system, in: PARLE'94, LNCS 817 (1994), pp. 398–413], we obtain both type-safe and efficient compilation into processes distributed over multiple cores with local memories.
@article{HVY2009, author = {Kohei Honda and Vasco Thudichum Vasconcelos and Nobuko Yoshida}, title = {{Type-Directed Compilation for Multicore Programming}}, journal = {ENTCS}, series = {ENTCS}, volume = {241}, pages = {101--111}, publisher = {Elsevier}, year = 2009 }
@article{HVY2009, author = {Kohei Honda and Vasco Thudichum Vasconcelos and Nobuko Yoshida}, title = {{Type-Directed Compilation for Multicore Programming}}, journal = {Electronic Notes in Theoretical Computer Science}, series = {ENTCS}, volume = {241}, pages = {101--111}, publisher = {Elsevier}, doi = "10.1007/978-3-642-04167-9_12", year = 2009 }