Reliable Many-Core Programming

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

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.