Abstract:

The increasing complexity of codes with the growing number of cores that should be utilised make such codes hard to optimise and maintain. In this talk, we present the OpenMP and MPI refactoring implemented in the ParaFormance tool. This tool transforms the sequential code into parallel code able to run on shared memory machines. Further refactoring is implemented to adapt the source code to exploit a larger number of processors on large HPC clusters with message passing support. In addition, the resulting MPI code can be used by developers as a starting point for further optimisation. Both refactorings are preceded by an advanced safety checking which reports concurrency problems and gives hints and suggestions on how to fix them.

Title:
A Type-System for describing System-on-a-Chip Architectures

Abstract:
The protocols that describe the interactions between IP Cores on System-on-a-Chip (SoC) architectures are well-documented. These protocols described not only the structural properties of the physical interfaces but also the behaviour of the emanating signals. However, there is a disconnect between the design of SoC architectures, their formal description, and the verification of their implementation in known hardware description languages.

Within the Border Patrol project we are investigating how to capture and reason about the structural and behavioural properties of SoC architectures using state-of-the-art advances in programming language research. Namely, we are investigating using dependent types and session types to capture and reason about hardware communication.

In this talk I will discuss my work in designing a dependent type- system and corresponding language that captures and reasons about the topological structure of a System-on-a-Chip. This language provides correct-by-construction guarantees over:

• the physical structure of an interaction protocol;
• the adherence of a component’s interface to a given protocol; and
• the validity of the specified connections made between components.

We provide these guarantees through the (ab)use of dependent types as presented in Idris; and abuse of indexed monads to reason about resource usage.

Given time I will give an account of how this language enables reasoning about SoC behaviour when considered in conjunction with Session Types.ssion Types.