Asynchronous GPU Operations

Provides async GPU compute using Lean 4's Task system.

Features

• Non-blocking shader execution
• Async buffer operations
• Task-based parallel GPU operations
• Future/promise pattern for GPU results

Usage Example

-- Launch async compute
let task ← asyncCompute shader inputBuffers

-- Do other work...
doOtherWork

-- Wait for result
let result ← task.get

structure Hesper.Async.AsyncResult (α : Type) : Type

Result of an async GPU operation

• value : α

  The computed result

• executionTimeMs : Float

  Execution time in milliseconds

def Hesper.Async.instInhabitedAsyncResult.default {a✝ : Type} [Inhabited a✝] : AsyncResult a✝

Equations

• Hesper.Async.instInhabitedAsyncResult.default = { value := default, executionTimeMs := default }

instance Hesper.Async.instInhabitedAsyncResult {a✝ : Type} [Inhabited a✝] : Inhabited (AsyncResult a✝)

Equations

• Hesper.Async.instInhabitedAsyncResult = { default := Hesper.Async.instInhabitedAsyncResult.default }

def Hesper.Async.instReprAsyncResult.repr {α✝ : Type} [Repr α✝] : AsyncResult α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Hesper.Async.instReprAsyncResult {α✝ : Type} [Repr α✝] : Repr (AsyncResult α✝)

Equations

• Hesper.Async.instReprAsyncResult = { reprPrec := Hesper.Async.instReprAsyncResult.repr }

@[reducible, inline]

abbrev Hesper.Async.AsyncTask (α : Type) : Type

Async GPU compute task

Equations

• Hesper.Async.AsyncTask α = Task (Hesper.Async.AsyncResult α)

def Hesper.Async.launchAsync {α : Type} [Inhabited α] (computation : IO (AsyncResult α)) : IO (AsyncTask α)

Helper to launch async task

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.asyncShaderExec (_shader : String) (_workgroups : Nat × Nat × Nat) [Inhabited Unit] : IO (AsyncTask Unit)

Launch async shader execution and return a Task

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.asyncBufferRead (_buffer : WebGPU.Buffer) (size : Nat) : IO (AsyncTask (Array Float))

Launch async buffer read and return a Task

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.asyncBufferWrite (_buffer : WebGPU.Buffer) (_data : Array Float) [Inhabited Unit] : IO (AsyncTask Unit)

Launch async buffer write and return a Task

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.parallel {α : Type} (tasks : Array (IO (AsyncTask α))) : IO (Array (AsyncTask α))

Execute multiple GPU tasks in parallel

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.awaitAll {α : Type} (tasks : Array (AsyncTask α)) : IO (Array (AsyncResult α))

Wait for all tasks to complete

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Async.mapTask {α β : Type} (f : α → β) (task : AsyncTask α) : AsyncTask β

Map a function over an async task result

Equations

• Hesper.Async.mapTask f task = Task.map (fun (result : Hesper.Async.AsyncResult α) => { value := f result.value, executionTimeMs := result.executionTimeMs }) task

def Hesper.Async.bindTask {α β : Type} (task : AsyncTask α) (f : α → IO (AsyncTask β)) : IO (AsyncTask β)

Bind two async tasks sequentially

Equations

• One or more equations did not get rendered due to their size.

structure Hesper.Async.AsyncPipeline (α : Type) : Type

Pipeline multiple async GPU operations

• run : IO (AsyncTask α)

  The pipeline computation

def Hesper.Async.AsyncPipeline.fromTask {α : Type} (task : IO (AsyncTask α)) : AsyncPipeline α

Create a pipeline from a single async operation

Equations

• Hesper.Async.AsyncPipeline.fromTask task = { run := task }

def Hesper.Async.AsyncPipeline.andThen {α β : Type} [Inhabited α] [Inhabited β] (p1 : AsyncPipeline α) (f : α → IO (AsyncTask β)) : AsyncPipeline β

Chain two pipeline stages

Equations

• p1.andThen f = { run := do let task1 ← p1.run Hesper.Async.bindTask task1 f }

def Hesper.Async.AsyncPipeline.map {α β : Type} (f : α → β) (p : AsyncPipeline α) : AsyncPipeline β

Map over pipeline result

Equations

• Hesper.Async.AsyncPipeline.map f p = { run := do let task ← p.run pure (Hesper.Async.mapTask f task) }

def Hesper.Async.AsyncPipeline.execute {α : Type} (p : AsyncPipeline α) : IO (AsyncResult α)

Execute the pipeline and wait for result

Equations

• p.execute = do let task ← p.run liftM (IO.wait task)

structure Hesper.Async.AsyncComputeConfig : Type

Async compute configuration

• shader : String

  Shader source code

• workgroups : Nat × Nat × Nat

  Workgroup dimensions

• inputSizes : Array Nat

  Input buffer sizes

• outputSize : Nat

  Output buffer size

def Hesper.Async.instInhabitedAsyncComputeConfig.default : AsyncComputeConfig

Equations

• Hesper.Async.instInhabitedAsyncComputeConfig.default = { shader := default, workgroups := default, inputSizes := default, outputSize := default }

instance Hesper.Async.instInhabitedAsyncComputeConfig : Inhabited AsyncComputeConfig

Equations

• Hesper.Async.instInhabitedAsyncComputeConfig = { default := Hesper.Async.instInhabitedAsyncComputeConfig.default }

def Hesper.Async.instReprAsyncComputeConfig.repr : AsyncComputeConfig → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Hesper.Async.instReprAsyncComputeConfig : Repr AsyncComputeConfig

Equations

• Hesper.Async.instReprAsyncComputeConfig = { reprPrec := Hesper.Async.instReprAsyncComputeConfig.repr }

def Hesper.Async.asyncCompute (config : AsyncComputeConfig) (_inputs : Array (Array Float)) : IO (AsyncTask (Array Float))

Launch async compute operation

Equations

• One or more equations did not get rendered due to their size.

structure Hesper.Async.BatchConfig (α : Type) : Type

Batch async operations

• operations : Array (IO (AsyncTask α))

  Operations to execute

• maxConcurrency : Nat

  Maximum concurrent tasks

def Hesper.Async.executeBatch {α : Type} (config : BatchConfig α) : IO (Array (AsyncResult α))

Execute operations in batches with concurrency limit

Equations

• One or more equations did not get rendered due to their size.

inductive Hesper.Async.TaskPriority : Type

Priority for async tasks (currently just documentation in Lean 4)

• low : TaskPriority
• normal : TaskPriority
• high : TaskPriority

def Hesper.Async.instInhabitedTaskPriority.default : TaskPriority

Equations

• Hesper.Async.instInhabitedTaskPriority.default = Hesper.Async.TaskPriority.low

instance Hesper.Async.instInhabitedTaskPriority : Inhabited TaskPriority

Equations

• Hesper.Async.instInhabitedTaskPriority = { default := Hesper.Async.instInhabitedTaskPriority.default }

instance Hesper.Async.instReprTaskPriority : Repr TaskPriority

Equations

• Hesper.Async.instReprTaskPriority = { reprPrec := Hesper.Async.instReprTaskPriority.repr }

def Hesper.Async.instReprTaskPriority.repr : TaskPriority → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.