browser.gpu

For work run on a GPU: a device held by a with, buffers on it held by withs of their own, written and read, a kernel loaded from its code, and a kernel dispatched over a grid of workgroups with buffers bound. Each operation’s answer goes to its continuation, as std.filesystem’s do, since a GPU finishes later: a dispatch’s continuation is called when the GPU is done with it. Import it by a name, import browser.gpu as GPU.

The first provider is WebGPU’s (a page’s): a kernel is WGSL, its buffers bound at @group(0), the first at @binding(0), the next at @binding(1). Native ones (Vulkan, Metal, CUDA’s driver API) are to come with the C backend.

A device, a buffer and a pipeline are the host’s own things, foreign values. The device is had by withDevice, at the top of a program (it lives as long as the program draws), a buffer by withBuffer inside it, each a With in a region of its own, so that neither leaves the body that has it: the device is closed, the buffer let go of, when its body ends. A pipeline is the device’s: load gives it as a value, there is nothing to let go of (WebGPU frees it with its device), and it is dispatched anywhere in the device’s body — given to a device that is closed, the host refuses it. The buffers bound to a dispatch are each in a region of their own, so a dispatch takes them one by one, dispatch1 to dispatch3, as browser.gpu.kernel’s kernels are of one to three. An operation that fails gives a value, an Either GpuError a, with what the host says of it: a buffer too large, a kernel’s code that does not compile (its messages, each with its line). A device not opened, a buffer not made, is no answer of the body its with runs, so it is thrown, over the exception effect: no GPU here, say — a browser without WebGPU throws its GpuError at withDevice.

browser.gpu.canvas shows a buffer on a <canvas>; browser.gpu.kernel writes a kernel in heff, not as WGSL text, browser.gpu.wgsl prints it, and browser.gpu.run runs it with typed buffers. heff’s pages examples have vecadd, adding two vectors on the GPU, and pixels, drawing a gradient.

Device

data Device

A GPU opened: the host’s own, had as a With s Device by withDevice’s body.

Buffer

data Buffer

A buffer of bytes on a GPU, a kernel’s storage: the host’s own, had as a With s Buffer by withBuffer’s body.

Pipeline

data Pipeline

A kernel loaded on a GPU, ready to be dispatched: the device’s, as long as the device is.

GpuError

type GpuError = { message : String }

Why an operation failed, as the host says it.

instanceShowGpuError

instance instanceShowGpuError : Show GpuError

As the host says it.

>>> show ({ message = "WebGPU is not here" } : GpuError)
"gpu: WebGPU is not here"

GpuF

data GpuF (m : Type -> Type) x
  = Open (Either GpuError Device -> x)
  | Close Device (Either GpuError Unit -> x)
  | NewBuffer Device Int (Either GpuError Buffer -> x)
  | FreeBuffer Buffer (Either GpuError Unit -> x)
  | WriteBuffer Device Buffer Int Bytes (Either GpuError Unit -> x)
  | ReadBuffer Device Buffer Int Int (Either GpuError Bytes -> x)
  | Load Device String String (Either GpuError Pipeline -> x)
  | Dispatch Device Pipeline (List Buffer) Int Int Int (Either GpuError Unit
                                                        -> x)

gpu

gpu : HFunctor

For work run on a GPU: a device opened, buffers made, written and read back, kernels loaded and dispatched over them.

withDevice

withDevice : {e : HFunctor}
           -> {a : Type}
           -> {{ev : gpu <: e}}
           -> {{cu : Custodian.custodian <: e}}
           -> {{ex : exception GpuError <: e}}
           -> ({s : Type} -> With s Device -> Co e a)
           -> Co e a

The GPU opened, held by body in a region of its own, and closed when body ends: what it came to; where there is no GPU here, why is thrown, a GpuError. A program opens its device once, at the top, and draws inside.

withBuffer

withBuffer : {e : HFunctor}
           -> {s a : Type}
           -> {{ev : gpu <: e}}
           -> {{cu : Custodian.custodian <: e}}
           -> {{ex : exception GpuError <: e}}
           -> With s Device
           -> Int
           -> ({t : Type} -> With t Buffer -> Co e a)
           -> Co e a

A buffer of n bytes on the device, 0 each, which a kernel reads and writes and which is written and read from the program: held by body in a region of its own, and let go of when body ends; a buffer not made (too large, say) is thrown, a GpuError.

writeBuffer

writeBuffer : {e : HFunctor}
            -> {s t : Type}
            -> {{ev : gpu <: e}}
            -> With s Device
            -> With t Buffer
            -> Int
            -> Bytes
            -> Co e (Either GpuError Unit)

The bytes written into the buffer from its byte at (a multiple of 4, as their length is).

readBuffer

readBuffer : {e : HFunctor}
           -> {s t : Type}
           -> {{ev : gpu <: e}}
           -> With s Device
           -> With t Buffer
           -> Int
           -> Int
           -> Co e (Either GpuError Bytes)

The buffer’s n bytes from its byte at (multiples of 4), read once what the GPU was given to do before is done.

load

load : {e : HFunctor}
     -> {s : Type}
     -> {{ev : gpu <: e}}
     -> With s Device
     -> String
     -> String
     -> Co e (Either GpuError Pipeline)

A kernel loaded from its code (WGSL, for WebGPU) and the name of its entry point, or what the compiler said of the code. The pipeline is the device’s: dispatched as long as the device is open.

dispatch1

dispatch1 : {e : HFunctor}
          -> {s t : Type}
          -> {{ev : gpu <: e}}
          -> With s Device
          -> Pipeline
          -> With t Buffer
          -> Int
          -> Int
          -> Int
          -> Co e (Either GpuError Unit)

The kernel run over x by y by z workgroups, its one buffer bound at @binding(0): done when the GPU is.

dispatch2

dispatch2 : {e : HFunctor}
          -> {s t u : Type}
          -> {{ev : gpu <: e}}
          -> With s Device
          -> Pipeline
          -> With t Buffer
          -> With u Buffer
          -> Int
          -> Int
          -> Int
          -> Co e (Either GpuError Unit)

… its two buffers bound in order (the first at @binding(0)).

dispatch3

dispatch3 : {e : HFunctor}
          -> {s t u v : Type}
          -> {{ev : gpu <: e}}
          -> With s Device
          -> Pipeline
          -> With t Buffer
          -> With u Buffer
          -> With v Buffer
          -> Int
          -> Int
          -> Int
          -> Co e (Either GpuError Unit)

… its three buffers bound in order.