source: CIVL/include/impls/cuda.cvl@ 1aaefd4

#include <civlc.cvh>

/* Functions in this file are meant to serve as drop-in CIVL replacements
 * for the Cuda function of the same name. Because of this, much of the
 * documentation of these functions is identical to the documentation
 * for its Cuda counterpart.
 */

#include <string.h>
#include <stdlib.h>
#include <civl-cuda.cvh>
#include <concurrency.cvh>
#include <cuda.h>

/* Returns in *count the number of devices with compute capability 
 * greater or equal to 1.0 that are available for execution.
 */
cudaError_t cudaGetDeviceCount(int *count) {
  // possibly this should return an value specified as $input?
  *count = 1;
  return cudaSuccess;
}

/* Returns in *device the current device for the calling host thread
 */
cudaError_t cudaGetDevice(int * device) {
  *device = 0;
  return cudaSuccess;
}

/* Returns in *prop the properties of device dev
 */
cudaError_t cudaGetDeviceProperties(struct cudaDeviceProp * prop, int dev) {
  if (dev > 1)
    return cudaErrorInvalidDevice;

  strcpy(prop->name, "CIVL_CudaDevice0");

  return cudaSuccess;
}

/* Creates and event object
 */
cudaError_t cudaEventCreate(cudaEvent_t *event) {
    *event = $cuda_event_create();
    return cudaSuccess;
}

/* Records an event. If stream is non-zero, the event is recorded 
 * after all preceding operations in stream have been completed; 
 * otherwise, it is recorded after all preceding operations in the 
 * CUDA context have been completed. Since operation is asynchronous, 
 * cudaEventQuery() and/or cudaEventSynchronize() must be used to 
 * determine when the event has actually been recorded.
 */
cudaError_t cudaEventRecord(cudaEvent_t event, cudaStream_t s) {
    if ($cuda_get_instances(event) != NULL) {
        //printf("freeing instance list b\n");
        $free($cuda_get_instances(event));
    }
    if (s == NULL) {
        $cuda_set_instances(event, $cuda_all_most_recent_kernels(), $cuda_get_num_streams(&$cuda_current_context) + 1);
    } else {
        //printf("mallocing instance list c\n");
        $cuda_kernel_instance_t **instanceList = ($cuda_kernel_instance_t**)malloc(sizeof($cuda_kernel_instance_t*));
        instanceList[0] = $cuda_get_instance($cuda_get_most_recent(s));
        $cuda_set_instances(event, instanceList, 1);
    }
}

/* Query the status of all device work preceding the most recent call 
 * to cudaEventRecord() (in the appropriate compute streams, as 
 * specified by the arguments to cudaEventRecord()).
 * 
 * If this work has successfully been completed by the device, or if 
 * cudaEventRecord() has not been called on event, then cudaSuccess 
 * is returned. If this work has not yet been completed by the device 
 * then cudaErrorNotReady is returned.
 */
cudaError_t cudaEventQuery(cudaEvent_t event) {
    _Bool allKernelsFinished = $true;

    for (int i = 0; i < $cuda_get_num_instances(event); i++) {
        if ($cuda_get_status($cuda_get_instances(event)[i]) != $cuda_kernel_status_finished) {
            allKernelsFinished = $false;
            break;
        }
    }
    return allKernelsFinished ? cudaSuccess : cudaErrorNotReady;
}

/* Wait until the completion of all device work preceding the most 
 * recent call to cudaEventRecord() (in the appropriate compute streams, 
 * as specified by the arguments to cudaEventRecord()).
 *
 * If cudaEventRecord() has not been called on event, cudaSuccess 
 * is returned immediately.
 */
cudaError_t cudaEventSynchronize(cudaEvent_t event) {
    $cuda_event_wait(event);
    return cudaSuccess;
}

/* since "timing" doesn't really make sense in the verification process
 * I'm not sure what this should do. maybe it shouldn't exist.
 */
cudaError_t cudaEventElapsedTime(float *t, cudaEvent_t from, cudaEvent_t to) {
    *t = 1.0;
    return cudaSuccess;
}

/* Destroys the event specified by event.
 */
cudaError_t cudaEventDestroy(cudaEvent_t event) {
    $cuda_event_destroy(event);
    return cudaSuccess;
}

/* Creates a new asynchronous stream.
 */
cudaError_t cudaStreamCreate(cudaStream_t *pStream) {
  $cuda_stream_node_t *newNode = $cuda_stream_node_create();

  *pStream = $cuda_stream_create();
  $cuda_set_stream(newNode, *pStream);
  $cuda_set_next(newNode, $cuda_get_head_node(&$cuda_current_context));
  $cuda_add_new_stream(&$cuda_current_context, newNode);

  return cudaSuccess;
}
    
/* Blocks until stream has completed all operations.
 */
cudaError_t cudaStreamSynchronize(cudaStream_t stream) {
    cudaStream_t s;

    if (stream == NULL)
        s = $cuda_get_null_stream(&$cuda_current_context);
    else
        s = stream;
    $cuda_stream_wait(s);
    return cudaSuccess;
}

/* Destroys and cleans up the asynchronous stream specified by stream.
 */
cudaError_t cudaStreamDestroy(cudaStream_t pStream) {
  $assert($cuda_is_usable(pStream));
  $cuda_set_usable(pStream, $false);
  return cudaSuccess;
}

/* Explicitly destroys and cleans up all resources associated with the 
 * current device in the current process. Any subsequent API call to 
 * this device will reinitialize the device.
 */
cudaError_t cudaDeviceReset( void ) {
  // TODO: Figure out if _cudaContext must be destroyed here
  return cudaSuccess;
}

/* locks until stream has completed all operations.
 */
cudaError_t cudaDeviceSynchronize() {
    $cuda_stream_wait_all();
    $cuda_stream_wait($cuda_get_null_stream(&$cuda_current_context));
    return cudaSuccess;
}

/* Copies count bytes from the memory area pointed to by src to the 
 * memory area pointed to by dst, where kind is one of 
 * cudaMemcpyHostToHost, cudaMemcpyHostToDevice, cudaMemcpyDeviceToHost, 
 * or cudaMemcpyDeviceToDevice, and specifies the direction of the 
 * copy. The memory areas may not overlap.
 */
cudaError_t cudaMemcpy ( void *dst, const void *src, size_t count, enum cudaMemcpyKind kind ) {
  cudaDeviceSynchronize();
  memcpy(dst, src, count);
  cudaDeviceSynchronize();
  return cudaSuccess;
}

/* Fills the first count bytes of the memory area pointed to by devPtr
 * with the constant byte value value
 */
cudaError_t cudaMemset(void * devPtr, int value, size_t count) {
  memset(devPtr, value, count);
  return cudaSuccess;
}

/* Frees the memory space pointed to by devPtr. Similar semantics to free/$free.
 */
cudaError_t cudaFree(void *devPtr) {
  $free(devPtr);
  return cudaSuccess;
}

/* Sets device as the current device for the calling host thread. Currently,
 * only a single device is supported, so this call always succeeds with a noop.
 */
cudaError_t cudaSetDevice(int device_id) {
  return cudaSuccess;
}

/* Returns the message string from an error code
 */
char _cudaErrorString[10];

const char* cudaGetErrorString(cudaError_t error) {
  strcpy(_cudaErrorString, "test");
  return _cudaErrorString;
}

/* Returns the last error that has been produced by any of the runtime calls
 * in the same host thread and resets it to cudaSuccess
 */
cudaError_t cudaGetLastError() {
  return cudaSuccess;
} 

/* DEPRECATED. DO NOT USE
 */
cudaError_t cudaThreadExit() {
  return cudaSuccess;
}

/* C++ Language Extensions */

/* Reads the 16-bit, 32-bit or 64-bit word old located at the address address in
 * global or shared memory, computes (old + val), and stores the result back to
 * memory at the same address. These three operations are performed in one atomic
 * transaction. The function returns old.
 */
int cudaAtomicAdd_int(int* address, int val) {
        int old = *address;
        *address += val;
        // Add call to $check_data_race??
        return old;
}
unsigned int cudaAtomicAdd_uint(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address += val;
        return old;
}
unsigned long long int cudaAtomicAdd_ullint(unsigned long long int* address,
                                        unsigned long long int val) {
        unsigned long long int old = *address;
        *address += val;
        return old;
}
float cudaAtomicAdd_float(float* address, float val) {
        float old = *address;
        *address += val;
        return old;
}
double cudaAtomicAdd_double(double* address, double val) {
        double old = *address;
        *address += val;
        return old;
}

/* reads the 32-bit word old located at the address address in global or shared
 * memory, computes (old - val), and stores the result back to memory at the same
 * address. These three operations are performed in one atomic transaction. The
 * function returns old.
 */
int cudaAtomicSub_int(int* address, int val) {
        int old = *address;
        *address -= val;
        return old;
}
unsigned int cudaAtomicSub_uint(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address -= val;
        return old;
}

/* reads the 32-bit or 64-bit word old located at the address address in global
 * or shared memory and stores val back to memory at the same address. These two
 * operations are performed in one atomic transaction. The function returns old. 
 */
int cudaAtomicExch_int(int* address, int val) {
        int old = *address;
        *address = val;
        return old;
}
unsigned int cudaAtomicExch_uint(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address = val;
        return old;
}
unsigned long long int cudaAtomicExch_ullint(unsigned long long int* address,
                                  unsigned long long int val) {
        unsigned long long int old = *address;
        *address = val;
        return old;
}
float cudaAtomicExch_float(float* address, float val) {
        float old = *address;
        *address = val;
        return old;
}

/* reads the 32-bit or 64-bit word old located at the address address in global
 * or shared memory, computes the minimum of old and val, and stores the result
 * back to memory at the same address. These three operations are performed in one
 * atomic transaction. The function returns old.
 */
int cudaAtomicMin_int(int* address, int val) {
        int old = *address;
        *address = (old <= val) ? old : val;
        return old;
}
unsigned int cudaAtomicMin_uint(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address = (old <= val) ? old : val;
        return old;
}
unsigned long long int cudaAtomicMin_ullint(unsigned long long int* address,
                                        unsigned long long int val) {
        unsigned long long int old = *address;
        *address = (old <= val) ? old : val;
        return old;
}

/* reads the 32-bit or 64-bit word old located at the address address in global
 * or shared memory, computes the maximum of old and val, and stores the result
 * back to memory at the same address. These three operations are performed in one
 * atomic transaction. The function returns old.
 */
int cudaAtomicMax_int(int* address, int val) {
        int old = *address;
        *address = (old >= val) ? old : val;
        return old;
}
unsigned int cudaAtomicMax_uint(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address = (old >= val) ? old : val;
        return old;
}
unsigned long long int cudaAtomicMax_ullint(unsigned long long int* address,
                                        unsigned long long int val) {
        unsigned long long int old = *address;
        *address = (old >= val) ? old : val;
        return old;
}

/* reads the 32-bit word old located at the address address in global or shared
 * memory, computes ((old >= val) ? 0 : (old+1)), and stores the result back to
 * memory at the same address. These three operations are performed in one atomic
 * transaction. The function returns old.
 */
unsigned int atomicInc(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address = (old >= val) ? 0 : old + 1;
        return old;
}

/* reads the 32-bit word old located at the address address in global or shared
 * memory, computes (((old == 0) || (old > val)) ? val : (old-1) ), and stores
 * the result back to memory at the same address. These three operations are
 * performed in one atomic transaction. The function returns old.
 */
unsigned int atomicDec(unsigned int* address, unsigned int val) {
        unsigned int old = *address;
        *address = ((old == 0) || (old > val)) ? val : old-1;
        return old;
}

/* reads the 16-bit, 32-bit or 64-bit word old located at the address address in
 * global or shared memory, computes (old == compare ? val : old) , and stores the
 * result back to memory at the same address. These three operations are performed
 * in one atomic transaction. The function returns old (Compare And Swap).
 */
int cudaAtomicCAS_int(int* address, int compare, int val) {
        int old = *address;
        *address = old == compare ? val : old;
        return old;
}
unsigned int cudaAtomicCAS_uint(unsigned int* address,
                            unsigned int compare,
                            unsigned int val) {
        unsigned int old = *address;
        *address = old == compare ? val : old;
        return old;
}
unsigned long long int cudaAtomicCAS_ullint(unsigned long long int* address,
                                        unsigned long long int compare,
                                        unsigned long long int val) {
        unsigned long long int old = *address;
        *address = old == compare ? val : old;
        return old;
}
unsigned short int cudaAtomicCAS_usint(unsigned short int* address,
                                   unsigned short int compare,
                                   unsigned short int val) {
        unsigned short int old = *address;
        *address = old == compare ? val : old;
        return old;
}