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
|
// Benchmark built by Alex Horn
// expect assertion violation if and only if
// - cbmc -D_SANITY_CHECK_ thread_chain_cbmc.c
#include <assert.h>
#ifndef NULL
#define NULL 0
#endif
// ========= Thread Chain library =========
// Internal thread local identifier of a thread
// The benefit of local thread identifiers is that CBMC is more likely
// to be able to perform constant propagation on thread identifiers.
// The downside is that the public interface requires the user to
// choose thread identifiers such that they are globally unique.
typedef unsigned long thread_id_t;
// Internal unbounded array indexed by local thread identifiers
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
// A thread_chain is like a chain of threads `f, g, ...` where `f`
// must terminate before `g` can start to run, and so forth.
typedef thread_id_t thread_chain_t;
// Initialize thread_chain
//
// Note that `init_thread_id` will be incremented on each `thread_chain_run`
// call in order to to generate a new thread identifier. It is the
// responsibility of the caller to ensure that the resulting thread
// identifiers are globally unique.
//
// So pick `init_thread_id` according to how many threads will be
// spawned across different threads in the system.
thread_chain_t make_thread_chain(thread_id_t init_thread_id)
{
// the first thread in the chain of threads is ready to to run
__CPROVER_threads_exited[init_thread_id] = 1;
return (thread_chain_t) init_thread_id;
}
// Public function pointer
typedef void (*start_routine)(void *);
// Internal start routine for a new thread in a thread_chain that waits on `thread_id`
//
// \pre: `f` is not null
static void thread_chain_start_routine(thread_id_t thread_id, start_routine f, void *arg)
{
__CPROVER_assume(__CPROVER_threads_exited[thread_id]);
f(arg);
}
// Create a new thread for `f` where `f(arg)` starts to run as
// soon as the currently running thread in `thread_chain` has terminated.
int thread_chain_run(thread_chain_t *thread_chain, start_routine f, void *arg)
{
assert(f != NULL);
thread_id_t current_thread_id, thread_id;
__CPROVER_atomic_begin();
current_thread_id = (thread_id_t) *thread_chain;
thread_id = current_thread_id + 1;
*thread_chain = (thread_chain_t) thread_id;
__CPROVER_atomic_end();
__CPROVER_ASYNC_1: thread_chain_start_routine(current_thread_id, f, arg),
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
"WWcumul", "RRcumul", "RWcumul", "WRcumul"),
__CPROVER_threads_exited[thread_id] = 1;
}
// ========= Symbolic test =========
char test_global;
void test_write_a(void *arg)
{
test_global = 'A';
}
void test_write_b(void *arg)
{
test_global = 'B';
}
int main(void)
{
thread_chain_t thread_chain = make_thread_chain(0UL);
thread_chain_run(&thread_chain, test_write_a, NULL);
thread_chain_run(&thread_chain, test_write_b, NULL);
char x = test_global;
char y = test_global;
// Verification condition:
//
// If global variable equals 'B', then it cannot change.
assert(x != 'B' || y == 'B');
#ifdef _SANITY_CHECK_
// can be violated regardless of _ENABLE_CHAIN_
assert(x != 'A' || y == 'A');
#endif
return 0;
}
|
