projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
6b01d1c
)
seed random number generator with time
vagrant
author
weiyu
<weiyuluo1232@gmail.com>
Sat, 12 Dec 2020 01:11:26 +0000
(17:11 -0800)
committer
weiyu
<weiyuluo1232@gmail.com>
Sat, 12 Dec 2020 01:11:26 +0000
(17:11 -0800)
libthreads.cc
patch
|
blob
|
history
model.cc
patch
|
blob
|
history
diff --git
a/libthreads.cc
b/libthreads.cc
index 4d61e536c9c4e44d603616d92d205ce0f193a7e5..3ed4937dabe4df8e2feaf79c07b17b6260b14dba 100644
(file)
--- a/
libthreads.cc
+++ b/
libthreads.cc
@@
-12,6
+12,7
@@
*/
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
{
*/
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
{
+ createModelIfNotExist();
struct thread_params params = { start_routine, arg };
/* seq_cst is just a 'don't care' parameter */
model->switch_thread(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)¶ms));
struct thread_params params = { start_routine, arg };
/* seq_cst is just a 'don't care' parameter */
model->switch_thread(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)¶ms));
@@
-20,6
+21,7
@@
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
int thrd_join(thrd_t t)
{
int thrd_join(thrd_t t)
{
+ createModelIfNotExist();
Thread *th = t.priv;
model->switch_thread(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
return 0;
Thread *th = t.priv;
model->switch_thread(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
return 0;
@@
-28,10
+30,12
@@
int thrd_join(thrd_t t)
/** A no-op, for now */
void thrd_yield(void)
{
/** A no-op, for now */
void thrd_yield(void)
{
+ createModelIfNotExist();
model->switch_thread(new ModelAction(THREAD_YIELD, std::memory_order_seq_cst, thread_current(), VALUE_NONE));
}
thrd_t thrd_current(void)
{
model->switch_thread(new ModelAction(THREAD_YIELD, std::memory_order_seq_cst, thread_current(), VALUE_NONE));
}
thrd_t thrd_current(void)
{
+ createModelIfNotExist();
return thread_current()->get_thrd_t();
}
return thread_current()->get_thrd_t();
}
diff --git
a/model.cc
b/model.cc
index 3f811d7d7b11a3ef7c5e7846e58cbbc0a0a4293d..c190e38cacb8c7ccb842957ef07c1c231f3c9bfe 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-22,6
+22,14
@@
ModelChecker *model = NULL;
int inside_model = 0;
ModelChecker *model = NULL;
int inside_model = 0;
+uint64_t get_nanotime()
+{
+ struct timespec currtime;
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+
+ return currtime.tv_nsec;
+}
+
void placeholder(void *) {
ASSERT(0);
}
void placeholder(void *) {
ASSERT(0);
}
@@
-524,12
+532,16
@@
bool ModelChecker::handleChosenThread(Thread *old)
void ModelChecker::startChecker() {
startExecution();
//Need to initial random number generator state to avoid resets on rollback
void ModelChecker::startChecker() {
startExecution();
//Need to initial random number generator state to avoid resets on rollback
- initstate(423121, random_state, sizeof(random_state));
+ //initstate(423121, random_state, sizeof(random_state));
+ uint64_t seed = get_nanotime();
+ srandom(seed);
snapshot = take_snapshot();
//reset random number generator state
snapshot = take_snapshot();
//reset random number generator state
- setstate(random_state);
+ //setstate(random_state);
+ seed = get_nanotime();
+ srandom(seed);
install_trace_analyses(get_execution());
redirect_output();
install_trace_analyses(get_execution());
redirect_output();