diff --git a/benchmarks/lfds/dglm.c b/benchmarks/lfds/dglm.c index 0c33c8259e..4b8c8d6c84 100644 --- a/benchmarks/lfds/dglm.c +++ b/benchmarks/lfds/dglm.c @@ -1,6 +1,5 @@ #include "dglm.h" #include -#include #ifndef NTHREADS #define NTHREADS 3 @@ -26,7 +25,7 @@ int main() init(); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, worker, (void *)i); + pthread_create(&t[i], 0, worker, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/lfds/dglm.h b/benchmarks/lfds/dglm.h index 630a99806b..64df3f08b7 100644 --- a/benchmarks/lfds/dglm.h +++ b/benchmarks/lfds/dglm.h @@ -1,4 +1,6 @@ #include +#include +#include #ifdef FAIL #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED)) diff --git a/benchmarks/lfds/hash_table.c b/benchmarks/lfds/hash_table.c index 0f146799a8..f09ce634ba 100644 --- a/benchmarks/lfds/hash_table.c +++ b/benchmarks/lfds/hash_table.c @@ -46,10 +46,10 @@ int main() init(); for (int i = 0; i < PAIRS; i++) - pthread_create(&t[i], 0, thread_1, (void *)i); + pthread_create(&t[i], 0, thread_1, (void *)(size_t)i); for (int i = 0; i < PAIRS; i++) - pthread_create(&t[PAIRS + i], 0, thread_2, (void *)i); + pthread_create(&t[PAIRS + i], 0, thread_2, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/lfds/ms.c b/benchmarks/lfds/ms.c index 9bd478acc0..23a1cb2cc6 100644 --- a/benchmarks/lfds/ms.c +++ b/benchmarks/lfds/ms.c @@ -25,7 +25,7 @@ int main() init(); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, worker, (void *)i); + pthread_create(&t[i], 0, worker, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/lfds/ms.h b/benchmarks/lfds/ms.h index bc68160777..3c2445db9a 100644 --- a/benchmarks/lfds/ms.h +++ b/benchmarks/lfds/ms.h @@ -1,4 +1,6 @@ #include +#include +#include #ifdef FAIL #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED)) diff --git a/benchmarks/lfds/treiber.c b/benchmarks/lfds/treiber.c index 036c9fe3a2..46e3f0512d 100644 --- a/benchmarks/lfds/treiber.c +++ b/benchmarks/lfds/treiber.c @@ -26,7 +26,7 @@ int main() init(); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, worker, (void *)i); + pthread_create(&t[i], 0, worker, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/lfds/treiber.h b/benchmarks/lfds/treiber.h index 3d590216db..f86d6bf359 100644 --- a/benchmarks/lfds/treiber.h +++ b/benchmarks/lfds/treiber.h @@ -1,4 +1,5 @@ #include +#include #ifdef FAIL #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED)) diff --git a/benchmarks/locks/clh_mutex.c b/benchmarks/locks/clh_mutex.c index b049201028..1dfb6b51c4 100644 --- a/benchmarks/locks/clh_mutex.c +++ b/benchmarks/locks/clh_mutex.c @@ -30,7 +30,7 @@ int main() clh_mutex_init(&lock); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/cna.c b/benchmarks/locks/cna.c index be68b9fa51..fd1b44ed6f 100644 --- a/benchmarks/locks/cna.c +++ b/benchmarks/locks/cna.c @@ -30,7 +30,7 @@ int main() pthread_t t[NTHREADS]; for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/mutex.c b/benchmarks/locks/mutex.c index 660e3d82e7..018d8ab778 100644 --- a/benchmarks/locks/mutex.c +++ b/benchmarks/locks/mutex.c @@ -30,7 +30,7 @@ int main() mutex_init(&mutex); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/mutex_musl.c b/benchmarks/locks/mutex_musl.c index bac40939e1..413b8b5b73 100644 --- a/benchmarks/locks/mutex_musl.c +++ b/benchmarks/locks/mutex_musl.c @@ -30,7 +30,7 @@ int main() mutex_init(&mutex); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/seqlock.c b/benchmarks/locks/seqlock.c index 10aef63e5a..7afc94120b 100644 --- a/benchmarks/locks/seqlock.c +++ b/benchmarks/locks/seqlock.c @@ -1,6 +1,5 @@ #include "seqlock.h" #include -#include #ifndef NREADERS #define NREADERS 3 diff --git a/benchmarks/locks/seqlock.h b/benchmarks/locks/seqlock.h index 0580a98f43..ff60341b80 100644 --- a/benchmarks/locks/seqlock.h +++ b/benchmarks/locks/seqlock.h @@ -1,4 +1,5 @@ #include +#include struct seqlock_s { // Sequence for reader consistency check diff --git a/benchmarks/locks/spinlock.c b/benchmarks/locks/spinlock.c index 801325a39c..77dabbbbd0 100644 --- a/benchmarks/locks/spinlock.c +++ b/benchmarks/locks/spinlock.c @@ -30,7 +30,7 @@ int main() spinlock_init(&lock); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/ticket_awnsb_mutex.c b/benchmarks/locks/ticket_awnsb_mutex.c index bd7cc7396c..3144c557a7 100644 --- a/benchmarks/locks/ticket_awnsb_mutex.c +++ b/benchmarks/locks/ticket_awnsb_mutex.c @@ -30,7 +30,7 @@ int main() ticket_awnsb_mutex_init(&lock, DEFAULT_MAX_WAITERS); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/ticket_awnsb_mutex.h b/benchmarks/locks/ticket_awnsb_mutex.h index 9c7d7b8b9b..adac88b724 100644 --- a/benchmarks/locks/ticket_awnsb_mutex.h +++ b/benchmarks/locks/ticket_awnsb_mutex.h @@ -131,7 +131,7 @@ typedef struct atomic_int egress; char padding2[8]; int maxArrayWaiters; - _Atomic(struct awnsb_node_t *)* waitersArray; + _Atomic(awnsb_node_t *)* waitersArray; } ticket_awnsb_mutex_t; /* @@ -155,9 +155,9 @@ void ticket_awnsb_mutex_init(ticket_awnsb_mutex_t * self, int maxArrayWaiters) atomic_init(&self->ingress, 0); atomic_init(&self->egress, 0); self->maxArrayWaiters = maxArrayWaiters; - self->waitersArray = (awnsb_node_t **)malloc(self->maxArrayWaiters*sizeof(awnsb_node_t *)); + self->waitersArray = (_Atomic(awnsb_node_t *)*)malloc(self->maxArrayWaiters*sizeof(awnsb_node_t *)); __VERIFIER_loop_bound(DEFAULT_MAX_WAITERS+1); - for (int i = 0; i < self->maxArrayWaiters; i++) self->waitersArray[i] = ATOMIC_VAR_INIT(NULL); + for (int i = 0; i < self->maxArrayWaiters; i++) atomic_init(&self->waitersArray[i], NULL); } @@ -178,7 +178,7 @@ void ticket_awnsb_mutex_destroy(ticket_awnsb_mutex_t * self) */ void ticket_awnsb_mutex_lock(ticket_awnsb_mutex_t * self) { - const long long ticket = atomic_fetch_add_explicit(&self->ingress, 1, memory_order_relaxed); + const int ticket = atomic_fetch_add_explicit(&self->ingress, 1, memory_order_relaxed); #ifdef FAIL if (atomic_load_explicit(&self->egress, memory_order_relaxed) == ticket) return; #else @@ -221,7 +221,7 @@ void ticket_awnsb_mutex_lock(ticket_awnsb_mutex_t * self) */ void ticket_awnsb_mutex_unlock(ticket_awnsb_mutex_t * self) { - long long ticket = atomic_load_explicit(&self->egress, memory_order_relaxed); + int ticket = atomic_load_explicit(&self->egress, memory_order_relaxed); // Clear up our entry in the array before releasing the lock. atomic_store_explicit(&self->waitersArray[(int)(ticket % self->maxArrayWaiters)], NULL, memory_order_relaxed); // We could do this load as relaxed per se but then the store on egress of -(ticket+1) could be re-ordered to be before, and we don't want that @@ -242,8 +242,8 @@ void ticket_awnsb_mutex_unlock(ticket_awnsb_mutex_t * self) */ int ticket_awnsb_mutex_trylock(ticket_awnsb_mutex_t * self) { - long long localE = atomic_load(&self->egress); - long long localI = atomic_load_explicit(&self->ingress, memory_order_relaxed); + int localE = atomic_load(&self->egress); + int localI = atomic_load_explicit(&self->ingress, memory_order_relaxed); if (localE != localI) return EBUSY; if (!atomic_compare_exchange_strong(&self->ingress, &localI, self->ingress+1)) return EBUSY; // Lock has been acquired diff --git a/benchmarks/locks/ticketlock.c b/benchmarks/locks/ticketlock.c index dae5886611..0ae025fa45 100644 --- a/benchmarks/locks/ticketlock.c +++ b/benchmarks/locks/ticketlock.c @@ -30,7 +30,7 @@ int main() ticketlock_init(&lock); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/benchmarks/locks/ttas.c b/benchmarks/locks/ttas.c index cc399bb939..70c3a12318 100644 --- a/benchmarks/locks/ttas.c +++ b/benchmarks/locks/ttas.c @@ -30,7 +30,7 @@ int main() ttaslock_init(&lock); for (int i = 0; i < NTHREADS; i++) - pthread_create(&t[i], 0, thread_n, (void *)i); + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); for (int i = 0; i < NTHREADS; i++) pthread_join(t[i], 0); diff --git a/include/dat3m.h b/include/dat3m.h index 1f753b05b2..4797c59ea9 100644 --- a/include/dat3m.h +++ b/include/dat3m.h @@ -1,4 +1,6 @@ extern int __VERIFIER_nondet_int(void); +extern int __VERIFIER_nondet_uint(void); +extern _Bool __VERIFIER_nondet_bool(void); extern void __VERIFIER_assume(int cond); extern void __VERIFIER_loop_bound(int);