Preserving provability over GPU program optimizations with annotation-aware transformations

Area of Science:

• Computer Science
• Software Engineering
• High-Performance Computing

Background:

• GPU programs require manual optimization for performance, which can introduce errors.
• Annotations (pre- and postconditions) capture functional properties but are difficult to maintain during optimization.

Purpose of the Study:

• To present an approach for automatically optimizing GPU programs while preserving their provability.
• To introduce annotation-aware transformations that modify both code and annotations.

Main Methods:

• Developed annotation-aware transformations to apply GPU optimizations.
• Implemented the approach in the Alpinist tool.
• Evaluated Alpinist with the VerCors program verifier on verified programs.

Main Results:

• Demonstrated the ability to automatically apply optimizations to GPU programs.
• Showcased the preservation of provability through transformed annotations.
• Successfully reverified optimized programs using Alpinist and VerCors.

Conclusions:

• Annotation-aware transformations offer an automated solution for optimizing GPU programs.
• This approach reduces the labor and error-proneness associated with manual optimization and annotation maintenance.
• Alpinist facilitates the development of correct and performant GPU software.