OpenMP: SIMD programs

Simple SIMD program written in OpenMP for C, where several arrays are read and written in parallel. We verify that the `#pragma` annotations are correct, meaning that the parallelised version of this program has the same functional meaning as the sequential program.

General information

ID103
Articlenone
Back-endSilicon
LanguageOpenMP for C
FeaturesArrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissions
Sources
Path to example fileopenmp/add-spec-simd.c
Date2017-06-20

Statistical information

Lines of code53 lines (comments not included)
Lines of specification13 lines (24.53% of the total)
Computation time20933 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.