Cuda
Types
linear type ReadyBuffer a
linear type Float64Download
Functions
def num_devices (_ : Unit) : {n : Int | n > 0}
def device (id : Int | id ≥ 0 && id < num_devices unit) : {d : Device | device_id d = id && max_threads_per_block d > 0}
def default_device (_ : Unit) : {d : Device | device_id d ≥ 0 && max_threads_per_block d > 0}
def default_stream (device : Device) : {stream : Stream | stream_device stream = device_id device}
def launch_1d (device : Device) (items : Int | items > 0) (threads : Int | threads > 0 && (threads ≤ items && threads ≤ max_threads_per_block device)) : {
launch : Launch1D | launch_device launch = device_id device
&&
(
launch_items launch = items
&&
(launch_threads launch = threads && launch_grid_size launch * launch_threads launch ≥ launch_items launch)
)
}
def upload_i32 (device : Device) (1 values : Array Int | Array.size values > 0) : {
buffer : ReadyBuffer Int | buffer_device buffer = device_id device
&&
(
buffer_size buffer = Array.size values
&&
(
buffer_elem_size buffer = 4
&&
(buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer && buffer_bytes buffer ≤ max_allocation device)
)
)
}
def upload_float64 (device : Device) (1 values : Array Float | Array.size values > 0) : {
buffer : ReadyBuffer Float | buffer_device buffer = device_id device
&&
(
buffer_size buffer = Array.size values
&&
(
buffer_elem_size buffer = 8
&&
(buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer && buffer_bytes buffer ≤ max_allocation device)
)
)
}
def add_i32 (launch : Launch1D) (stream : Stream | stream_device stream = launch_device launch) (
1 left : ReadyBuffer Int | buffer_size left > 0
&&
(
buffer_elem_size left = 4
&&
(
buffer_device left = launch_device launch
&&
(buffer_size left = launch_items launch && launch_grid_size launch * launch_threads launch ≥ buffer_size left)
)
)
) (
1 right : ReadyBuffer Int | buffer_size right = buffer_size left
&&
(buffer_elem_size right = buffer_elem_size left && buffer_device right = buffer_device left)
) : {
pending : Pending Int | pending_device pending = launch_device launch
&&
(pending_size pending = launch_items launch && pending_stream pending = stream_id stream)
}
def add_float64 (launch : Launch1D) (stream : Stream | stream_device stream = launch_device launch) (
1 left : ReadyBuffer Float | buffer_size left > 0
&&
(
buffer_elem_size left = 8
&&
(
buffer_device left = launch_device launch
&&
(buffer_size left = launch_items launch && launch_grid_size launch * launch_threads launch ≥ buffer_size left)
)
)
) (
1 right : ReadyBuffer Float | buffer_size right = buffer_size left
&&
(buffer_elem_size right = buffer_elem_size left && buffer_device right = buffer_device left)
) : {
pending : Pending Float | pending_device pending = launch_device launch
&&
(pending_size pending = launch_items launch && pending_stream pending = stream_id stream)
}
def synchronize (1 pending : Pending a) : {
buffer : ReadyBuffer a | buffer_device buffer = pending_device pending
&&
(buffer_size buffer = pending_size pending && buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer)
}
def download_i32 (1 buffer : ReadyBuffer Int) : {
result : I32Download | i32_download_device result = buffer_device buffer
&&
i32_download_size result = buffer_size buffer
}
def download_float64 (1 buffer : ReadyBuffer Float) : {
result : Float64Download | float64_download_device result = buffer_device buffer
&&
float64_download_size result = buffer_size buffer
}
def unpack_i32_download (1 p : I32Download) : {
pair : I32DownloadPair | i32_download_pair_device pair = i32_download_device p
&&
i32_download_pair_size pair = i32_download_size p
}
def unpack_float64_download (1 p : Float64Download) : {
pair : Float64DownloadPair | float64_download_pair_device pair = float64_download_device p
&&
float64_download_pair_size pair = float64_download_size p
}
def download_values_i32 (p : I32DownloadPair) : {xs : Array Int | Array.size xs = i32_download_pair_size p}
def download_buffer_i32 (p : I32DownloadPair) : {
b : ReadyBuffer Int | buffer_device b = i32_download_pair_device p
&&
(
buffer_size b = i32_download_pair_size p
&&
(buffer_elem_size b = 4 && buffer_bytes b = buffer_size b * buffer_elem_size b)
)
}
def download_values_float64 (p : Float64DownloadPair) : {xs : Array Float | Array.size xs = float64_download_pair_size p}
def download_buffer_float64 (p : Float64DownloadPair) : {
b : ReadyBuffer Float | buffer_device b = float64_download_pair_device p
&&
(
buffer_size b = float64_download_pair_size p
&&
(buffer_elem_size b = 8 && buffer_bytes b = buffer_size b * buffer_elem_size b)
)
}
def free (1 buffer : ReadyBuffer a) : Unit
def discard (1 pending : Pending a) : Unit
Uninterpreted
Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.
def device_id : (d : Device) → Int
def num_devices : (_ : Unit) → Int
def max_threads_per_block : (d : Device) → Int
def max_allocation : (d : Device) → Int
def launch_device : (launch : Launch1D) → Int
def launch_items : (launch : Launch1D) → Int
def launch_threads : (launch : Launch1D) → Int
def launch_grid_size : (launch : Launch1D) → Int
def stream_device : (stream : Stream) → Int
def stream_id : (stream : Stream) → Int
def pending_stream : (pending : Pending a) → Int
def buffer_device : (buffer : ReadyBuffer a) → Int
def buffer_size : (buffer : ReadyBuffer a) → Int
def buffer_elem_size : (buffer : ReadyBuffer a) → Int
def buffer_bytes : (buffer : ReadyBuffer a) → Int
def pending_device : (pending : Pending a) → Int
def pending_size : (pending : Pending a) → Int
def i32_download_device : (p : I32Download) → Int
def i32_download_size : (p : I32Download) → Int
def i32_download_pair_device : (p : I32DownloadPair) → Int
def i32_download_pair_size : (p : I32DownloadPair) → Int
def float64_download_device : (p : Float64Download) → Int
def float64_download_size : (p : Float64Download) → Int
def float64_download_pair_device : (p : Float64DownloadPair) → Int
def float64_download_pair_size : (p : Float64DownloadPair) → Int