source: CIVL/examples/concurrency/spawnBad.cvl@ 9705dfd

/* spawn2.cvl: simple example of spawning two processes.
 * More difficult to reduce than spawn.cvl, because
 * both are accessing variables in the same scope.
 *      civl verify -inputN=10 spawn2.cvl
 */
#include<civlc.h>

$input int N;
int s1, s2;

void f1(int n) {
  s1 = 0;
  for (int i=0; i<n; i++) s1 += i;
}

void f2(int n) {
  s2 = 0;
  for (int i=0; i<n; i++) s2 += i;
}

void main() {
  $proc p = $spawn f1(N);
  $proc q = $spawn f2(N);

  $assert s1==s2; // oops, should wait first
  $wait p;
  $wait q;
}