Skip to content

Verify Concurrency Issues: Version 5.12 can verify this problem, but version 5.93.0 can not. #7957

@fir3workX

Description

@fir3workX

CBMC version:5.12 & 5.93.0
Operating system: Linux (ubuntu)
Exact command line resulting in the issue:cbmc dataRaceCond.c
What behaviour did you expect: Verify Concurrency
What happened instead: Version 5.12 can verify this problem, but version 5.93.0 can not.

--------dataRaceCond.c--------

#include <assert.h>
#include <pthread.h>
pthread_mutex_t mutex;
int balance =1000;
void* transaction(void* amount)
{
// pthread_mutex_lock(&mutex);

int current = balance;
current += *(int *)amount;
balance = current;

// pthread_mutex_unlock(&mutex);

return 0;
}
int main()
{
pthread_t t1,t2;
pthread_mutex_init(&mutex, 0);
int amount1 = -3000;
pthread_create(&t1, 0, transaction, &amount1);
int amount2 = 9000;
pthread_create(&t2, 0, transaction, &amount2);
pthread_join(t1, 0);
pthread_join(t2, 0);
assert(balance == 7000);
pthread_mutex_destroy(&mutex);
return 0;
}


image

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions