Sarek_execute.Soa_launchAn argument to run_soa: either a regular Execute.vector_arg, or a SoA custom vector (lowered in place to its N leaf base pointers + shared length).
val kernel_params_info :
Sarek_ir_types.kernel ->
(string * Sarek_ir_types.elttype option) listThe kernel's DParams as (name, array element type), in declaration order. ONE source of positional truth: run_soa aligns args with this list by index, both to name the SoA params and to validate their layout, so the two must not be derived by separate traversals that could disagree.
val kernel_param_names : Sarek_ir_types.kernel -> string listNames of the kernel's DParams, in declaration order.
val describe_leaf : Spoc_core.Soa.leaf -> stringval describe_leaves : Spoc_core.Soa.leaf list -> stringval check_soa_layout :
param:string ->
kernel_ty:Sarek_ir_types.elttype option ->
declared:Spoc_core.Soa.plan ->
unitval rs_args_of_reg_vector :
('a, 'b) Spoc_core.Vector.t ->
Spoc_core.Device.t ->
Spoc_framework.Framework_sig.run_source_arg listrun_source_args for one regular vector: (buffer, length).
val rs_args_of_soa_vector :
'a Spoc_core.Soa_vector.t ->
Spoc_core.Device.t ->
Spoc_framework.Framework_sig.run_source_arg listrun_source_args for a SoA vector: N leaf base pointers (leaf order) followed by one shared RSA_Vector_Length.
val rs_args_of_reg :
Execute.vector_arg ->
Spoc_core.Device.t ->
Spoc_framework.Framework_sig.run_source_arg listval run_soa :
device:Spoc_core.Device.t ->
ir:Sarek_ir_types.kernel ->
args:soa_arg list ->
block:Spoc_framework.Framework_sig.dims ->
grid:Spoc_framework.Framework_sig.dims ->
?shared_mem:int ->
unit ->
unitExecute a kernel with SoA-lowered custom-vector arguments.
Host coherence contract. The AoS host buffer of each SoA vector is the source of truth. run_soa calls Spoc_core.Soa_vector.scatter internally (AoS host -> per-leaf host -> device) immediately before launch, so there is no user-visible window between scatter and launch and host sets made before the call are always reflected on the device. For a kernel that only reads SoA leaves nothing more is needed. For a kernel that writes an SoA leaf, the device-side leaf buffers become authoritative; to observe the result through the AoS vector the caller must round-trip explicitly: transfer each leaf back to the host (e.g. Spoc_core.Transfer.to_cpu on every Spoc_core.Soa_vector.leaves entry — run_soa marks them stale so this triggers a D2H copy) and then call Spoc_core.Soa_vector.gather (per-leaf host -> AoS host). run_soa never gathers automatically.
It does not synchronize either: it returns once the launch is QUEUED. Today every backend issues the launch and the D2H that Spoc_core.Transfer.to_cpu performs on the same (default) stream, so they are already ordered by ordinary same-stream FIFO, which every driver promises; that is not a legacy-vs-per-thread-default-stream distinction, and this contract does not promise that placement will hold — drain the device (e.g. Spoc_core.Transfer.flush) before the read-back rather than resting on it.
This same hazard — a caller reading back before the device has actually finished — is not specific to run_soa: Execute.run_vectors and Execute.run_source reach the same CUDA path (a bare launch on the default stream, no drain), and neither documents an obligation to synchronize before reading results back. This docstring covers only run_soa's contract; it makes no claim about those two entry points one way or the other.