source: CIVL/examples/concurrency/spawn2.cvl@ 4f22a92

/* 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) {
  $atomic{
    s1 = 0;
    for (int i=0; i<n; i++) s1 += i;
  }
}

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

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

  $wait p;
  $wait q;
  $assert s1==s2;
}