Heterogeneous metaprogramming is using a generally higher-level host language to generate code in a lower-lever object language. Its appeal is taking advantage of the module system, higher-order functions, data types, type system and verification tools of the host language to quicker produce high-performant lower-level code with some correctness guarantees.
We present two heterogeneous programming systems whose host language is OCaml and object language is C. The first relies on offshoring: treating a subset of (MetaOCaml-generated) OCaml as a different notation for (a subset of) C. The second embeds C in OCaml in tagless-final style. The systems have been used in several projects, including the generation of C supersets OpenCL and OpenMP.
Generating C with some correctness guarantees is far less trivial than it may appear, with pitfalls abound. Not coincidentally, the most subtle ones accompany the introduction of variables into the code. Maintaining the offshoring system has traps of its own. We expound the pitfalls we have came across in our experience, and describe counter-measures.
Wed 11 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
22:00 - 22:50 | |||
22:00 25mTalk | Generating C: System Description FLOPS 2022 Oleg Kiselyov Tohoku University | ||
22:25 25mTalk | Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform FLOPS 2022 |