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.