*/
bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
{
- bool updated = false;
+ while(true) {
- const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
-
- 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();
+ }
}
/**
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())
#include "threads-model.h"
#include "model.h"
-ModelAction * Fuzzer::selectWrite(ModelAction *read, ModelVector<ModelAction *> * rf_set) {
+int Fuzzer::selectWrite(ModelAction *read, ModelVector<ModelAction *> * rf_set) {
int random_index = random() % rf_set->size();
- return (*rf_set)[random_index];
+ return random_index;
}
Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) {
class Fuzzer {
public:
Fuzzer() {}
- ModelAction * selectWrite(ModelAction *read, ModelVector<ModelAction *>* rf_set);
+ int selectWrite(ModelAction *read, ModelVector<ModelAction *>* rf_set);
Thread * selectThread(Node *n, int * threadlist, int numthreads);
Thread * selectNotify(action_list_t * waiters);
MEMALLOC