Isolation Types and Multi-core Processors

Abstract

Private local memory and shared memory in multi-core systems causes headaches: programs have concurrency errors (races); cache effects expose the fiction of random access memory; and private local memory requires explicit inter-processor data transfers.

We show how an intuitive type system can enforce data isolation between tasks. This eliminates data races and also allows a compiler to freely allocate tasks to processors without changing program meaning and with increased performance predictability.

Short bio

Alan Mycroft is Professor of Computing in the Computer Laboratory of Cambridge University -- where he has been a faculty member since 1984. He is also a Fellow at Robinson College and co-founder of the European Association for Programming Languages and Systems and a co-founder and Trustee of the Raspberry Pi Foundation. He has degrees in Mathematic (Cambridge) and Computer Science (Edinburgh). He is the author of around 100 research papers and has supervised over 20 PhD theses. His research centres on programming languages, their semantics, optimisation and implementation. He maintains strong industrial links, having worked at AT&T Laboratoriesand at Intel Research during academic leave, as well as spinning out Codemist Ltd who built the original ARM C Compiler under the 'Norcroft' name.