2.5. Close a span only after asynchronous work finishes🔗

An ordinary span stops when its host action returns. That is correct for synchronous work, but a GPU launch or foreign runtime may return while the measured operation is still running. SpanHooks makes the completion rule explicit:

prepare
  start timestamp
    action
    completeTiming
  stop timestamp
enrich
record event

prepare creates adapter state outside the timed interval. completeTiming waits for the work whose completion defines the measurement. enrich runs after the stop timestamp and can attach counters without adding their collection cost to the duration.

let hooks : SpanHooks := {
  State := DeviceToken
  prepare := makeTimingToken
  completeTiming := waitForDevice
  enrich := fun token metadata => do
    let live ← readLiveBytes token
    pure { metadata with allocLiveBytes := some live }
}

span "model.forward" forward
  (metadata := {
    device := some "cuda"
    timing := some "device-synchronized"
  })
  (hooks := hooks)

This span measures the host launch path, queue delay, required device work, and synchronization overhead as one interval. It does not reveal individual kernels or memory copies. CUPTI, Kineto, or a native device profiler is still needed for that lower-level timeline.

Errors from completeTiming and enrich are written to metadata.hookError. They do not replace an exception raised by forward. An error from prepare occurs before the event is reserved and returns directly to the caller.