Reliable Many-Core Programming

可靠的多核编程

• 批准号: EP/N026314/1
• 负责人: Alastair Donaldson
• 金额: $ 128.15万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2016
• 资助国家: 英国
• 起止时间: 2016 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FN026314%2F1
• 关键词: Reliable; Many; Core; Programming

The computational demands of modern computer applications make thepursuit of high performance more critical than ever, and mobile,battery-powered devices, as well as concerns related to climatechange, require high performance to co-exist with energy-efficiency.Due to physical limits, the traditional means for improving hardwareperformance by increasing processor frequency now carries anunacceptably high energy cost. Advances in processor fabricationtechnology instead allow the construction of many-core processors,where hundreds or thousands of processing elements are placed on asingle chip, promising high performance and energy-efficiency throughsheer volume of processing elements.Many-core devices are present in practically all consumer devices,including smartphones and tablets. As a result, the general public indeveloped countries interact with many-core software daily. Many-coretechnology is also used to accelerate safety-critical software indomains such as medical imaging and autonomous vehicle navigation.It is thus important that many-core software should be reliable. Thisrequires reliable software from programmers, but also a reliable"stack" to support this software, including compilers that allowsoftware to execute on many-core devices, and the many-core devicesthemselves. Recent work on formal verification and testing by myselfand other researchers has identified serious technical problemsspanning the many-core stack. These problems undermine confidence inapplications of many-core technology: defective many-core softwarecould risk fatal accidents in critical domains, and impact negativelyon users in other important application areas.My long-term vision is that the reliability of many-core programmingcan be transformed through breakthroughs in programming languagespecification, formal verification and test case generation, enablingautomated tools to assist programmers and platform vendors inconstructing reliable many-core applications and languageimplementations. The aim of this five-year Fellowship is to undertakefoundational research to investigate a number of open problems whosesolution is key to enabling this long-term vision.First, I seek to investigate whether it is possible to preciselyexpress the intricacies of many-core programming language using formalmathematics, providing a rigorous basis on which software and languageimplementations can be constructed.Second, I aim to tackle several open problems that stand in the way ofeffective formal verification of many-core software, which would allowdevelopers to obtain strong guarantees that such software will operateas required.Third, I will investigate raising this level of rigour beyondmany-core languages. A growing trend is for applications to be writtenin relatively simple, high-level representations, and thenautomatically translated into high-performance many-core code. Thistranslation process must preserve the meaning of programs; I willinvestigate methods for formally certifying that it does.Fourth, I will formulate new methods for testing many-core languageimplementations, exploiting the rigorous language definitions broughtby my approach to enable high test coverage of subtle languagefeatures.Collectively, progress on these problems promises to enable a*high-assurance* many-core stack. I will demonstrate one instance ofsuch a stack for the industry-standard OpenCL language and the PENCILhigh-level language, showing that high-level PENCIL programs can bereliably compiled into rigorously-defined OpenCL, integrated withverified library components, and deployed on thoroughly testedimplementations from many-core vendors.Partnership with four leading many-core technology vendors, AMD, ARM,Imagination Technologies and NVIDIA, provides excellent opportunitiesfor the advances the Fellowship makes to have broad industrial impact.

现代计算机应用的计算需求使得对高性能的追求比以往任何时候都更加重要，而移动的电池供电设备以及与气候变化相关的问题都要求高性能与能效共存。由于物理限制，通过提高处理器频率来提高硬件性能的传统方法现在带来了不可接受的高能耗成本。相反，处理器制造技术的进步允许构建众核处理器，其中数百或数千个处理元件被放置在单个芯片上，通过处理元件的体积来保证高性能和能源效率。众核设备几乎存在于所有消费设备中，包括智能手机和平板电脑。因此，发达国家的公众每天都在与众核软件互动。众核技术也被用于加速医学成像和自动车辆导航等领域的安全关键软件。因此，众核软件的可靠性至关重要。这需要程序员提供可靠的软件，但也需要一个可靠的“堆栈”来支持这些软件，包括允许软件在众核设备上执行的编译器，以及众核设备本身。最近我和其他研究人员在形式验证和测试方面的工作已经确定了许多核心堆栈中的严重技术问题。这些问题削弱了对众核技术应用的信心：有缺陷的众核软件可能会在关键领域发生致命事故，并对其他重要应用领域的用户产生负面影响。我的长期愿景是，众核编程的可靠性可以通过编程语言规范、形式化验证和测试用例生成方面的突破来转变，启用自动化工具，以帮助程序员和平台供应商构建可靠的众核应用程序和语言实现。这个为期五年的奖学金的目的是进行基础研究，以调查一些开放的问题，这些问题的解决方案是实现这一长期愿景的关键。首先，我试图调查是否有可能使用形式数学精确地表达众核编程语言的复杂性，为软件和语言实现提供严格的基础。其次，我的目标是解决几个公开的问题，这些问题阻碍了对众核软件进行有效的形式化验证，这将使开发人员能够获得这样的软件将按要求运行的强有力的保证。第三，我将研究如何将这种严格性提高到超越众核语言的水平。一个日益增长的趋势是应用程序以相对简单的高级表示形式编写，然后自动转换为高性能的众核代码。这个翻译过程必须保留程序的含义;我将研究方法来正式证明它确实如此。第四，我将制定新的方法来测试众核语言实现，利用我的方法带来的严格的语言定义来实现对微妙语言特性的高测试覆盖率。总的来说，这些问题的进展有望实现一个 * 高保证 * 的众核堆栈。我将展示一个这样的堆栈的一个例子，用于行业标准的OpenCL语言和PENCIL高级语言，表明高级PENCIL程序可以可靠地编译成严格定义的OpenCL，与经过验证的库组件集成，并部署在来自众核供应商的经过全面测试的实现上。与四个领先的众核技术供应商，AMD，ARM，Imagination Technologies和NVIDIA的合作伙伴关系，为奖学金的进步提供了极好的机会，以产生广泛的工业影响。

项目成果

GPU schedulers: how fair is fair enough?

GPU 调度程序：多公平才算公平？

• DOI: 10.4230/lipics.concur.2018.23
• 发表时间: 2018
• 作者: Sorensen T

Automated testing of graphics shader compilers

• DOI: 10.1145/3133917
• 发表时间: 2017-10
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Alastair F. Donaldson;Hugues Evrard;Andrei Lascu;Paul Thomson

Floating-point symbolic execution: A case study in N-version programming

• DOI: 10.1109/ase.2017.8115670
• 发表时间: 2017-10
• 期刊: 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
• 作者: D. Liew;Daniel Schemmel;Cristian Cadar;Alastair F. Donaldson;Rafael Zähl;Klaus Wehrle

Dynamic race detection for C++11

C 11 的动态竞争检测

• 发表时间: 2017
• 作者: Lidbury C

Cooperative kernels: GPU multitasking for blocking algorithms

协作内核：用于阻塞算法的 GPU 多任务处理

• DOI: 10.1145/3106237.3106265
• 发表时间: 2017
• 作者: Sorensen T