|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Macros | |
| #define | CURANDAPI |
| #define CURANDAPI |
| typedef unsigned int curandDirectionVectors32_t[32] |
CURAND array of 32-bit direction vectors.
| typedef unsigned long long curandDirectionVectors64_t[64] |
CURAND array of 64-bit direction vectors.
CURAND choice of direction vector set.
| typedef struct curandGenerator_st* curandGenerator_t |
CURAND generator.
| typedef enum curandOrdering curandOrdering_t |
CURAND orderings of results in memory.
| typedef enum curandRngType curandRngType_t |
CURAND generator types.
| typedef enum curandStatus curandStatus_t |
CURAND function call status types.
CURAND choice of direction vector set.
CURAND orderings of results in memory.
CURAND generator types.
CURAND Host API datatypes.
CURAND function call status types
| curandStatus_t CURANDAPI curandCreateGenerator | ( | curandGenerator_t * | generator, |
| curandRngType_t | rng_type ) |
Create new random number generator.
Creates a new random number generator of type rng_type and returns it in *generator.
Legal values for rng_type are:
When rng_type is CURAND_RNG_PSEUDO_DEFAULT, the type chosen is CURAND_RNG_PSEUDO_XORWOW.
When rng_type is CURAND_RNG_QUASI_DEFAULT, the type chosen is CURAND_RNG_QUASI_SOBOL32.
The default values for rng_type = CURAND_RNG_PSEUDO_XORWOW are:
seed = 0offset = 0ordering = CURAND_ORDERING_PSEUDO_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SOBOL32 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SOBOL64 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SCRAMBBLED_SOBOL32 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SCRAMBLED_SOBOL64 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULT| generator | - Pointer to generator |
| rng_type | - Type of generator to create |
rng_type is invalid | curandStatus_t CURANDAPI curandCreateGeneratorHost | ( | curandGenerator_t * | generator, |
| curandRngType_t | rng_type ) |
Create new host CPU random number generator.
Creates a new host CPU random number generator of type rng_type and returns it in *generator.
Legal values for rng_type are:
When rng_type is CURAND_RNG_PSEUDO_DEFAULT, the type chosen is CURAND_RNG_PSEUDO_XORWOW.
When rng_type is CURAND_RNG_QUASI_DEFAULT, the type chosen is CURAND_RNG_QUASI_SOBOL32.
The default values for rng_type = CURAND_RNG_PSEUDO_XORWOW are:
seed = 0offset = 0ordering = CURAND_ORDERING_PSEUDO_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SOBOL32 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SOBOL64 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SCRAMBLED_SOBOL32 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULTThe default values for rng_type = CURAND_RNG_QUASI_SCRAMBLED_SOBOL64 are:
dimensions = 1offset = 0ordering = CURAND_ORDERING_QUASI_DEFAULT| generator | - Pointer to generator |
| rng_type | - Type of generator to create |
rng_type is invalid | curandStatus_t CURANDAPI curandDestroyGenerator | ( | curandGenerator_t | generator | ) |
Destroy an existing generator.
Destroy an existing generator and free all memory associated with its state.
| generator | - Generator to destroy |
| curandStatus_t CURANDAPI curandGenerate | ( | curandGenerator_t | generator, |
| unsigned int * | outputPtr, | ||
| size_t | num ) |
Generate 32-bit pseudo or quasirandom numbers.
Use generator to generate num 32-bit results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 32-bit values with every bit random.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| num | - Number of random 32-bit values to generate |
| curandStatus_t CURANDAPI curandGenerateLogNormal | ( | curandGenerator_t | generator, |
| float * | outputPtr, | ||
| size_t | n, | ||
| float | mean, | ||
| float | stddev ) |
Generate log-normally distributed floats.
Use generator to generate num float results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 32-bit floating point values with log-normal distribution based on an associated normal distribution with mean mean and standard deviation stddev.
Normally distributed results are generated from pseudorandom generators with a Box-Muller transform, and so require num to be even. Quasirandom generators use an inverse cumulative distribution function to preserve dimensionality. The normally distributed results are transformed into log-normal distribution.
There may be slight numerical differences between results generated on the GPU with generators created with curandCreateGenerator() and results calculated on the CPU with generators created with curandCreateGeneratorHost(). These differences arise because of differences in results for transcendental functions. In addition, future versions of CURAND may use newer versions of the CUDA math library, so different versions of CURAND may give slightly different numerical values.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| n | - Number of floats to generate |
| mean | - Mean of associated normal distribution |
| stddev | - Standard deviation of associated normal distribution |
| curandStatus_t CURANDAPI curandGenerateLogNormalDouble | ( | curandGenerator_t | generator, |
| double * | outputPtr, | ||
| size_t | n, | ||
| double | mean, | ||
| double | stddev ) |
Generate log-normally distributed doubles.
Use generator to generate num double results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 64-bit floating point values with log-normal distribution based on an associated normal distribution with mean mean and standard deviation stddev.
Normally distributed results are generated from pseudorandom generators with a Box-Muller transform, and so require num to be even. Quasirandom generators use an inverse cumulative distribution function to preserve dimensionality. The normally distributed results are transformed into log-normal distribution.
There may be slight numerical differences between results generated on the GPU with generators created with curandCreateGenerator() and results calculated on the CPU with generators created with curandCreateGeneratorHost(). These differences arise because of differences in results for transcendental functions. In addition, future versions of CURAND may use newer versions of the CUDA math library, so different versions of CURAND may give slightly different numerical values.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| n | - Number of doubles to generate |
| mean | - Mean of normal distribution |
| stddev | - Standard deviation of normal distribution |
| curandStatus_t CURANDAPI curandGenerateLongLong | ( | curandGenerator_t | generator, |
| unsigned long long * | outputPtr, | ||
| size_t | num ) |
Generate 64-bit quasirandom numbers.
Use generator to generate num 64-bit results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 64-bit values with every bit random.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| num | - Number of random 64-bit values to generate |
| curandStatus_t CURANDAPI curandGenerateNormal | ( | curandGenerator_t | generator, |
| float * | outputPtr, | ||
| size_t | n, | ||
| float | mean, | ||
| float | stddev ) |
Generate normally distributed floats.
Use generator to generate num float results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 32-bit floating point values with mean mean and standard deviation stddev.
Normally distributed results are generated from pseudorandom generators with a Box-Muller transform, and so require num to be even. Quasirandom generators use an inverse cumulative distribution function to preserve dimensionality.
There may be slight numerical differences between results generated on the GPU with generators created with curandCreateGenerator() and results calculated on the CPU with generators created with curandCreateGeneratorHost(). These differences arise because of differences in results for transcendental functions. In addition, future versions of CURAND may use newer versions of the CUDA math library, so different versions of CURAND may give slightly different numerical values.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| n | - Number of floats to generate |
| mean | - Mean of normal distribution |
| stddev | - Standard deviation of normal distribution |
| curandStatus_t CURANDAPI curandGenerateNormalDouble | ( | curandGenerator_t | generator, |
| double * | outputPtr, | ||
| size_t | n, | ||
| double | mean, | ||
| double | stddev ) |
Generate normally distributed doubles.
Use generator to generate num double results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 64-bit floating point values with mean mean and standard deviation stddev.
Normally distributed results are generated from pseudorandom generators with a Box-Muller transform, and so require num to be even. Quasirandom generators use an inverse cumulative distribution function to preserve dimensionality.
There may be slight numerical differences between results generated on the GPU with generators created with curandCreateGenerator() and results calculated on the CPU with generators created with curandCreateGeneratorHost(). These differences arise because of differences in results for transcendental functions. In addition, future versions of CURAND may use newer versions of the CUDA math library, so different versions of CURAND may give slightly different numerical values.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| n | - Number of doubles to generate |
| mean | - Mean of normal distribution |
| stddev | - Standard deviation of normal distribution |
| curandStatus_t CURANDAPI curandGenerateSeeds | ( | curandGenerator_t | generator | ) |
Setup starting states.
Generate the starting state of the generator. This function is automatically called by generation functions such as curandGenerate() and curandGenerateUniform(). It can be called manually for performance testing reasons to separate timings for starting state generation and random number generation.
| generator | - Generator to update |
| curandStatus_t CURANDAPI curandGenerateUniform | ( | curandGenerator_t | generator, |
| float * | outputPtr, | ||
| size_t | num ) |
Generate uniformly distributed floats.
Use generator to generate num float results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 32-bit floating point values between 0.0f and 1.0f, excluding 0.0f and including 1.0f.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| num | - Number of floats to generate |
| curandStatus_t CURANDAPI curandGenerateUniformDouble | ( | curandGenerator_t | generator, |
| double * | outputPtr, | ||
| size_t | num ) |
Generate uniformly distributed doubles.
Use generator to generate num double results into the device memory at outputPtr. The device memory must have been previously allocated and be large enough to hold all the results. Launches are done with the stream set using curandSetStream(), or the null stream if no stream has been set.
Results are 64-bit double precision floating point values between 0.0 and 1.0, excluding 0.0 and including 1.0.
| generator | - Generator to use |
| outputPtr | - Pointer to device memory to store CUDA-generated results, or Pointer to host memory to store CPU-generated resluts |
| num | - Number of doubles to generate |
| curandStatus_t CURANDAPI curandGetDirectionVectors32 | ( | curandDirectionVectors32_t * | vectors[], |
| curandDirectionVectorSet_t | set ) |
Get direction vectors for 32-bit quasirandom number generation.
Get a pointer to an array of direction vectors that can be used for quasirandom number generation. The resulting pointer will reference an array of direction vectors in host memory.
The array contains vectors for many dimensions. Each dimension has 32 vectors. Each individual vector is an unsigned int.
Legal values for set are:
| vectors | - Address of pointer in which to return direction vectors |
| set | - Which set of direction vectors to use |
| curandStatus_t CURANDAPI curandGetDirectionVectors64 | ( | curandDirectionVectors64_t * | vectors[], |
| curandDirectionVectorSet_t | set ) |
Get direction vectors for 64-bit quasirandom number generation.
Get a pointer to an array of direction vectors that can be used for quasirandom number generation. The resulting pointer will reference an array of direction vectors in host memory.
The array contains vectors for many dimensions. Each dimension has 64 vectors. Each individual vector is an unsigned long long.
Legal values for set are:
| vectors | - Address of pointer in which to return direction vectors |
| set | - Which set of direction vectors to use |
| curandStatus_t CURANDAPI curandGetScrambleConstants32 | ( | unsigned int ** | constants | ) |
Get scramble constants for 32-bit scrambled Sobol' .
Get a pointer to an array of scramble constants that can be used for quasirandom number generation. The resulting pointer will reference an array of unsinged ints in host memory.
The array contains constants for many dimensions. Each dimension has a single unsigned int constant.
| constants | - Address of pointer in which to return scramble constants |
| curandStatus_t CURANDAPI curandGetScrambleConstants64 | ( | unsigned long long ** | constants | ) |
Get scramble constants for 64-bit scrambled Sobol' .
Get a pointer to an array of scramble constants that can be used for quasirandom number generation. The resulting pointer will reference an array of unsinged long longs in host memory.
The array contains constants for many dimensions. Each dimension has a single unsigned long long constant.
| constans | - Address of pointer in which to return scramble constants |
| curandStatus_t CURANDAPI curandGetVersion | ( | int * | version | ) |
Return the version number of the library.
Return in *version the version number of the dynamically linked CURAND library. The format is the same as CUDART_VERSION from the CUDA Runtime. The only supported configuration is CURAND version equal to CUDA Runtime version.
| version | - CURAND library version |
| curandStatus_t CURANDAPI curandSetGeneratorOffset | ( | curandGenerator_t | generator, |
| unsigned long long | offset ) |
Set the absolute offset of the pseudo or quasirandom number generator.
Set the absolute offset of the pseudo or quasirandom number generator.
All values of offset are valid. The offset position is absolute, not relative to the current position in the sequence.
| generator | - Generator to modify |
| offset | - Absolute offset position |
| curandStatus_t CURANDAPI curandSetGeneratorOrdering | ( | curandGenerator_t | generator, |
| curandOrdering_t | order ) |
Set the ordering of results of the pseudo or quasirandom number generator.
Set the ordering of results of the pseudo or quasirandom number generator.
Legal values of order for pseudorandom generators are:
Legal values of order for quasirandom generators are:
| generator | - Generator to modify |
| order | - Ordering of results |
| curandStatus_t CURANDAPI curandSetPseudoRandomGeneratorSeed | ( | curandGenerator_t | generator, |
| unsigned long long | seed ) |
Set the seed value of the pseudo-random number generator.
Set the seed value of the pseudorandom number generator. All values of seed are valid. Different seeds will produce different sequences. Different seeds will often not be statistically correlated with each other, but some pairs of seed values may generate sequences which are statistically correlated.
| generator | - Generator to modify |
| seed | - Seed value |
| curandStatus_t CURANDAPI curandSetQuasiRandomGeneratorDimensions | ( | curandGenerator_t | generator, |
| unsigned int | num_dimensions ) |
Set the number of dimensions.
Set the number of dimensions to be generated by the quasirandom number generator.
Legal values for num_dimensions are 1 to 20000.
| generator | - Generator to modify |
| num_dimensions | - Number of dimensions |
| curandStatus_t CURANDAPI curandSetStream | ( | curandGenerator_t | generator, |
| cudaStream_t | stream ) |
Set the current stream for CURAND kernel launches.
Set the current stream for CURAND kernel launches. All library functions will use this stream until set again.
| generator | - Generator to modify |
| stream | - Stream to use or NULL for null stream |