| | 146 | |
| | 147 | == Capture Read / Write at Runtime == |
| | 148 | * If the OpenMP Simplifier fails to sequentialize a program, transform the OpenMP program to the following form for model checking: |
| | 149 | {{{ |
| | 150 | $mem writes[nthreads], reads[nthreads]; |
| | 151 | $parfor (int tid:0..nthreads-1) { |
| | 152 | $write_set_push(); |
| | 153 | $read_set_push(); |
| | 154 | block1; |
| | 155 | // barrier |
| | 156 | writes[tid] = $write_set_pop(); |
| | 157 | reads[tid] = $read_set_pop(); |
| | 158 | // check for dataraces (collective operation) |
| | 159 | $write_set_push(); |
| | 160 | $read_set_push(); |
| | 161 | // barrier |
| | 162 | stmt2; |
| | 163 | // barrier |
| | 164 | writes[tid] = $write_set_pop(); |
| | 165 | reads[tid] = $read_set_pop(); |
| | 166 | // check for dataraces (collective operation) |
| | 167 | } |
| | 168 | }}} |
