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
|
// ©2013 Cameron Desrochers.
// Distributed under the simplified BSD license (see the LICENSE file that
// should have come with this file).
#include "model-checker/include/threads.h"
#include "corealgo.h"
void producer_thread(void*)
{
enqueue(1234);
}
void consumer_thread(void*)
{
int element;
bool result = try_dequeue(element);
MODEL_ASSERT(!result || element == 1234);
if (result) {
MODEL_ASSERT(!try_dequeue(element));
}
}
int user_main(int, char**)
{
init();
thrd_t p, c;
thrd_create(&p, &producer_thread, nullptr);
thrd_create(&c, &consumer_thread, nullptr);
thrd_join(p);
thrd_join(c);
return 0;
}
|
