Module Sarek_vulkan.Vulkan_api_device

type t = {
  1. id : int;
  2. physical_device : Vulkan_types.vk_physical_device Ctypes.structure Ctypes.ptr;
  3. device : Vulkan_types.vk_device Ctypes.structure Ctypes.ptr;
  4. compute_queue : Vulkan_types.vk_queue Ctypes.structure Ctypes.ptr;
  5. queue_family : int;
  6. instance : Vulkan_types.vk_instance Ctypes.structure Ctypes.ptr;
  7. name : string;
  8. api_version : int * int * int;
  9. memory_properties : Vulkan_types.vk_physical_device_memory_properties Ctypes.structure;
  10. command_pool : Vulkan_types.vk_command_pool;
  11. supports_fp64 : bool;
    (*

    Physical-device shaderFloat64 feature, queried via vkGetPhysicalDeviceFeatures and mirrored into the logical device's pEnabledFeatures at creation time (see get below).

    *)
  12. supports_int64 : bool;
    (*

    Physical-device shaderInt64 feature, on the same query-and-mirror path as supports_fp64. Both halves matter and only the mirroring half is easy to forget: a kernel whose SPIR-V declares OpCapability Int64 is legal only against a logical device that ENABLED the feature, so querying it without requesting it would still be the #142 defect.

    *)
  13. supports_fp16 : bool;
    (*

    VkPhysicalDeviceShaderFloat16Int8Features.shaderFloat16, queried through the VkPhysicalDeviceFeatures2 chain and REQUESTED in VkDeviceCreateInfo.pNext (backlog-62 slice 2). It is not in core VkPhysicalDeviceFeatures, which is why it could not be plumbed on the #142 path.

    docs/fp-contraction-policy.md §7(b) records that RADV accepts f16 shaders today without this feature enabled. That makes the existing f16 tripwire a measurement of an un-enabled path — fine for measuring a driver, not fine for shipping — and it is precisely the "supported but never requested" shape of #332. Enabling it here does NOT lift any f16 refusal; that is slice 3.

    *)
  14. storage_buffer_16bit : bool;
    (*

    VkPhysicalDevice16BitStorageFeatures.storageBuffer16BitAccess, queried and requested on the same chain. Required before a shader may declare 16-bit types in a storage buffer, which every f16 or cooperative-matrix kernel that reads its operands from memory must do.

    *)
  15. supports_int8 : bool;
    (*

    VkPhysicalDeviceShaderFloat16Int8Features.shaderInt8, on the same chain as supports_fp16 (backlog-62 slice 3).

    Every INTEGER cooperative-matrix configuration the local RX 7900 XTX advertises has 8-bit operands — measured, all twelve of them — so a shader that reaches coopMatMulAdd on the strict-contract path declares OpCapability Int8. Querying without requesting would be #142 verbatim.

    *)
  16. storage_buffer_8bit : bool;
    (*

    VkPhysicalDevice8BitStorageFeatures.storageBuffer8BitAccess (backlog-62 slice 3). coopMatLoad requires the backing array's element type to match the fragment's component type, so an 8-bit fragment loaded from memory declares OpCapability StorageBuffer8BitAccess. There is no route to an integer fragment that avoids it: the operand buffer cannot be widened without changing which instruction is emitted.

    *)
  17. vulkan_memory_model : bool;
    (*

    VkPhysicalDeviceVulkanMemoryModelFeatures.vulkanMemoryModel (backlog-62 slice 3). glslang makes GL_KHR_memory_scope_semantics a prerequisite of GL_KHR_cooperative_matrix, and it lowers to OpCapability VulkanMemoryModel — so this is required by the FLOAT coopmat path too, and slice 2 shipped without it.

    *)
  18. driver_id : int;
    (*

    VkPhysicalDeviceDriverProperties.driverID. 3 is VK_DRIVER_ID_MESA_RADV. This is the driver KEY that docs/fp-contraction-policy.md §11.7 and the is_anv_device comment in Test_helpers both ask for: an allowlist keyed on a device-NAME substring would match a future non-Mesa driver on the same silicon.

    *)
  19. driver_name : string;
    (*

    e.g. "radv".

    *)
  20. driver_info : string;
    (*

    e.g. "Mesa 26.1.4-arch3.1".

    *)
  21. subgroup_size : int;
    (*

    VkPhysicalDeviceSubgroupProperties.subgroupSize — the real one, not a constant. Measured 64 on the RX 7900 XTX under radv / Mesa 26.1.4-arch3.1, where Vulkan_plugin_base reported a hard-coded 32. A cooperative-matrix fragment is distributed across exactly this many invocations, so the wrong value is a wrong ABI.

    Guaranteed positive: it is fallback_subgroup_size rather than the driver's zero when the query came back unwritten, so a consumer may divide by it. subgroup_size_probed says which it is.

    *)
  22. subgroup_size_probed : bool;
    (*

    Whether subgroup_size is a measurement rather than the fallback. Both local devices are probed; a false here is a test failure, not a degradation to be tolerated.

    *)
  23. coopmat_extension_advertised : bool;
    (*

    Whether vkEnumerateDeviceExtensionProperties listed VK_KHR_cooperative_matrix for this physical device.

    *)
  24. coopmat_enabled : bool;
    (*

    Whether the extension was advertised AND VkPhysicalDeviceCooperativeMatrixFeaturesKHR.cooperativeMatrix was true, so the extension and the feature were both REQUESTED at vkCreateDevice.

    Recorded separately from coopmat rather than derived from it, because deriving it is exactly the mistake this pair exists to catch: ds_configs comes from a query that answers even for devices without the extension, so a non-empty list is NOT evidence that the device supports anything. The implication ds_configs <> [] ==> coopmat_enabled is asserted by test_vulkan_coopmat_capability, and it is what goes red if the extension check in probe_coopmat is ever removed — the gate test alone does not, because it compares the verdict against the same list.

    *)
  25. coopmat : Sarek_coopmat.device_support option;
    (*

    Cooperative-matrix support, None when it could not be probed at all (loader too old to resolve the entry point). See probe_coopmat for why an empty list and None must stay distinguishable, and for the measurement that makes the extension check load-bearing.

    *)
}
val instance_ref : Vulkan_types.vk_instance Ctypes.structure Ctypes.ptr option Stdlib.ref
val initialized : bool Stdlib.ref
val device_cache : (int, t) Stdlib.Hashtbl.t
val get_total_device_memory : Vulkan_types.vk_physical_device_memory_properties Ctypes.structure -> int64

Calculate total device memory from memory heaps

Sums all memory heaps that have VK_MEMORY_HEAP_DEVICE_LOCAL_BIT set. This gives us the actual GPU memory for discrete GPUs, or the largest device-accessible heap for integrated GPUs (which may be shared system RAM).

VK_MEMORY_HEAP_DEVICE_LOCAL_BIT = 0x00000001 per Vulkan spec.

val init : unit -> unit
val get_or_create_instance : unit -> Vulkan_types.vk_instance Ctypes.structure Ctypes.ptr

Create Vulkan instance (shared among all devices)

val count : unit -> int

Extended feature and property probes (backlog-62 slice 2)

val string_of_char_array : char Ctypes.CArray.t -> string

Read a NUL-terminated fixed-size C char array into an OCaml string.

val u32_is_true : Unsigned.UInt32.t -> bool
val zero_struct : 'a Ctypes.structure Ctypes.typ -> 'a Ctypes.structure -> unit

Zero a struct's bytes before a pNext query.

A driver that does not recognise an sType leaves the struct alone, so without this an unrecognised feature struct would be read out of uninitialised memory — and the failure direction is "feature present", on exactly the devices that lack it. ctypes' make does not zero.

val device_extension_names : Vulkan_types.vk_physical_device Ctypes.structure Ctypes_static.ptr -> string list

The device extension names a physical device advertises.

type extended_features = {
  1. ef_shader_float16 : bool;
  2. ef_shader_int8 : bool;
  3. ef_storage_buffer_16bit : bool;
  4. ef_storage_buffer_8bit : bool;
  5. ef_vulkan_memory_model : bool;
  6. ef_cooperative_matrix : bool;
  7. ef_coopmat_robust_buffer_access : bool;
}
val query_extended_features : Vulkan_types.vk_physical_device Ctypes.structure Ctypes_static.ptr -> extended_features

Query the extension feature structs in one VkPhysicalDeviceFeatures2 chain.

Chaining a struct whose extension the device does not advertise is harmless — the driver skips an sType it does not know, and zero_struct guarantees the fields then read false. What is NOT harmless is calling an extension's own entry point on such a device; see probe_coopmat.

type extended_properties = {
  1. ep_driver_id : int;
  2. ep_driver_name : string;
  3. ep_driver_info : string;
  4. ep_subgroup_size : int;
    (*

    Always positive — see fallback_subgroup_size.

    *)
  5. ep_subgroup_size_probed : bool;
    (*

    false when the driver left subgroupSize at the zero zero_struct wrote, so ep_subgroup_size is the fallback rather than a measurement.

    *)
}
val fallback_subgroup_size : int

Used only when VkPhysicalDeviceSubgroupProperties came back unwritten.

zero_struct zeroes the struct before the query, so a driver that does not recognise the sType leaves subgroupSize = 0 — and zero flowing into warp_size is worse than the wrong-but-usable 32 that preceded this work, because any consumer that divides by it faults instead of merely being wrong. 32 is that historical value, kept as the fallback for continuity and for nothing else.

It is WRONG on both devices this project measures on, which report 64 (RX 7900 XTX / RADV NAVI31 and the Ryzen 9 7950X iGPU / RADV RAPHAEL_MENDOCINO, radv / Mesa 26.1.4-arch3.1). So it must never become the silent normal: ep_subgroup_size_probed records which of the two a caller is holding, and test_vulkan_coopmat_capability asserts that every local device is PROBED — the fallback going live here is a test failure, not a quiet degradation.

val query_extended_properties : Vulkan_types.vk_physical_device Ctypes.structure Ctypes_static.ptr -> extended_properties

Driver identity and subgroup size, through one VkPhysicalDeviceProperties2 chain. Both are core Vulkan 1.1 property structs, so no extension gate.

Cooperative-matrix configuration enumeration

val component_type_of_enum : int32 -> Sarek_coopmat.component_type option
val scope_of_enum : int32 -> Sarek_coopmat.scope option
val probe_coopmat : instance:Vulkan_types.vk_instance Ctypes.structure Ctypes_static.ptr -> phys_dev:Vulkan_types.vk_physical_device Ctypes.structure Ctypes_static.ptr -> extensions:string list -> features:extended_features -> subgroup_size:int -> Sarek_coopmat.device_support option

Probe cooperative-matrix support for one physical device.

The extension check is load-bearing and this is measured, not tidy. vkGetPhysicalDeviceCooperativeMatrixPropertiesKHR is an instance-level entry point that dispatches on the physical device handle, and on this workstation RADV answers it for BOTH local devices: the AMD Ryzen 9 7950X iGPU (RADV RAPHAEL_MENDOCINO), which does not advertise VK_KHR_cooperative_matrix and reports cooperativeMatrix = false, still returns VK_SUCCESS and fourteen configurations — the same fourteen as the RX 7900 XTX. Calling an extension entry point on a device that does not support the extension is undefined behaviour, and here the undefined behaviour is a plausible, well-formed, entirely wrong answer.

So a probe that populated the configuration list from the query alone would report the iGPU as fully cooperative-matrix capable, and every gate downstream would say Available for a device that cannot execute the instruction. The order below — extension advertised, THEN feature true, THEN query — is what makes the gate able to refuse.

None is returned only when the loader cannot resolve the entry point at all; that is "not probed", and it refuses. A device that is probed and has nothing returns Some with an empty list, which is a different fact.

val find_compute_queue_family : Vulkan_types.vk_physical_device Ctypes.structure Ctypes_static.ptr -> int

Find compute queue family index

val get : int -> t
val set_current : 'a -> unit
val synchronize : t -> unit
val destroy : t -> unit