Merge branch 'development_rework' into threadCf&mustEdges

benchmarks/lfds/dglm.c

@@ -1,6 +1,5 @@
 #include "dglm.h"
 #include <pthread.h>
-#include <assert.h>
 
 #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);

benchmarks/lfds/dglm.h

@@ -1,4 +1,6 @@
 #include <stdatomic.h>
+#include <assert.h>
+#include <stdlib.h>
 
 #ifdef FAIL
 #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED))

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);

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);

benchmarks/lfds/ms.h

@@ -1,4 +1,6 @@
 #include <stdatomic.h>
+#include <assert.h>
+#include <stdlib.h>
 
 #ifdef FAIL
 #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED))

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);

benchmarks/lfds/treiber.h

@@ -1,4 +1,5 @@
 #include <stdatomic.h>
+#include <stdlib.h>
 
 #ifdef FAIL
 #define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED))

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);

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);

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);

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);

benchmarks/locks/seqlock.c

@@ -1,6 +1,5 @@
 #include "seqlock.h"
 #include <pthread.h>
-#include <assert.h>
 
 #ifndef NREADERS
 #define NREADERS 3

benchmarks/locks/seqlock.h

@@ -1,4 +1,5 @@
 #include <stdatomic.h>
+#include <assert.h>
 
 struct seqlock_s {
     // Sequence for reader consistency check

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);

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);

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

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);

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);

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);