CUDA Float32 Buffers #
Low-level buffer operations for the native CUDA autograd runtime. CUDA builds use
csrc/cuda/tensor/torchlean_cuda_tensor.cu; ordinary CPU builds link the parity implementation in
csrc/cuda/tensor/torchlean_cuda_tensor_stub.c so that the same runtime interfaces remain testable.
Runtime Availability #
What implementation sits behind the CUDA FFI symbols in the current process.
- cpuStub : RuntimeStatus
Default non-CUDA builds provide host-memory parity stubs for low-level tests.
- nativeAvailable : RuntimeStatus
The project was built with CUDA and at least one CUDA device is visible.
Instances For
Instances For
Query whether the linked CUDA symbols are native or the CPU parity stubs.
Instances For
Require real CUDA execution for a user-selected CUDA session.
Instances For
Deterministic Reductions Mode #
TorchLean's CUDA runtime uses atomicAdd in a few kernels to accumulate float32 results. This is
fast, but floating-point addition is non-associative, and CUDA does not fix a global order for the
interleaving of atomic updates. As a result, some kernels can be bit-nondeterministic across runs.
TorchLean therefore exposes an opt-in deterministic mode that replaces those atomic accumulation paths with fixed-order reductions. This trades performance for reproducibility.
This flag is a runtime setting affecting only the CUDA/stub backends; it has no effect on the pure Lean Spec.
Enable/disable deterministic reductions mode as an IO action.
The native setter runs at this point in IO and reports the resulting setting. Checking that value
both verifies the request and keeps the native effect attached to the action. Throws if the runtime
reports a different setting.
Instances For
Query whether deterministic reductions mode is enabled.
The read runs inside IO, so each call observes the current setting. A pure definition could retain
the value read during module initialization even after setDeterministicReductions changes it.
Instances For
Allocator Telemetry #
Snapshot of the CUDA buffer allocator.
liveBytes/peakBytes count device or stub payloads allocated by this runtime layer. The wrapper
counters track Lean external buffer objects, including empty wrappers and wrappers whose payloads
were explicitly released. In a steady workload, wrapperAllocCount - wrapperFinalizeCount should
remain bounded. deviceFreeBytes and deviceTotalBytes come from cudaMemGetInfo in the CUDA
build and are 0 in the CPU stub. Together these fields distinguish payload leaks, wrapper-lifetime
leaks, and broader CUDA memory pressure or fragmentation.
allocCount and freeCount count buffer payload lifetimes, including reuse. They do not count
calls to cudaMalloc and cudaFree. Live kernel workspace is outside these payload counters.
cacheBytes counts unused tensor buffers and kernel workspaces retained for reuse. Their combined
budget is cacheCapBytes, which defaults to 1 GiB. TORCHLEAN_CUDA_CACHE_CAP_BYTES can override
that budget; an explicit 0 selects unbounded caching, and invalid values use the default. Both
cache fields are 0 in the CPU stub, which keeps no cache.
The fields are read separately. A snapshot can include concurrent allocator activity and should not be treated as an atomic account of every allocation in the process.
- liveBytes : UInt64
- peakBytes : UInt64
- allocCount : UInt64
- freeCount : UInt64
- wrapperLiveCount : UInt64
- wrapperPeakCount : UInt64
- wrapperAllocCount : UInt64
- wrapperFinalizeCount : UInt64
- deviceFreeBytes : UInt64
- deviceTotalBytes : UInt64
- cacheBytes : UInt64
- cacheCapBytes : UInt64
Instances For
Instances For
Read the current CUDA allocator counters.
Each read is sequenced at this point in IO, including repeated calls in a loop. The native reads
stay inside the action rather than constructing a record that Lean could retain from an earlier
call. Applications do not need a step counter or another changing argument to obtain fresh values.
Instances For
One-line allocator report for progress logs.
A zero cache cap is printed as 0: it means unbounded caching in a CUDA build and no cache in the
CPU stub.
Instances For
Create a device buffer by copying from a host FloatArray (casts each element to float32).
This primitive has a pure Lean type, but the native implementation allocates a fresh device buffer.
Runtime code should use ofFloatArrayIO: each call allocates a distinct buffer, and ordinary device
exhaustion is returned as an IO error that the caller can handle.
Copy a host FloatArray into a fresh device buffer, rounding each element to float32.
The upload runs at this point in the IO sequence. Repeated calls with the same host array allocate
distinct buffers, so releasing one does not invalidate another. If device allocation fails, the
allocator releases unused cached blocks and retries; a second OOM throws
IO.Error.resourceExhausted. The host array and existing device buffers remain owned by the caller.
Copy a buffer back to a host FloatArray (casts float32 elements to Float).
Download a buffer to the host, widening each element to Lean Float.
Copy a buffer to its raw float32 byte representation.
This is primarily used by streaming checkpoints. Unlike toFloatArrayIO, it does not widen every
element to Lean Float, so a large CUDA parameter can be written without constructing a second
double-precision host array.
Upload a raw float32 byte payload to a fresh device buffer.
Checkpoint values retain their float32 representation. Device allocation uses the same cache
reclamation and retry as zerosIO; ordinary device exhaustion throws IO.Error.resourceExhausted
before a buffer is returned. The borrowed byte payload remains available to the caller.
Encode a host FloatArray as raw float32 bytes.
Decode raw float32 bytes into a host FloatArray.
Number of float32 elements in the buffer.
Effectfully release a device allocation owned by a completed runtime scope.
The changing token makes the release depend on the surrounding IO sequence. Buffer values are
copyable Lean references to one native allocation, so release invalidates every raw alias and Lean's
type system does not establish unique ownership. Callers must enforce that no alias remains usable;
removing one cache reference is insufficient when a tape still retains the same buffer. Parameter
mirrors and their recorded snapshots therefore use ordinary Lean reference counting. Pure CUDA
formulas that retire an owned intermediate use releaseThen, which threads cleanup through the
returned buffer.
Instances For
Release workspace and return keep.
This exists for pure CUDA tape code: because the returned buffer is used downstream, Lean cannot erase the native release call as dead code.
Release a collection of workspace buffers and return keep.
Many CUDA tape formulas create a group of intermediate buffers, then continue with one final result buffer. Threading cleanup through the result keeps ownership local to the formula and avoids waiting for external-object finalizers in long training loops.
Instances For
A CUDA result together with workspace buffers that were needed to compute it.
This is the common ownership shape for eager CUDA formulas. Some forward computations need intermediate buffers again during the backward pass, so the tape keeps those buffers on the node and releases them when the node is retired. Backward formulas use the same shape when they recompute a value only to differentiate through it.
- value : Buffer
Instances For
Return keep after releasing all workspace buffers owned by this result.
Instances For
Return keep after releasing both the result buffer and its workspace buffers.
Instances For
Collect unused host allocator pages while retaining CUDA buffers for reuse.
Training and evaluation call this after retiring a completed tape and its temporary gradients. The native cache budget bounds retained device memory, so ordinary callers do not need to flush the cache between updates. Live parameters and optimizer state remain owned by their sessions.
Instances For
Return all unused tensor buffers and kernel workspaces to the CUDA driver.
This explicit operation waits for cached blocks to become safe to free and also asks the host allocator to release unused pages. It does not release live tensors, parameter mirrors, or optimizer state. Normal training retains a bounded cache automatically; use this when returning unused memory to another workload matters more than keeping it for the next operation.
Every invocation performs a fresh collection, including calls after an earlier flush. The raw call
stays inside the IO action so repeated requests cannot share a previously computed result.
Instances For
Allocate a length-n buffer filled with zeros.
Allocate a fresh zero-filled buffer inside IO code.
The allocation runs at this point in the IO sequence. If device memory is exhausted, the native
allocator first releases unused cached blocks and retries. A second device OOM throws
IO.Error.resourceExhausted, so a caller can release its own temporary buffers and try a smaller
allocation. Existing live buffers remain owned by their callers, and a failed allocation adds no
live buffer to the counters.
The allocating IO constructors share this recovery behavior. Pure allocation and kernel primitives retain their native failure policy. Host allocation failure and errors encountered while flushing an invalid CUDA context are outside this recovery path.
Allocate a fresh length-n buffer filled with v, rounded to float32.
Each call owns a distinct buffer. Device allocation follows the cache reclamation and retry used
by zerosIO, and ordinary device exhaustion throws IO.Error.resourceExhausted.
Deterministic RNG (device-side) #
These are low-level building blocks used by TorchLean's seeded RNG ops (rand_uniform,
bernoulli_mask) when running on the eager CUDA backend.
They use the same SplitMix64-style mixing as TorchLean.Random so results are
deterministic given (seed, counter) and a row-major linear index.
Deterministic U[0,1) generator: returns a length-n buffer (float32) keyed by key.
Generate the deterministic values of randUniform in a fresh buffer.
The key determines the values; repeated calls still allocate distinct buffers. Device allocation
uses the recovery behavior of zerosIO, including IO.Error.resourceExhausted on ordinary OOM.
Generate the deterministic mask of bernoulliMask in a fresh buffer.
The probability and key retain the pure primitive's meaning. Each call allocates independently,
using the cache reclamation, retry, and ordinary device-OOM error of zerosIO.
Absolute value applied pointwise to a CUDA buffer.
Backward for abs: dx = sign(x) * dLdy (with sign(0)=0).
Elementwise sqrt (max x 0), matching Tensor.sqrtSpec.
Negative inputs and either signed zero return positive zero. NaN inputs remain NaN; the clamp uses the same ordered comparison as the floating-point maximum in the tensor spec.
Backward for sqrt.
Uses the TorchLean convention: dx = dLdy * (1 / (2*sqrt(x))) for x > 0, else 0.
Elementwise exp.
Elementwise sine of angles in radians, returning a new float32 buffer.
The native implementation applies sinf to each entry. The input is borrowed, so the tape can
retain it for the cosine factor in the backward pass.
Elementwise cosine of angles in radians, returning a new float32 buffer and borrowing its input.
Elementwise natural logarithm.
Reciprocal: 1/x.
Pointwise maximum of two equal-length CUDA buffers.
Elementwise minimum of two buffers.
Pointwise division of two equal-length CUDA buffers.
Pointwise ReLU activation on a CUDA buffer.
Backward for relu: dx = dLdy where x > 0, else 0.
Tanh-approximate GELU evaluated by one pointwise CUDA kernel.
Backward for tanh-approximate GELU using Activation.geluDerivSpec.
Elementwise addition (sizes must match).
Elementwise subtraction (sizes must match).
Elementwise multiplication (sizes must match).
Device-to-device copy, implemented as a scale-by-one kernel.
Instances For
Copy a buffer and release the source after the copy has been produced.
The native operation creates the destination before it retires the source, so the compiler cannot reorder the two lifetime events. Use this at ownership-transfer boundaries in the sparse CUDA tape.
Perform one Adam-family update in a single CUDA pass.
The result is (parameters, firstMoment, secondMoment). Passing decay = 0 gives Adam; passing
decay = -(learningRate * weightDecay) gives AdamW's decoupled parameter decay. The caller
computes the two bias-correction scales from the step counter, exactly as in Optim.Adam.update
and Optim.AdamW.update.
This primitive changes only the execution plan. TorchLean's optimizer definitions remain the semantic reference, while this native boundary avoids materializing every intermediate tensor in the pointwise update.
Scaled product exponential: exp((c * x) * y), a single fused device kernel with one launch and
one result buffer instead of the four elementwise ops (full c, two muls, exp) of the
composed form, and bit-identical to it (same left-association, same fp32 rounding). c is a host
Float (cast to float32); x and y are equal-length buffers.
Domain-neutral: a scaled product exponential recurs across the sciences: a Beer–Lambert /
propagation two-way extinction exp(-2 * κ * ℓ) in computational electromagnetism and radar/optical
remote sensing, or a Boltzmann-type weight exp(-β * E * s). Fusing the exponential with its scaled
product is the hot inner form in those forward models.
Reductions (return a length-1 buffer).
Mean of all elements, returned as a one-element buffer.