/********************************************************
 * An example source module to accompany...
 *
 * "Using POSIX Threads: Programming with Pthreads"
 *     by Brad nichols, Dick Buttlar, Jackie Farrell
 *     O'Reilly & Associates, Inc.
 *
 ********************************************************
 * simple_threads.c
 *
 * Simple multi-threaded example.
 */
 
#include <civlc.h>
#include <stdio.h>

$input int INUM;
$input int JNUM;
$input int IBOUND;
$input int JBOUND;

$assume 0 < INUM && INUM <= IBOUND;
$assume 0 < JNUM && JNUM <= JBOUND;

int r1 = 0;
int r2 = 0;
 
void do_one_thing(int *pnum_times)
{
  int i, j;
  int x = 0;

  for (i = 0;  i < INUM; i++) {
    printf("doing one thing\n"); 
    for (j = 0; j < JNUM; j++){ 
      x = x + i;
      (*pnum_times)++;
    }
  } 
}
 
void do_another_thing(int *pnum_times)
{
  int i, j;
  int x = 0;

  for (i = 0;  i < INUM; i++) {
    printf("doing another \n"); 
    for (j = 0; j < JNUM; j++){ 
      x = x + i;
      (*pnum_times)++;
    }
  }
}
 
void do_wrap_up(int one_times, int another_times)
{
  int total;

  total = one_times + another_times;
  printf("All done, one thing %d, another %d for a total of %d\n",
  one_times, another_times, total);
}
 
void main()
{
  $proc thread1, thread2;
  
  thread1 = $spawn do_one_thing(&r1);
  thread2 = $spawn do_another_thing(&r2);

  $wait thread1;
  $wait thread2;

  do_wrap_up(r1, r2);

  $assert (r1==INUM*JNUM);
  $assert (r2==INUM*JNUM);
}