source: CIVL/examples/pthread/sync01_true.cvl@ f6ce0eb

/**
* This is a translation of a Pthread program from 
* the Pthread benchmarks of SV-COMP 2014.
* https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/
*
* Command line execution:
* civl verify sync01_true.cvl
*/

#include <civlc.h>
#include "pthread.cvh"

int  num;
pthread_mutex_t  m;
pthread_cond_t  empty, full;

void *thread1(void*arg)
{
  pthread_mutex_lock(&m);

  while (num > 0) 
    pthread_cond_wait(&empty, &m);
  
  num++;

  pthread_mutex_unlock(&m);
  pthread_cond_signal(&full);
  return NULL;
}


void *thread2(void*arg)
{
  pthread_mutex_lock(&m);

  while (num == 0) 
    pthread_cond_wait(&full, &m);

  num--;
  
  pthread_mutex_unlock(&m);

  pthread_cond_signal(&empty);

  return NULL;
}


void main()
{
  pthread_t  t1, t2;

  num = 1;

  pthread_mutex_init(&m, 0);
  pthread_cond_init(&empty, NULL);
  pthread_cond_init(&full, NULL);
  
  pthread_create(&t1, 0, thread1, 0);
  pthread_create(&t2, 0, thread2, 0);
  
  pthread_join(t1, 0);
  pthread_join(t2, 0);

  if (num!=1)
  {
    $assert($false);
  }
}