Synthesizing Code for GPGPUs from abstract formal models

• Today multiple frameworks exist for elevating the task of writing programs for GPGPUs, which are massively data-parallel execution platforms. These are needed as writing correct and high-performing applications for GPGPUs is notoriously difficult due to the intricacies of the underlying architecture. However, the existing frameworks lack a formal foundation that makes them difficult to use together with formal verification, testing, and design space exploration. We present in this chapter a novel software synthesis tool—called f2cc—which is capable of generating efficient GPGPU code from abstract formal models based on the synchronous model of computation. These models can be built using high-level modeling methodologies that hide low-level architecture details from the developer. The correctness of the tool has been experimentally validated on models derived from two applications. The experiments also demonstrate that the synthesized GPGPU code yielded a 28× speedup when executed on a graphics card with 96 cores and compared against a sequential version that uses only the CPU.

Ämnesord

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering (hsv//eng)

Nyckelord

Architectural design

Codes (symbols)

Computational linguistics

Program processors

Systems analysis

Design space exploration

Formal foundation

Graphics card

High-level modeling

High-performing applications

Software synthesis

Synchronous models

Writing projects

Design

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)