source: CIVL/examples/concurrency/threadprivate.cvl@ 95f2d75

/*
 * Command line execution:
 * civl verify -por=new -inputNTHREADS=10 -inputN=20 threadprivate.cvl
 */
#include<civlc.h>
#include<stdio.h>
$input int NTHREADS;
$input int N;
#define OWNS(numIters, threadId, index) ((index)%NTHREADS==threadId)
$heap h;
$proc threads[NTHREADS];

int calculate_sum(int length, int *_pglobal) {
   int sum = 0;

   for (int j=0; j<length; j++) sum += _pglobal[j];
   return(sum);
}

void main() {
  int i, j, sum, TID, n=N;
  int length[n], check[n];

  for (i=0; i<n; i++) {
    length[i] = 10*(i+1);
    check[i] = length[i]*(length[i]+1)/2;
  }

  void __par_1(int _TID) { // every thread runs this
    int *_pglobal;

    void __for_loop_1 (int _i) {
      int _j, _sum;

      _pglobal = (int*)$malloc(&h, length[_i]*sizeof(int));
      _sum = 0;
      for (_j=0; _j<length[_i]; _j++) _pglobal[_j]=_j+1;
        _sum = calculate_sum(length[_i], _pglobal);
      printf("TID %d: value of sum for i = %d is %8d (check = %8d)\n",
               _TID, _i, _sum, check[_i]);
      $assert(_sum == check[_i]);
      $free(&h, _pglobal);
    }

    for (int _i=0; _i<n; _i++)
      if (OWNS(n, _TID, _i)) __for_loop_1(_i);
  }
  
  for (int t=0; t<NTHREADS; t++) threads[t] = $spawn __par_1(t);
  for (int t=0; t<NTHREADS; t++) $wait threads[t];
}