| | 38 | == Helper primitives == |
| | 39 | |
| | 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. |
| | 62 | |
