00_prodcons is broken on newer builds

[rafaelsamenezes]

#include <pthread.h>
#include <stdio.h>

#define AMOUNT_PROD 5

#define AMOUNT_CONS 1

#define CS_OVERHEAD 1
#define DEADLINE 45
#define TRUE  1
#define FALSE 0

//@ DEFINE-MAIN-TIMER timer
unsigned int timer = 0;
void __ESBMC_atomic_begin();
void __ESBMC_atomic_end();
int __ESBMC_activeThread = -1;
_Bool join[AMOUNT_PROD+AMOUNT_CONS];

int item = 0;

pthread_mutex_t  lock = PTHREAD_MUTEX_INITIALIZER;
int thread_id[AMOUNT_PROD+AMOUNT_CONS];

void *producer(void *v) 
{
  //@ WCET-BLOCK [8]
  __ESBMC_atomic_begin();
  timer += 8; 
  int id = *(int*) v;
  pthread_mutex_lock(&lock);
  item = id;
  printf("Producer (%d): item = %d.\n", id, item);
  pthread_mutex_unlock(&lock);
  if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; 
  __ESBMC_activeThread = id;
  //@ ASSERT-TIMER (timer <= DEADLINE)
  assert (timer <= DEADLINE);
  join[id] = TRUE;
  __ESBMC_atomic_end();
  //@ BLOCK END

  return NULL;
}

void *consumer(void *v) 
{
  //@ WCET-BLOCK [7]
  __ESBMC_atomic_begin();
  timer += 7;
  int id = *(int*) v;
  pthread_mutex_lock(&lock);
  printf("Consumer (%d): item = %d.\n", id, item);
  pthread_mutex_unlock(&lock);
  if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; 
  __ESBMC_activeThread = id;
  //@ ASSERT-TIMER (timer <= DEADLINE)
  assert (timer <= DEADLINE);
  join[id] = TRUE;
  __ESBMC_atomic_end();
  //@ BLOCK END

  return NULL;
}


int main() 
{

  pthread_t thr_prod[AMOUNT_PROD];
  pthread_t thr_cons[AMOUNT_CONS];
  int i, j;

  __ESBMC_atomic_begin();
  for (i=0; i<(AMOUNT_PROD+AMOUNT_CONS); i++)
    join[i] = FALSE;
    
  // Creating PRODUCER'S threads
  for (i = 0; i < AMOUNT_PROD ; i++) {
    thread_id[i] = i;
    pthread_create(&thr_prod[i], NULL, producer, &thread_id[i]);
  }
  
  i = AMOUNT_PROD;
  // Creating CONSUMER'S threads
  for (j = 0; j < AMOUNT_CONS; j++) {
    thread_id[i] = i;
    pthread_create(&thr_cons[j], NULL, consumer, &thread_id[i]);
    i++;
  }

  __ESBMC_atomic_end();

  pthread_mutex_destroy (&lock);

  return 0;
}

With desc:

THOROUGH
main.c
--no-bounds-check --round-robin --context-bound 22
^VERIFICATION FAILED$

Is not working for macOS. We have to fix this and add again into the regression

[lucasccordeiro]

you could just reduce the context-bound to 2. Em seg., 15 de mar. de 2021 às 13:49, Rafael Sá Menezes < ***@***.***> escreveu:

…

#include <pthread.h> #include <stdio.h> #define AMOUNT_PROD 5 #define AMOUNT_CONS 1 #define CS_OVERHEAD 1 #define DEADLINE 45 #define TRUE 1 #define FALSE 0 //@ DEFINE-MAIN-TIMER timerunsigned int timer = 0;void __ESBMC_atomic_begin();void __ESBMC_atomic_end();int __ESBMC_activeThread = -1;_Bool join[AMOUNT_PROD+AMOUNT_CONS]; int item = 0; pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;int thread_id[AMOUNT_PROD+AMOUNT_CONS]; void *producer(void *v) { //@ WCET-BLOCK [8] __ESBMC_atomic_begin(); timer += 8; int id = *(int*) v; pthread_mutex_lock(&lock); item = id; printf("Producer (%d): item = %d.\n", id, item); pthread_mutex_unlock(&lock); if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; __ESBMC_activeThread = id; //@ ASSERT-TIMER (timer <= DEADLINE) assert (timer <= DEADLINE); join[id] = TRUE; __ESBMC_atomic_end(); //@ BLOCK END return NULL; } void *consumer(void *v) { //@ WCET-BLOCK [7] __ESBMC_atomic_begin(); timer += 7; int id = *(int*) v; pthread_mutex_lock(&lock); printf("Consumer (%d): item = %d.\n", id, item); pthread_mutex_unlock(&lock); if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; __ESBMC_activeThread = id; //@ ASSERT-TIMER (timer <= DEADLINE) assert (timer <= DEADLINE); join[id] = TRUE; __ESBMC_atomic_end(); //@ BLOCK END return NULL; } int main() { pthread_t thr_prod[AMOUNT_PROD]; pthread_t thr_cons[AMOUNT_CONS]; int i, j; __ESBMC_atomic_begin(); for (i=0; i<(AMOUNT_PROD+AMOUNT_CONS); i++) join[i] = FALSE; // Creating PRODUCER'S threads for (i = 0; i < AMOUNT_PROD ; i++) { thread_id[i] = i; pthread_create(&thr_prod[i], NULL, producer, &thread_id[i]); } i = AMOUNT_PROD; // Creating CONSUMER'S threads for (j = 0; j < AMOUNT_CONS; j++) { thread_id[i] = i; pthread_create(&thr_cons[j], NULL, consumer, &thread_id[i]); i++; } __ESBMC_atomic_end(); pthread_mutex_destroy (&lock); return 0; } With desc: THOROUGH main.c --no-bounds-check --round-robin --context-bound 22 ^VERIFICATION FAILED$ Is not working for macOS. We have to fix this and add again into the regression — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#418>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA4F4HPAGJZTPZZ5P6T2YCTTDYF53ANCNFSM4ZGS4OUA> .

-- Lucas C. Cordeiro​ https://ssvlab.github.io/lucasccordeiro/

[lucasccordeiro]

I think it is better to mark this test case as KNOWNBUG. The option round-robin is not maintained for quite some time. Em seg., 15 de mar. de 2021 às 13:51, Lucas Cordeiro < ***@***.***> escreveu:

…

you could just reduce the context-bound to 2. Em seg., 15 de mar. de 2021 às 13:49, Rafael Sá Menezes < ***@***.***> escreveu: > #include <pthread.h> > #include <stdio.h> > > #define AMOUNT_PROD 5 > > #define AMOUNT_CONS 1 > > #define CS_OVERHEAD 1 > #define DEADLINE 45 > #define TRUE 1 > #define FALSE 0 > //@ DEFINE-MAIN-TIMER timerunsigned int timer = 0;void __ESBMC_atomic_begin();void __ESBMC_atomic_end();int __ESBMC_activeThread = -1;_Bool join[AMOUNT_PROD+AMOUNT_CONS]; > int item = 0; > pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;int thread_id[AMOUNT_PROD+AMOUNT_CONS]; > void *producer(void *v) > { > //@ WCET-BLOCK [8] > __ESBMC_atomic_begin(); > timer += 8; > int id = *(int*) v; > pthread_mutex_lock(&lock); > item = id; > printf("Producer (%d): item = %d.\n", id, item); > pthread_mutex_unlock(&lock); > if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; > __ESBMC_activeThread = id; > //@ ASSERT-TIMER (timer <= DEADLINE) > assert (timer <= DEADLINE); > join[id] = TRUE; > __ESBMC_atomic_end(); > //@ BLOCK END > > return NULL; > } > void *consumer(void *v) > { > //@ WCET-BLOCK [7] > __ESBMC_atomic_begin(); > timer += 7; > int id = *(int*) v; > pthread_mutex_lock(&lock); > printf("Consumer (%d): item = %d.\n", id, item); > pthread_mutex_unlock(&lock); > if (__ESBMC_activeThread != id) timer += CS_OVERHEAD; > __ESBMC_activeThread = id; > //@ ASSERT-TIMER (timer <= DEADLINE) > assert (timer <= DEADLINE); > join[id] = TRUE; > __ESBMC_atomic_end(); > //@ BLOCK END > > return NULL; > } > > int main() > { > > pthread_t thr_prod[AMOUNT_PROD]; > pthread_t thr_cons[AMOUNT_CONS]; > int i, j; > > __ESBMC_atomic_begin(); > for (i=0; i<(AMOUNT_PROD+AMOUNT_CONS); i++) > join[i] = FALSE; > > // Creating PRODUCER'S threads > for (i = 0; i < AMOUNT_PROD ; i++) { > thread_id[i] = i; > pthread_create(&thr_prod[i], NULL, producer, &thread_id[i]); > } > > i = AMOUNT_PROD; > // Creating CONSUMER'S threads > for (j = 0; j < AMOUNT_CONS; j++) { > thread_id[i] = i; > pthread_create(&thr_cons[j], NULL, consumer, &thread_id[i]); > i++; > } > > __ESBMC_atomic_end(); > > pthread_mutex_destroy (&lock); > > return 0; > } > > With desc: > > THOROUGH > main.c > --no-bounds-check --round-robin --context-bound 22 > ^VERIFICATION FAILED$ > > Is not working for macOS. We have to fix this and add again into the > regression > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#418>, or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AA4F4HPAGJZTPZZ5P6T2YCTTDYF53ANCNFSM4ZGS4OUA> > . > -- Lucas C. Cordeiro​ https://ssvlab.github.io/lucasccordeiro/

-- Lucas C. Cordeiro​ https://ssvlab.github.io/lucasccordeiro/

[rafaelsamenezes]

I think it is better to mark this test case as KNOWNBUG.

It is working on Linux.

[rafaelsamenezes]

We could:

1. Let the CI keep failing and every time check if it was because of this testcase
2. Create another regression suites for OS.
3. Solve this and add it again

[mikhailramalho]

I'm OK with removing the round-robin option altogether. It never really worked and no one is maintaining it. Em seg., 15 de mar. de 2021 às 10:28, Rafael Sá Menezes < ***@***.***> escreveu:

…

We could: 1. Let the CI keep failing and every time check if it was because of this testcase 2. Create another regression suites for OS. 3. Solve this and add it again — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#418 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKEJHYQGJZ4FI2FZROVLTTTDYKRFANCNFSM4ZGS4OUA> .

-- Mikhail Ramalho.