CUDA Buffers #
Low-level dtype-preserving operations for the LibTorch CUDA runtime. TorchLean retains its tape and
selected local VJPs; native calls do not record a LibTorch autograd graph. CUDA builds use
csrc/libtorch/torchlean.cpp. Builds without LibTorch link csrc/libtorch/unavailable.c, which
reports .notLinked and fails every buffer operation.
Scalar representation retained by a live native buffer. Released handles must not be read.
Complete binary format retained by an encoded buffer; native buffers return none.
Upload complete configured words without converting through a native floating-point type.
Download complete configured words, retaining signed zero and exceptional-value encodings.
Runtime Availability #
What implementation sits behind the CUDA FFI symbols in the current process.
- notLinked : RuntimeStatus
The default build does not link LibTorch; buffer operations fail.
- nativeAvailable : RuntimeStatus
The project was built with LibTorch CUDA and at least one CUDA device is visible.
Instances For
Instances For
Query whether LibTorch is linked and can see a CUDA device.
Instances For
Require real CUDA execution for a user-selected CUDA session.
Instances For
Allocator Telemetry #
Snapshot of TorchLean ownership counters and the LibTorch CUDA allocator.
liveBytes/peakBytes count logical device payloads owned by TorchLean handles. They are
not physical VRAM usage: shared tensor storage may be counted more than once, and native
temporaries or saved attention state need not have a separate TorchLean handle. allocCount and
freeCount count those payload lifetimes, not native allocation calls.
The wrapper counters track Lean external buffer objects, including empty and explicitly released wrappers. All these ownership counters are process-wide. They help distinguish retained Lean owners from storage managed internally by LibTorch.
allocatedBytes, reservedBytes, peakAllocatedBytes, and peakReservedBytes are the native
allocator's counters for the selected CUDA device. Reserved bytes include storage the allocator
retains for reuse; the difference from allocated bytes is not a promise of immediately reclaimable
memory. deviceFreeBytes and deviceTotalBytes report driver memory for that device. These six
device counters are zero when LibTorch is not linked. Native allocator peaks follow its own reset
lifecycle.
LibTorch owns caching policy. Runtime.Autograd.LibTorch.setMemoryFraction configures its
selected-device allocation
limit.
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
- allocatedBytes : UInt64
- reservedBytes : UInt64
- peakAllocatedBytes : UInt64
- peakReservedBytes : UInt64
Instances For
Instances For
Read current memory usage and buffer ownership 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 distinguishing logical payloads from native storage.
Instances For
Create a device buffer by copying from a host FloatArray in the requested dtype.
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 in the requested dtype.
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. Native allocation failures return
IO.Error.resourceExhausted; LibTorch owns the device allocator's retry policy. The host array and
existing device buffers remain owned by the caller.
Copy a buffer back to a host FloatArray, widening binary32 when needed.
Download a buffer to the host, widening each element to Lean Float.
Copy a buffer to little-endian scalar words. By default its dtype is preserved; an explicit different dtype requests conversion, as when exporting a legacy binary32 checkpoint.
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 for binary32 data.
Upload little-endian scalar words to a fresh device buffer.
source describes the payload; dtype selects storage. They agree by default. A different
source is an explicit conversion, used to load legacy binary32 files into binary64 storage.
Native allocation failures return
IO.Error.resourceExhausted before a buffer is returned. The borrowed byte payload remains
available to the caller.
Number of scalar elements in the buffer, independently of dtype.
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. LibTorch retains its reusable device cache. Live parameters and optimizer state remain owned by their sessions.
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. Native allocation failures return
IO.Error.resourceExhausted, so a caller can release its temporary buffers and try a smaller
allocation. LibTorch owns the device allocator's retry policy. 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 error boundary. Pure allocation and kernel primitives have their own native failure policy.
Allocate a length-n buffer filled with v, rounded in the requested dtype.
Allocate a fresh length-n buffer filled with v, rounded in the requested dtype.
Each call owns a distinct buffer. Native allocation failures return IO.Error.resourceExhausted,
as in zerosIO.
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 in the requested dtype, keyed by key.
Generate the deterministic values of randUniform in a fresh buffer.
The key determines the values; repeated calls still allocate distinct buffers. Native allocation
failures return IO.Error.resourceExhausted, as in zerosIO.
Deterministic normal generator using Box-Muller on the device.
Deterministic {0,1} mask generator: returns a length-n buffer keyed by key.
Generate the deterministic mask of bernoulliMask in a fresh buffer.
The probability and key retain the pure primitive's meaning. Each call allocates independently,
with the allocation error boundary 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, retaining the input dtype.
The native implementation uses at::sin. The input is borrowed, so the tape can
retain it for the cosine factor in the backward pass.
Elementwise cosine of angles in radians, retaining the input dtype and borrowing its input.
Elementwise natural logarithm.
Elementwise log(1 + x) without losing a small positive x in the addition.
Reciprocal: 1/x.
Pointwise maximum of two equal-length CUDA buffers.
Elementwise minimum of two buffers.
Pointwise quotient in the stored format; exceptional values follow that format.
Instances For
Direct negation, including the format's signed-zero convention.
Instances For
Keep values where the equal-length mask is nonzero and select zero elsewhere.
Selection discards nonfinite values in blocked entries; multiplication by the mask would not. A NaN mask is nonzero, matching the numerical backend's boolean conversion.
Pointwise ReLU activation on a CUDA buffer.
Backward for relu: dx = dLdy where x > 0, else 0.
Elementwise logistic sigmoid through at::sigmoid, retaining the input dtype.
The input is borrowed; TorchLean's tape owns the y * (1 - y) derivative. Values follow ATen's
rounding and saturation in that dtype, including zero when the negative-tail exponential overflows.
Elementwise hyperbolic tangent through at::tanh, retaining the input dtype.
Direct evaluation avoids cancellation near zero and preserves signed zero. The input is borrowed;
TorchLean's tape owns the 1 - y * y derivative.
Tanh-approximate GELU evaluated through staged ATen operations. The arithmetic ordering follows TorchLean's activation specification.
Backward for tanh-approximate GELU using Activation.geluDerivSpec.
Pointwise addition, retaining the complete configured format when present.
Instances For
Pointwise subtraction without implicit precision conversion.
Instances For
Pointwise multiplication without implicit precision conversion.
Instances For
Multiply each element by a scalar c, rounded in the buffer dtype.
This is a primitive building block for many ops (e.g. scaling gradients).
Device-to-device copy without arithmetic or precision conversion.
Two independently owned copies. Separate identical pure calls can be shared by Lean's compiler, which is unsafe when one VJP contribution is retired before the other is consumed.
Copy before retiring the source, preserving its scalar format.
Instances For
Fused multiply-add: a + c * b (sizes and dtypes must match; c is rounded in that dtype).
This is the classic BLAS-style axpy primitive and is useful for optimizers and bias-like updates.
Perform one Adam-family update through LibTorch tensor operations.
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.
The caller must validate that epsilon remains finite and positive in the parameter dtype.
The native eager optimizer and its checkpoint reader share that validation.
TorchLean's optimizer definitions specify the update. The native bridge evaluates the pointwise expressions and returns the updated parameter and moment buffers.
Scaled product exponential: exp((c * x) * y).
LibTorch evaluates the two multiplications followed by the exponential. c is a host Float
rounded in the buffer dtype; x and y have equal lengths and dtypes.
Reductions (return a length-1 buffer).
Mean of all elements, returned as a one-element buffer.