| 40 | | Here are some new proposed CIVL abstract datatypes that may be helpful. |
| 41 | | |
| 42 | | Handle type `$intseq`, representing a finite sequence of integers: |
| 43 | | {{{ |
| 44 | | $intseq $intseq_empty(); // returns empty sequence |
| 45 | | $intseq $intseq_add($intseq seq, int m); // appends m to sequence |
| 46 | | $intseq $intseq_remove($intseq seq, int i); // removes i-th element |
| 47 | | int $intseq_get($intseq seq, int i); // returns i-th element |
| 48 | | $intseq $intseq_set($intseq seq, int index, int value); // sets i-th element |
| 49 | | $intseq $intseq_insert($intseq seq, int index, int value); // inserts at index i |
| 50 | | int $intseq_length($intseq seq); // returns length of seq |
| 51 | | }}} |
| 52 | | |
| 53 | | Handle type `$distribution`, representing a distribution of n things into k disjoint sequences: |
| 54 | | |
| 55 | | {{{ |
| 56 | | /* distribute the integers 0,1,...,n-1 into k sequences NONDETERMINISTICALLY */ |
| 57 | | $distribution $distribute(int n, int k); |
| 58 | | $intseq $distribution_get(int i); |
| 59 | | }}} |
| 60 | | |
| 61 | | We can play with different implementations of the distribute function. On one extreme, it can return an arbitrary distribution; this will allow exploration of all possible executions of an OpenMP for loop. On the other extreme, we can sacrifice soundness for tractability and have it used a fixed strategy, like round-robin with chunk size 1. And various things in between. |
| | 40 | `$int_iter` is a handle type for an iterator of integers. |
| | 41 | |
| | 42 | /* Tells whether the integer iterator has any more elements */ |
| | 43 | _Bool $int_iter_hasNext($int_iter iter); |
| | 44 | |
| | 45 | /* Returns the next element in the iterator (and updates the iterator) */ |
| | 46 | int $int_iter_next($int_iter iter); |
| | 47 | |
| | 48 | |
| | 49 | == Worksharing state == |
| | 50 | |
| | 51 | The worksharing state will be stored in another handle type object. The situation here is analogous to the `$gcomm` and `$comm` use for MPI. Those objects store the shared state for message-passing. We need similar object for shared state the coordinates work-sharing and barrier constructs: |
| | 52 | * `$omp_gws`: global work-sharing state |
| | 53 | * `$omp_ws`: local state. A reference to a global object and a thread ID. |
| | 54 | |
| | 55 | API: |
| | 56 | {{{ |
| | 57 | /* Creates new global work-sharing state object, returning |
| | 58 | * handle to it. nthreads is the number of threads in |
| | 59 | * the parallel region. There is one of these per parallel region, |
| | 60 | * created upon entering the region */ |
| | 61 | $omp_gws $omp_gws_create($scope scope, int nthreads); |
| | 62 | |
| | 63 | $omp_gws_destroy($omp_gws gws); |
| | 64 | |
| | 65 | /* Creates a local work-sharing object, which is basically |
| | 66 | * a pair consisting of a global work-sharing handle and |
| | 67 | * a thread id. */ |
| | 68 | $omp_ws $omp_ws_create($omp_gws, int tid); |
| | 69 | |
| | 70 | $omp_ws_destroy($omp_ws ws); |
| | 71 | |
| | 72 | /* for "for" loops only: called when a thread arrives, it |
| | 73 | * returns the sequence of loop iterations to be performed by |
| | 74 | * the thread. Parameter location is the ID of the model location |
| | 75 | * of the top of the loop. It is needed to check that all threads |
| | 76 | * encounter the same worksharing statements in the same order. |
| | 77 | * Parameter start is the initial value of the loop variable; |
| | 78 | * end is its final value; and inc is the increment (which can be |
| | 79 | * positive or negative). */ |
| | 80 | $int_iter $omp_ws_arrive_loop($omp_ws ws, int location, int start, int end, int inc); |
| | 81 | |
| | 82 | /* for sections: called at arrival, returns the sequence of sections to |
| | 83 | * be executed by calling thread. The sections are numbered in order, |
| | 84 | * starting from 0. */ |
| | 85 | $int_iter $omp_ws_arrive_sections($omp_ws ws, int location); |
| | 86 | |
| | 87 | /* for single: called on arrival, returns whether or not to execute |
| | 88 | * the single code */ |
| | 89 | _Bool $omp_ws_arrive_single($omp_ws ws, int location); |
| | 90 | |
| | 91 | /* called when arriving at a barrier. This does not |
| | 92 | * impose the barrier, you still need to call system function |
| | 93 | * $barrier... for that. This is needed to ensure all threads |
| | 94 | * in the team call the same sequence of worksharing and barrier |
| | 95 | * constructs. */ |
| | 96 | void $omp_ws_arrive_barrier($omp_ws ws, int location); |
| | 97 | }}} |
| | 98 | |
