GPU kernel generation and use?

Stream: lean4

[Geoffrey Irving]

I’m curious whether anyone has explored dispatching Lean 4 code to GPU kernels, in particular for straight line code operating on simple types used inside Array.map. It seems like one could write a quite general plugin to do this given the flexibility of the system.

[Geoffrey Irving]

Note that both the Metal and CUDA shading languages are C-based, so conceivably one could try to restrict to the mutually compatible fragment and re-use the existing code generator.

[Geoffrey Irving]

@Daniel Selsam: Do you know whether people have tried this?

[Tomas Skrivan]

A long time ago I attempted something like that, but I knew very little metaprogramming and got nowhere. I would be quite happy to try again. I'm thinking of writing bindings for CUDA Thrust library and some meta code to generate transformations and reduction kernels based on Lean code.

[Tomas Skrivan]

I'm not aware of anyone giving it a proper try.

[Tomas Skrivan]

Soon I should have backpropagation working in Lean. Generating reasonable GPU code would be really useful to properly test it out.

[Schrodinger ZHU Yifan]

I do know another project focusing on using dependently typed arrays to program GPU/CPU parallel kernels. https://github.com/google-research/dex-lang

[Daniel Selsam]

Geoffrey Irving said:

Daniel Selsam: Do you know whether people have tried this?

Hi @Geoffrey Irving! I am afraid I have no idea.