Forward dependencies (succeeding)
Verification example with a loop where the iterations have forward dependencies. Permissions are redistributed via sends receives.
|Language||OpenMP for C|
|Features||Arrays, Iteration contracts, Loop parallelisations|
|Path to example file||carp/forward-loop.c|
|Lines of code||47 lines (comments not included)|
|Lines of specification||27 lines (57.45% of the total)|
|Computation time||18190 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.