return model->get_execution_number();
}
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
{
action_list_t *tmp = hash->get(ptr);
if (tmp == NULL) {
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
{
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
return true;
}
+ /* The sleep is literally sleeping */
if (asleep->is_sleep()) {
if (fuzzer->shouldWake(asleep))
return true;
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *thr = get_thread(int_to_id(i));
if (scheduler->is_sleep_set(thr)) {
- if (should_wake_up(curr, thr))
+ if (should_wake_up(curr, thr)) {
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
+ if (thr->get_pending()->is_sleep())
+ thr->set_wakeup_state(true);
+ }
}
}
}
rf_set->push_back(nonatomicstore);
}
+ // Remove writes that violate read modification order
+ for (uint i = 0; i < rf_set->size(); i++) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
+ }
+ }
+
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
if (index == -1) // no feasible write exists
}
break;
}
- case ATOMIC_WAIT:
+ case ATOMIC_WAIT: {
+ /* wake up the other threads */
+ for (unsigned int i = 0;i < get_num_threads();i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
+ }
+
+ /* unlock the lock - after checking who was waiting on it */
+ state->locked = NULL;
+
+ if (fuzzer->shouldWait(curr)) {
+ /* disable this thread */
+ get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+ scheduler->sleep(get_thread(curr));
+ }
+
+ break;
+ }
+ case ATOMIC_TIMEDWAIT:
case ATOMIC_UNLOCK: {
//TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
/* unlock the lock - after checking who was waiting on it */
state->locked = NULL;
-
- if (!curr->is_wait())
- break;/* The rest is only for ATOMIC_WAIT */
-
break;
}
case ATOMIC_NOTIFY_ALL: {
case THREAD_START: {
break;
}
+ case THREAD_SLEEP: {
+ Thread *th = get_thread(curr);
+ th->set_pending(curr);
+ scheduler->add_sleep(th);
+ break;
+ }
default:
break;
}
wake_up_sleeping_actions(curr);
/* Add uninitialized actions to lists */
- if (!second_part_of_rmw && curr->get_type() != NOOP)
+ if (!second_part_of_rmw)
add_uninit_action_to_lists(curr);
SnapVector<ModelAction *> * rf_set = NULL;
rf_set = build_may_read_from(curr);
if (curr->is_read() && !second_part_of_rmw) {
- bool success = process_read(curr, rf_set);
+ process_read(curr, rf_set);
+ delete rf_set;
+
+/* bool success = process_read(curr, rf_set);
delete rf_set;
if (!success)
return curr; // Do not add action to lists
+*/
} else
ASSERT(rf_set == NULL);
/* Add the action to lists */
- if (!second_part_of_rmw && curr->get_type() != NOOP)
+ if (!second_part_of_rmw)
add_action_to_lists(curr);
if (curr->is_write())
*
* @param curr The current action. Must be a read.
* @param rf The ModelAction or Promise that curr reads from. Must be a write.
+ * @param check_only If true, then only check whether the current action satisfies
+ * read modification order or not, without modifiying priorset and canprune.
+ * False by default.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
+ SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
*act < *last_sc_fence_thread_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 4 */
*act < *last_sc_fence_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 6 */
*act < *last_sc_fence_thread_before) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
}
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
} else {
const ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
- priorset->push_back(prevrf);
+ if (!check_only)
+ priorset->push_back(prevrf);
} else {
if (act->get_tid() == curr->get_tid()) {
//Can prune curr from obj list
- *canprune = true;
+ if (!check_only)
+ *canprune = true;
}
}
}
projects / c11tester.git / blobdiff