2 OpenMP Transformation CIVL Types and Functions

2.1 CIVL-C Types Introduced for OpenMP Transformation

$omp_gteam

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 (incomplete array-of-$omp_work_record) for every thread.

Definition:

typedef struct OMP_gteam {
  $scope scope;
  int nthreads;
  _Bool init[];
  $omp_work_record work[][];
  $gbarrier gbarrier;
} * $omp_gteam;

$omp_team

local object belonging to a single thread and referencing the global team object. A handle type. It also includes a local barrier.

Definition:

typedef struct OMP_team {
  $omp_gteam gteam;
  $scope scope;
  int tid;
  $barrier barrier;
} * $omp_team;

$omp_work_record

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).

Definition:

typedef struct OMP_work_record {
  int kind; // loop, barrier, sections, or single
  int location; // location in model of construct
  _Bool arrived; // has this thread arrived yet?
  $domain loop_dom;// full loop domain; null if not loop
  $domain subdomain; // tasks this thread must do
} $omp_work_record;

2.2 CIVL-C Functions Introduced for OpenMP Transformation

2.2.1 Team Creation and Destruction Functions

$omp_gteam $omp_gteam_create($scope scope, int nthreads)

returns a reference to a newly created global team obejct.

scope is a scope of a heap where this object is allocated.

nthreads is the number of threads in this global team.

void $omp_gteam_destroy($omp_gteam gteam)

destroys the given global team object. All shared objects associated with this global team object must have been destroyed before calling the function.

gteam is a global team object shall be destroyed.

$omp_team $omp_team_create($scope scope, $omp_gteam gteam, int tid)

returns a reference to a newly created local team object for a specific thread.

scope is the scope of a heap where this object is allocated.

gteam is the global team object where this local team object is associated.

tid is the id of the specific thread that this local team object is related to.

void $omp_team_destroy($omp_team team)

destroys the given local team object.

team is a local team object shall be destroyed.

2.2.2 Worksharing and Barriers Functions

void $omp_barrier($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.

team is the local team object representing a specific thread performing this barrier operation.

void $omp_barrier_and_flush($omp_team team)

performs a barrier and a flush-all (on all shared objects owned by the given team). It is implicitly performed in many OpenMP worksharing constructs. Data race violations are checked in this function by examining read and write set intersections between different threads.

team is the local team object representing a specific thread performing this barrier and flush-all operation.

$domain $omp_arrive_loop($omp_team team, int location, $domain loop_dom, $domain_strategy strategy)

returns the subset of the given loop domain specifying the iterations that this thread will execute. The function is called by a thread when it reaches an OpenMP for/do loop.

team is the local team object representing a specific thread.

location is the location of the encountered OpenMP for/do loop.

loop_dom is the complete loop domain containing all valid iterations.

strategy is the strategy distributing loop iterations to threads.

$domain(1) $omp_arrive_sections($omp_team team, int location, int numSections)

returns the subset of integers ranging from 0 to numSections - 1 specifying indices of sections that this thread will execute. The function is called by a thread when it reaches an OpenMP sections construct. (Sections are numbered from 0 to numSections - 1)

team is the local team object representing a specific thread.

location is the location of the encountered OpenMP sections construct.

numSections is the total number of section constructs in the encountered sections construct.

int $omp_arrive_single($omp_team team, int location)

returns the ID of the thread that shall execute the encountered single construct.

team is the local team object representing a specific thread.

location is the location of the encountered OpenMP single construct.

2.2.3 $mem Functions

$mem

A mem object is an immutable value representing a set of memory locations. The mem library provides the $mem type and a set of operations on mem objects. In CIVL-C, each process has, as part of its state, a "read stack" and a "write stack". Each stack consists of mutable stack entries. Each stack entry has a mem field, which is updated automatically each time the process performs a read or write. When the process reads memory location l, every entry on the read stack is updated with new mem values that are obtained by adding l to the old values. Similarly, when a process writes l, every entry on the write stack is so updated. New entries can be pushed onto the stacks using functions provided here. Similarly, each stack can be popped and the final mem value of the popped entry can be retrieved. These functions are useful for many things, such as checking for data races in multi-threaded programs. Note that $mem values can be created by casting a pointer expression to $mem. Examples:

   int x;
   $mem m1 = ($mem)&x;
   int a[10];
   $mem m2 = ($mem)&a[0]; // just the bits of "a[0]"
   $mem m3 = ($mem)&a; // all locations in a: a[0..9]
   $mem m4 = ($mem)a[0..9];
   $mem_equals(m3, m4); // true 

$system void $write_set_push()

$system $mem $write_set_pop()

$state_f $system $mem $write_set_peek()

$system void $read_set_push()

$system $mem $read_set_pop()

$state_f $system $mem $read_set_peek()

$atomic_f $system $mem $mem_empty()

$atomic_f $system _Bool $mem_equals($mem m0, $mem m1)

$atomic_f $system _Bool $mem_contains($mem super, $mem sub)

$atomic_f $system _Bool $mem_no_intersect($mem m0, $mem m1, $mem *out0, $mem *out1)

$atomic_f $system $mem $mem_union($mem mem0, $mem mem1)

$atomic_f $system $mem $mem_union_widening($mem, $mem)

$atomic_f $system void $mem_havoc($mem m)

$atomic_f $system $mem $mem_unary_widening($mem m)

$atomic_f $system void $mem_assign_from($state s, $mem m)

2.2.4 $track Block and Functions

(in-progress)

$track{ /* SRC CODE */ }

void $track_empty()

$mem $tracked_resds()

$mem $tracked_writes()

$depends_on( .. ){ /* SRC CODE */ }

2.2.5 Miscellaneous Functions

void $omp_apply_assoc(void * x, $operation op, void * y)

is the translation of x = x op y

x is the variable shall be updated

op is the binary operator applied on x

y is the second operand used for updating x value by applying op

void $omp_flush_all($omp_team team)

performs an OpenMP flush operation on all shared objects. This is the default in OpenMP if no argument is specified for a flush construct.

team is the local team object representing a specific thread performing this flush-all operation.

2.3 Worksharing Model

This section describes how the system functions dealing with worksharing are implemented.

The global data structure $omp_gteam contains a FIFO queue for each thread. The queue contains work-sharing records, one record for each work-sharing or barrier construct encountered. The record contains the basic information about the construct as provided by the arguments to the arrival function, as well as the distribution chosen for that thread.

The constructs are a lot like MPI collective operations, and are modeled similarly.

When a thread arrives at one of these constructs, it invokes the relevant arrival function. At this point you can determine whether this thread is the first to arrive at that construct. If its queue is empty, it is the first, otherwise it is not first, and the oldest entry in its queue will be the entry corresponding to this construct.

When a thread is the first thread to arrive at a construct, a distribution is chosen for every thread and a record is created and enqueued in each thread queue (including the caller). The distributions can be chosen nondeterministically, possibly with some restrictions to achieve some tractability/soundness compromise. The record for this thread is then dequeued and the iterator returned.

If a thread is not the first to arrive, its record is dequeued and compared with the arguments given in the function call. They should match, and if they don't, an error is reported. This indicates that either threads encountered constructs in different orders or the loop parameters changed.

Notes

• This OpenMP transformation assumes given OpenMP programs are sequentially consistent.
• OpenMP atomic construct without seq_cst is out of our current verification domain.

---

Back: Index

Prev: Introduction

Next: Supported OpenMP Features