Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems

现代计算系统正变得越来越多样化，但所有新兴计算平台的共同特征是，通过提供大量处理器内核，并行执行许多计算的潜力不断增加。由各种不同平台组成的计算机系统具有快速有效地执行任务的巨大潜力。然而，为这样的系统编程是一个巨大的挑战。通过提高时钟速度来提高性能的时代已经结束，我们已经进入了一个只能通过增加异构计算核心数量以及软件对其有效利用来提高性能的时代。由于使用现有技术使现有的并行软件适应新的硬件架构需要付出巨大的努力，因此存在一个非常现实的危险，即硬件性能的未来进步将对使用遗留软件的实际大规模计算产生很小的影响。我们在本提案中要解决的具体挑战是如何利用给定计算平台的并行性，例如多核CPU，图形处理器（GPU）或现场可编程门阵列（FPGA），以最好的方式，而不必改变原始程序。这些不同的平台在可用的并行性方面具有非常不同的属性，这取决于处理核心和内存的性质和组织。特别是fpga具有巨大的并行潜力，但它们在架构上与主流处理器截然不同。这使得它们很难编程。这里的关键问题是如何转换程序，使其能够最好地利用计算平台提供的并行性的潜力，以及至关重要的是，如何做到这一点，从而保证生成的程序具有与原始程序相同的行为。我们建议的方法是使用一种称为多方会话类型的高级类型系统来描述组成计算的任务之间的通信。打个粗略的比方，计算可以被看作是一条汽车装配线，其中每个单元执行一项特定的任务，如油漆、安装门、车轮、电机等。根据工厂的组织和组成，执行这些操作的顺序将决定汽车组装的速度。但是，在对操作进行重新排序时，当然必须确保更改顺序不会导致错误的组装。回到计算问题，通过使用多方会话类型来描述通信，我们有一种关于转换的正式推理方法。通过为转换开发一种形式语言，我们可以证明它们的正确性。这是该建议的主要新颖之处：类型转换的形式系统。实际的转换可以看作是这种形式语言中的“程序”。他们将通过计算平台的属性获得信息。为了提供转换和平台之间的这种联系，我们还将开发并行计算平台的正式描述。通过将这些正式系统构建到编译器中，我们将能够将程序转换为在混合多核平台上以最有效的方式运行。这项研究的主要好处是，程序员不需要深入了解混合多核平台的高度复杂架构。这对于科学计算来说是非常有益的，因为这也意味着程序不需要重写就可以在新系统上以最佳性能运行。为了证明我们方法的有效性，我们的目标是开发一个概念验证编译器，它将转换程序，使它们可以在fpga上运行，因为这种类型的计算平台与其他平台最不同，因此最具挑战性。

Modern computing systems are becoming increasingly diverse, but the common feature of all emerging computing platforms is the increased potential for performing many computations in parallel, by providing large numbers of processor cores. Computer systems consisting of various different platforms have great potential for performing tasks fast and efficiently. However, programming such systems is a great challenge. The era of performance increase through increased clock speeds has come to an end and we have entered a period where performance increases can only come from increased numbers of heterogeneous computational cores and their effective exploitation by software. Because of the immense effort required to adapt existing parallel software to novel hardwarearchitectures with present technology, there is a very real danger that future advances in hardware performance will have little impact on practical large-scale computingusing legacy software.The specific challenge that we want to address in this proposal is how to exploit the parallelism of a given computing platform, e.g. a multicore CPU, a graphics processor (GPU) or a Field-Programmable Gate Array (FPGA), in the best possible way, without having to change the original program. These different platforms have very different properties in terms of the available parallelism, depending on the nature and organisation of the processing cores and the memory. In particular FPGAs have great potential for parallelism but they are radically different in architecture from mainstream processors. This makes them very difficult to program.The key problem here is how to transform a program so that it will best use the potential for parallelism provided by the computing platform, and crucially, how to do this so that the resulting program is guaranteed to have the same behaviour as the original program.Our proposed approach is to use an advanced type system called Multi-Party Session Types to describe the communication between the tasks that make up a computation. To use a rough analogy, the computation could for instance be viewed as a car assembly line, where every unit performs a particular task such as painting, inserting doors, wheels, motor etc. Depending on the organisation and composition of the factory, the order in which these operations is performed will determine the speed with which a car can be assembled. However, when reordering the operations, one must of course ensure that changing the order does not lead to incorrect assembly. To return to the computational problem, by using the Multi-Party Session Types to describe the communication, we have a formal way of reasoning about the transformations. By developing a formal language for the transformations we can prove their correctness. This is the main novelty of the proposal: the formal system for type transformations. The actual transformations can be viewed as "programs" in this formal language. They will be informed by the properties of the computing platform. To provide this link between the transformation and the platform, we will also develop a formal description of parallel computing platforms. By building these formal systems into a compiler we will be able to transform programs to run in the most efficient way on hybrid manycore platforms. The main benefit from the proposed research is that the programmer will not need to have in-depth knowledge of the highly complex architecture of a hybrid manycore platform. This will be of great benefit to in particular scientific computing, because it also means that programs will not need to be rewritten to run with best performance on novel systems.To demonstrate the effectiveness of our approach we aim to develop a proof-of-concept compiler which will transform programs so that they can run on FPGAs, because this type of computing platform is the most different from other platforms and hence the most challenging.