// civlc-omp.cvh: header file for CIVL-C support functions for OpenMP. #ifndef _CIVLC_OMP_ #define _CIVLC_OMP_ #include #include #include #pragma CIVL ACSL /** Important notes: * 1. none of those variables that comprise a shared object should ever * be accessed directly. All access must happen through $omp_read/write, * including the local views, status, and shared view. */ /* *********************** Types *********************** */ /* The status of a shared variable (or component of a shared * variable). For each shared variable, there is a "local view", * for each thread, which is a copy of the shared variable in * the thread scope. There is also the shared variable proper. * The local copy may be either empty or full. Flush operations * copy data between the local and shared copies, and modify * the empty/full bit. */ typedef enum $omp_var_status { EMPTY, // local is empty FULL, // local is occupied, no writes to it have been made MODIFIED // local is occupied, writes have been made to it } $omp_var_status; /* An enumerated type specifying the different kinds of OpenMP * "worksharing" constructs. */ typedef enum $omp_worksharing_kind { LOOP, BARRIER, SECTIONS, SINGLE } $omp_worksharing_kind; /* global shared object, containing a reference to a shared variable. * A handle type. */ typedef struct OMP_gshared * $omp_gshared; /* local view of a shared object, belonging to a single * thread, with reference to the global object, and * a local copy and a status of the shared object. * The type of the status variable is obtained from * the type of the original variable by replacing * all leaf nodes in the type tree with "int". * A handle type. */ typedef struct OMP_shared * $omp_shared; /* the worksharing information that a thread needs for executing * a worksharing region. It contains the kind of the worksharing * region, the location of the region, the status of the region * and the subdomain (iterations/sections/task assigned to the thread). */ typedef struct OMP_work_record $omp_work_record; /* global team object, represents a team of threads executing * in a parallel region. A handle type. This is where all the * state needed to correctly execute a parallel region will * be stored. This includes a global barrier, and a worksharing * queue for every thread. */ typedef struct OMP_gteam * $omp_gteam; /* * local object belonging to a single thread and referencing the * global team object. A handle type. It also includes the local * views of all shared data and a local barrier. */ typedef struct OMP_team * $omp_team; /* * semaphore struct used for helping control the execution of * CIVL-C code transformed from OpenMP programs. * It includes an integer value 'value' as its only field, * which is used for P/V operations. */ /* A helper struct used by CIVL for synchronizing the execution * of multiple threads required by an OpenMP program. * It has an 'int' field named as 'value', which is used for * determining the actual sync behaviors: block/unblock */ typedef struct OMP_HELPER_SIGNAL $omp_helper_signal; /* *********************** Functions *********************** */ /* creates new global team object, allocating object in heap * in specified scope. Number of threads that will be in the * team is nthreads. */ /*@ depends_on \nothing; */ $atomic_f $omp_gteam $omp_gteam_create($scope scope, int nthreads); /* destroys the global team object. All shared objects * associated to the team must have been destroyed before * calling this function. */ /*@ depends_on \access(gteam); */ $atomic_f void $omp_gteam_destroy($omp_gteam gteam); /* creates new local team object for a specific thread. */ /*@ depends_on \access(gteam); */ $atomic_f $omp_team $omp_team_create($scope scope, $omp_gteam gteam, int tid); /* destroys the local team object */ /*@ depends_on \access(team); */ $atomic_f void $omp_team_destroy($omp_team team); /* creates new global shared object, associated to the given * global team. A pointer to the shared variable that this * object corresponds to is given. */ /*@ depends_on \access(gteam, original); */ $atomic_f $omp_gshared $omp_gshared_create($omp_gteam gteam, void *original); /* destroys the global shared object, copying the content * to the original variable. */ /*@ depends_on \access(gshared); */ $atomic_f void $omp_gshared_destroy($omp_gshared gshared); /* creates a local shared object, returning handle to it. * The local copy of the shared object is initialized * by copying the values from the original variable referenced to * by the gshared object. The status variable is initialized to FULL. * The created shared object is appended * to the shared queue of the $omp_team object. */ /*@ depends_on \access(team, gshared, local, status); */ $atomic_f $omp_shared $omp_shared_create($omp_team team, $omp_gshared gshared, void *local, void *status); /* destroys the local shared object */ /*@ depends_on \access(shared); */ $atomic_f void $omp_shared_destroy($omp_shared shared); /* called by a thread to read a shared object. * ref is a pointer into the local copy of the shared variable. * The result of the read is stored in the * memory unit pointed to by result. * assumes ref is a pointer to a scalar. */ void $omp_read($omp_shared shared, void *result, void *ref); /* called by a thread to write to the shared object. * ref is a pointer into the local copy of the shared variable. * The value to be written is taken * from the memory unit pointed to by value. * assumes ref is a pointer to a scalar. */ void $omp_write($omp_shared shared, void *ref, void *value); /* applies the associative operator * specified by op to the local copy and the corresponding shared copy, * and writes the result back to the shared copy. * This happens in one atomic step. Example: you can * use this to add some value to a shared variable, * using CIVL_SUM for op. * assumes local is a pointer to a scalar. */ $atomic_f void $omp_apply_assoc($omp_shared shared, $operation op, void *local); /* applies the operation indicated by the given 'op' to combine * all referenced local copy values and the original reduction * item value. */ $atomic_f void $omp_reduction_combine( $operation op, void *reduction_final, void *reduction_local); /* performs an OpenMP flush operation on the shared object */ void $omp_flush($omp_shared shared, void *ref); /* performs an OpenMP flush operation on all shared * objects. This is the default in OpenMP if no argument * is specified for a flush construct. */ void $omp_flush_all($omp_team team); /* performs a barrier only. Note however that usually * (always?) a barrier is accompanied by a flush-all, * so $omp_barrier_and_flush should be used instead. */ void $omp_barrier($omp_team team); /* called by a thread when it reaches an omp for loop, * this function returns the subset of the loop domain * specifying the iterations that this thread will execute, * according to the given policy. In general, this * function is nondeterministic. * The dimension of the domain returned equals the * dimension of the given domain loop_dom. */ $domain $omp_arrive_loop($omp_team team, int location, $domain loop_dom, $domain_strategy strategy); /* called by a thread when it reaches an omp sections * construct, this function returns the subset of the * integers 0..numSections-1 specifying the indexes of * the sections that this thread will execute. The sections * are numbered from 0 in increasing order. */ $domain(1) $omp_arrive_sections($omp_team team, int location, int numSections); /* called by a thread when it reaches on omp single * construct, returns the thread ID of the thread that * will execute the single construct. */ int $omp_arrive_single($omp_team team, int location); /* called by a thread when a openMP synchronization point * is encountered and then this function will check and report * any possible occurrence of data race as assertion violations * iff there is a non-empty intersection between checked $mem pairs */ $atomic_f void $check_data_race($omp_team team); /* OMP Helper Signal Instance Creation * creates and returns an initialized '$omp_helper_signal' instance * with a given initial integer value 'initValue' */ $atomic_f $omp_helper_signal $omp_helper_signal_create( int initValue); /* OMP Helper Signal Wait Operation: * The caller process will wait (or be blocked) until the associated * $omp_helper_signal instance 'signal' value (signal->value) is set * as the same value being equal to 'waitValue' by calling * '$omp_helper_signal_send' with the same $omp_helper_signal instance */ $atomic_f void $omp_helper_signal_wait( $omp_helper_signal *signal, int waitValue); /* OMP Helper Signal Send Operation: * The caller process will set the given 'signal' value to be 'sendValue'. * This operation can be regarded as sending a 'signal' to those threads, * who are waiting for a specific integer value so that they can continue * executing statements following the call of '$omp_helper_signal_wait'. */ $atomic_f void $omp_helper_signal_send( $omp_helper_signal *signal, int sendValue); /* called by a thread to update its current read and write sets * with ones peeked from the current read/write set stack. * NOTE: both stacks are assumed to be non-empty. */ $atomic_f void $read_and_write_sets_pop($omp_team team); $atomic_f void $read_and_write_sets_push($omp_team team); $atomic_f void $omp_atomic_execution_lock_acquire( $omp_team team, $omp_helper_signal *lock); $atomic_f void $omp_atomic_execution_lock_release( $omp_team team, $omp_helper_signal *lock); $atomic_f void $omp_loop_operation($omp_team team); $atomic_f void $omp_thread_termination($omp_team team); #endif