1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
// Benchmark built by Alex Horn
// cbmc thread_chain_posix.c: assertion violation since we only use regular threads
// cbmc -D_ENABLE_CHAIN_ --unwind 2 thread_chain_posix.c: no assertion violation
// cbmc -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2 thread_chain_posix.c: assertion violation
#include <pthread.h>
#include <assert.h>
#ifndef _ENABLE_MEMORY_BUG_
#include <stdlib.h>
void *malloc(size_t size);
void free(void* ptr);
#endif
// Define _EXPOSE_BUG_ when _ENABLE_CHAIN_ is undefined in
// order to get an executable that shows the effect of
// using thread_chains instead of regular threads.
#if defined(_EXPOSE_BUG_) || defined(_EXPOSE_SANITY_CHECK_)
#include <unistd.h>
#define TINY_DELAY 1
#define SHORT_DELAY 3
#define LONG_DELAY 5
#endif
// ========= Chain library =========
// This struct is not thread-safe itself!
//
// A thread_chain is like a chain of threads `f, g, ...` where `f`
// must terminate before `g` can start to run, and so forth.
struct thread_chain_t
{
// last thread in chain
pthread_t thread;
};
// Public function pointer
typedef void *(*start_routine)(void *);
// Internal
struct thread_chain_args_t
{
// last thread in chain
pthread_t thread;
// function pointer for new thread, never null
start_routine f;
// argument to f, possibly null
void *f_arg;
};
// Internal start routine for a thread in a thread_chain
static void* thread_chain_start_routine(void *ptr)
{
struct thread_chain_args_t *args = (struct thread_chain_args_t *) ptr;
// ignore errors
pthread_join(args->thread, NULL);
assert(args->f != NULL);
void* r = args->f(args->f_arg);
#ifndef _ENABLE_MEMORY_BUG_
free(args);
#endif
pthread_exit(NULL);
return r;
}
// This function is not thread-safe itself!
//
// Create a new thread for `f` where `f(arg)` starts to run as
// soon as the currently running `self->thread` has terminated.
//
// \post: `self->thread` is the newly created thread for `f`
int thread_chain_run(struct thread_chain_t *self, start_routine f, void *arg)
{
#ifdef _ENABLE_MEMORY_BUG_
struct thread_chain_args_t local_args;
struct thread_chain_args_t *args = &local_args;
#else
// since the address of a local variable results
// in undefined behaviour when thread_chain_run returns,
// we allocate a thread_chain_args_t struct instead in
// case thread_chain_start_routine outlives thread_chain_run.
struct thread_chain_args_t *args = malloc(sizeof(struct thread_chain_args_t));
if (!args)
return -1;
#endif
args->thread = self->thread;
args->f = f;
args->f_arg = arg;
return pthread_create(&(self->thread), NULL, thread_chain_start_routine, (void *) args);
}
// ========= Symbolic test =========
char test_global;
void* test_write_a(void *arg)
{
#ifdef _EXPOSE_BUG_
sleep(SHORT_DELAY);
#endif
test_global = 'A';
return NULL;
}
void* test_write_b(void *arg)
{
#ifdef _EXPOSE_SANITY_CHECK_
sleep(SHORT_DELAY);
#endif
test_global = 'B';
return NULL;
}
int main(void)
{
#ifdef _ENABLE_CHAIN_
struct thread_chain_t thread_chain;
thread_chain_run(&thread_chain, test_write_a, NULL);
thread_chain_run(&thread_chain, test_write_b, NULL);
#else
pthread_t a_thread, b_thread;
pthread_create(&a_thread, NULL, test_write_a, NULL);
pthread_create(&b_thread, NULL, test_write_b, NULL);
#endif
#if defined(_EXPOSE_BUG_) || defined(_EXPOSE_SANITY_CHECK_)
sleep(TINY_DELAY);
#endif
char x = test_global;
#if defined(_EXPOSE_BUG_) || defined(_EXPOSE_SANITY_CHECK_)
sleep(LONG_DELAY);
#endif
char y = test_global;
// Verification condition:
//
// If global variable equals 'B', then it cannot change.
//
// It is expected that this implication
// fails if _ENABLE_CHAIN_ is undefined.
assert(x != 'B' || y == 'B');
#ifdef _SANITY_CHECK_
// can be violated regardless of _ENABLE_CHAIN_
assert(x != 'A' || y == 'A');
#endif
#ifdef _ENABLE_CHAIN_
// the other joins happen in the chain of threads
pthread_join(thread_chain.thread, NULL);
#else
pthread_join(a_thread, NULL);
pthread_join(b_thread, NULL);
#endif
return 0;
}
|
