#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
+#include "fuzzer.h"
#define INITIAL_THREAD_ID 0
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
- next_backtrack(NULL),
bugs(),
- too_many_reads(false),
- no_valid_reads(false),
bad_synchronization(false),
bad_sc_read(false),
asserted(false)
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
- ModelAction *next_backtrack;
SnapVector<bug_message *> bugs;
- bool too_many_reads;
- bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
bool bad_sc_read;
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m,
- const struct model_params *params,
Scheduler *scheduler,
NodeStack *node_stack) :
model(m),
- params(params),
+ params(NULL),
scheduler(scheduler),
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
thrd_last_fence_release(),
node_stack(node_stack),
priv(new struct model_snapshot_members()),
- mo_graph(new CycleGraph())
+ mo_graph(new CycleGraph()),
+ fuzzer(new Fuzzer())
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
*/
bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
{
- int random_index = random() % rf_set->size();
- bool updated = false;
+ while(true) {
- const ModelAction *rf = (*rf_set)[random_index];
- ASSERT(rf);
-
- mo_graph->startChanges();
-
- updated = r_modification_order(curr, rf);
- read_from(curr, rf);
- mo_graph->commitChanges();
- get_thread(curr)->set_return_value(curr->get_return_value());
- return updated;
+ int index = fuzzer->selectWrite(curr, rf_set);
+ const ModelAction *rf = (*rf_set)[index];
+
+
+ ASSERT(rf);
+
+ mo_graph->startChanges();
+ bool updated = r_modification_order(curr, rf);
+ if (!is_infeasible()) {
+ read_from(curr, rf);
+ mo_graph->commitChanges();
+ get_thread(curr)->set_return_value(curr->get_return_value());
+ return updated;
+ }
+ mo_graph->rollbackChanges();
+ (*rf_set)[index] = rf_set->back();
+ rf_set->pop_back();
+ }
}
/**
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
-
- //BCD -- TOFIX FUZZER
- //THIS SHOULD BE A RANDOM CHOICE
- // int wakeupthread = curr->get_node()->get_misc();
- int wakeupthread = 0;
- action_list_t::iterator it = waiters->begin();
-
- // WL
- if (it == waiters->end())
- break;
-
- advance(it, wakeupthread);
- scheduler->wake(get_thread(*it));
- waiters->erase(it);
+ Thread * thread = fuzzer->selectNotify(waiters);
+ scheduler->wake(thread);
break;
}
break;
}
case PTHREAD_CREATE: {
- (*(pthread_t *)curr->get_location()) = pthread_counter++;
+ (*(uint32_t *)curr->get_location()) = pthread_counter++;
struct pthread_params *params = (struct pthread_params *)curr->get_value();
Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
if (curr->is_read() && !second_part_of_rmw) {
process_read(curr, rf_set);
delete rf_set;
+ } else {
+ ASSERT(rf_set == NULL);
}
if (curr->is_write())
char *ptr = buf;
if (mo_graph->checkForCycles())
ptr += sprintf(ptr, "[mo cycle]");
- if (priv->too_many_reads)
- ptr += sprintf(ptr, "[too many reads]");
- if (priv->no_valid_reads)
- ptr += sprintf(ptr, "[no valid reads-from]");
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
if (priv->bad_sc_read)
bool ModelExecution::is_infeasible() const
{
return mo_graph->checkForCycles() ||
- priv->no_valid_reads ||
- priv->too_many_reads ||
priv->bad_synchronization ||
priv->bad_sc_read;
}
return get_parent_action(tid)->get_cv();
}
+bool valequals(uint64_t val1, uint64_t val2, int size) {
+ switch(size) {
+ case 1:
+ return ((uint8_t)val1) == ((uint8_t)val2);
+ case 2:
+ return ((uint16_t)val1) == ((uint16_t)val2);
+ case 4:
+ return ((uint32_t)val1) == ((uint32_t)val2);
+ case 8:
+ return val1==val2;
+ default:
+ ASSERT(0);
+ return false;
+ }
+}
+
/**
* Build up an initial set of all past writes that this 'read' action may read
* from, as well as any previously-observed future values that must still be valid.
if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
allow_read = false;
+ /* Need to check whether we will have two RMW reading from the same value */
+ if (curr->is_rmwr()) {
+ /* It is okay if we have a failing CAS */
+ if (!curr->is_rmwrcas() ||
+ valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+ //Need to make sure we aren't the second RMW
+ CycleNode * node = mo_graph->getNode_noCreate(act);
+ if (node != NULL && node->getRMW() != NULL) {
+ //we are the second RMW
+ allow_read = false;
+ }
+ }
+ }
+
if (allow_read) {
/* Only add feasible reads */
mo_graph->startChanges();
* @return A Thread reference
*/
Thread * ModelExecution::get_pthread(pthread_t pid) {
- if (pid < pthread_counter + 1) return pthread_map[pid];
+ union {
+ pthread_t p;
+ uint32_t v;
+ } x;
+ x.p = pid;
+ uint32_t thread_id = x.v;
+ if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
else return NULL;
}
return NULL;
}
-/** @return True if the execution has taken too many steps */
-bool ModelExecution::too_many_steps() const
-{
- return params->bound != 0 && priv->used_sequence_numbers > params->bound;
-}
-
/**
* Takes the next step in the execution, if possible.
* @param curr The current step to take
return action_select_next_thread(curr);
}
+Fuzzer * ModelExecution::getFuzzer() {
+ return fuzzer;
+}