The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / mcs-lock / testcase.cc
1 #include <stdio.h>
2 #include <threads.h>
3
4 #include "mcs-lock.h"
5
6 /* For data race instrumentation */
7 #include "librace.h"
8
9 struct mcs_mutex *mutex;
10 static uint32_t shared;
11
12 void threadA(void *arg)
13 {
14         mcs_mutex::guard g(mutex);
15         //printf("store: %d\n", 17);
16         //store_32(&shared, 17);
17         mcs_unlock(mutex, &g);
18         //mutex->unlock(&g);
19         mcs_lock(mutex, &g);
20         //mutex->lock(&g);
21         //printf("load: %u\n", load_32(&shared));
22 }
23
24 void threadB(void *arg)
25 {
26         mcs_mutex::guard g(mutex);
27         //printf("load: %u\n", load_32(&shared));
28         mcs_unlock(mutex, &g);
29         //mutex->unlock(&g);
30         mcs_lock(mutex, &g);
31         //mutex->lock(&g);
32         //printf("store: %d\n", 17);
33         //store_32(&shared, 17);
34 }
35
36 int user_main(int argc, char **argv)
37 {
38         thrd_t A, B;
39
40         mutex = new mcs_mutex();
41         /** @Entry */
42         thrd_create(&A, &threadA, NULL);
43         thrd_create(&B, &threadB, NULL);
44         thrd_join(A);
45         thrd_join(B);
46         return 0;
47 }