A Formal Model for Portable, Heterogeneous Accelerator Programming
summary
A formal core language called H-IMP models execution spaces (host, OpenMP, CUDA) and memory spaces (host, CUDA, UVM) with an accessibility relation that records which executor can access which memory; a type system embeds the execution space into judgments and proves type safety (no heterogeneous memory or execution-capability errors) and a portability result: a portable program is one whose free exec/memory variables safely instantiate to every architecture in a given frame. Theory is mostly mechanized and a C++ static-checker is planned.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:28Cocos abstractions
- 6:01Heterogeneous safety questions
- 7:51Hemp core language
- 10:25Operational semantics
- 13:23Safety and execution errors
- 14:30Type system modalities
- 16:23Portability in Cocos
- 18:15Key takeaways
- 20:05Q&A
related talks
01h 03mPrinciples of Persistent Programming
57mInvited Talk: Bridging Safety and Performance
13mCohort: Software-Oriented Acceleration for You, Me, and Our Heterogeneous SoCs
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
32mMind the Gap: General-Purpose Programming Languages Impede Scientific Model(…)
17mFour Languages for Portability
01h 01mProgramming Abstractions for Orchestration of HPC Scientific Computing