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

  • Backend: Silicon
  • Language: C / OpenMP / OpenCL
  • Features: Iteration contracts, Arrays, Loop parallelisations, Quantified permissions, Pragmas
  • Path to Example File: openmp/add-spec-simd.c
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 53 (comments not included)
  • Lines of Specification: 13 (24.5% of total)
  • Computation Time: 20.9 seconds