Advanced Formal Verification Techniques for Heterogeneous Multi-core Programming

异构多核处理器是解决实时医学成像、金融分析和高清视频等复杂计算问题的关键，因为它们提供了更高的处理能力。这些应用程序的可靠性和诚实性是至关重要的，但异构多核处理器是出了名的难以正确编程。需要分析和验证技术来帮助在多核软件设计的早期检测和修复错误。这些技术的发展是拟议的奖学金研究的目标。该研究将涉及扩展现有的理论计算机科学技术的能力，基于类型检查和模型检查。类型检查是一种常用的轻量级方法，用于消除计算机程序中的错误：一个基本的类型检查器将拒绝一个无效的表达式，如Hello + 1。基于会话类型的更复杂的类型检查可以允许自动检查系统中双方之间的协议。该奖学金研究的一部分将涉及扩展会话类型的概念，使其适用于异构多核处理器。新的类型检查方法亦会发展，以协助程序员处理多核心系统中因管理独立的记忆空间而引起的复杂问题。模型检查是一种验证硬件和软件系统的技术，它试图通过检查系统的抽象模型来发现系统错误。模型检查不如类型检查广泛使用，但模型检查技术最近已被纳入主要供应商（如Microsoft）的软件产品中。研究计划的其中一项主要工作，是发展先进的模型检查技术，以协助找出不同种类多核心处理器软件的动态行为所引致的错误;另一项工作则是发展一套以新颖的形式分析技术为基础的开放源码工具。经验表明，对多核编程感兴趣的开发人员不愿意采用新的语言和形式主义，并且只会考虑使用简单直观的新技术，并且可以集成到现有的开发工具链中。为了增加行业最终采用的可能性，在奖学金研究期间开发的新技术将涉及Codeplay Software Ltd.的定期投入和建议，一家专门从事多核处理器开发工具的英国公司。

Heterogeneous multi-core processors are key to complex computational problems such as real-time medical imaging, financial analysis and high-definition video, because of the increased processing power they make available. The reliability and probity of such applications is of critical importance, yet heterogeneous multi-core processors are notoriously difficult to program correctly. There is a need for analysis and verification techniques to help detect and fix errors early in the design of multi-core software. The development of such techniques is the aim of the proposed Fellowship research.The research will involve extending the capabilities of existing theoretical computer science techniques based on typechecking and model checking. Typechecking is a commonly used lightweight method for eliminating errors in computer programs: a basic typechecker will reject an invalid expression such as Hello + 1. More complex typechecking, based on session types , can allow a protocol between two parties in a system to be automatically checked. One part of the Fellowship research will involve extending the notion of session types to be applicable to heterogeneous multi-core processors. New typechecking methods will also be developed to help programmers deal with complex issues arising from the management of separate memory spaces in multi-core systems.Model checking is a technique for verifying hardware and software systems which attempts to find system bugs by checking an abstract model of the system. Model checking is less widely used than typechecking, but model checking techniques have recently been incorporated in software products from major vendors such as Microsoft. A major part of the fellowship research will involve developing advanced model checking techniques to help find errors associated with the dynamic behaviour of software for heterogeneous multi-core processors.Part of the research will involve developing a set of open-source tools based on the novel formal analysis techniques. Experience has shown that developers interested in multi-core programming are reluctant to adopt new languages and formalisms, and will only consider new techniques if they are easy and intuitive to use, and can be integrated into an existing development tool-chain. To increase the potential for eventual adoption by industry, the new techniques developed during the Fellowship research will involve regular input and advice from Codeplay Software Ltd., a UK based company specialising in development tools for multi-core processors.