#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
+#include "history.h"
#include "fuzzer.h"
#define INITIAL_THREAD_ID 0
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
- pthread_counter(0),
+ pthread_counter(1),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
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 */
return tmp;
}
-action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
-{
- SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
- if (wrv==NULL)
- return NULL;
- unsigned int thread=id_to_int(tid);
- if (thread < wrv->size())
- return &(*wrv)[thread];
- else
- return NULL;
-}
-
/** @return a thread ID for a new Thread */
thread_id_t ModelExecution::get_next_id()
{
* @param rf_set is the set of model actions we can possibly read from
* @return True if processing this read updates the mo_graph.
*/
-void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
{
SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
while(true) {
ASSERT(rf);
-
- if (r_modification_order(curr, rf, priorset)) {
+ bool canprune = false;
+ if (r_modification_order(curr, rf, priorset, &canprune)) {
for(unsigned int i=0;i<priorset->size();i++) {
mo_graph->addEdge((*priorset)[i], rf);
}
read_from(curr, rf);
get_thread(curr)->set_return_value(curr->get_return_value());
delete priorset;
+ if (canprune && curr->get_type() == ATOMIC_READ) {
+ int tid = id_to_int(curr->get_tid());
+ (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+ }
return;
}
priorset->clear();
}
//otherwise fall into the lock case
case ATOMIC_LOCK: {
- if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
- assert_bug("Lock access before initialization");
+ //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
+ //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ // assert_bug("Lock access before initialization");
state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
}
case ATOMIC_WAIT:
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...
+
/* wake up the other threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *t = get_thread(int_to_id(i));
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
- Thread * thread = fuzzer->selectNotify(waiters);
- scheduler->wake(thread);
+ if (waiters->size() != 0) {
+ Thread * thread = fuzzer->selectNotify(waiters);
+ scheduler->wake(thread);
+ }
break;
}
*/
void ModelExecution::process_write(ModelAction *curr)
{
-
w_modification_order(curr);
-
-
get_thread(curr)->set_return_value(VALUE_NONE);
}
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
- if (!second_part_of_rmw)
+ if (!second_part_of_rmw && curr->get_type() != NOOP)
add_action_to_lists(curr);
- SnapVector<ModelAction *> * rf_set = NULL;
+ SnapVector<const ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
rf_set = build_may_read_from(curr);
* @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 ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
- ModelAction *last_sc_write = NULL;
- if (curr->is_seqcst())
- last_sc_write = get_last_seq_cst_write(curr);
+ int tid = curr->get_tid();
+ ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++) {
- /* Last SC fence in thread i */
+ for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
+ /* Last SC fence in thread tid */
ModelAction *last_sc_fence_thread_local = NULL;
- if (int_to_id((int)i) != curr->get_tid())
- last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+ if (i != 0)
+ last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
- /* Last SC fence in thread i, before last SC fence in current thread */
+ /* Last SC fence in thread tid, before last SC fence in current thread */
ModelAction *last_sc_fence_thread_before = NULL;
if (last_sc_fence_local)
- last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
+
+ //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
+ if (prev_same_thread != NULL &&
+ (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+ (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+ continue;
+ }
/* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
+ action_list_t *list = &(*thrd_lists)[tid];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
* before" curr
*/
if (act->happens_before(curr)) {
+ if (i==0) {
+ if (last_sc_fence_local == NULL ||
+ (*last_sc_fence_local < *prev_same_thread)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
if (mo_graph->checkReachable(rf, prevrf))
return false;
priorset->push_back(prevrf);
+ } else {
+ if (act->get_tid() == curr->get_tid()) {
+ //Can prune curr from obj list
+ *canprune = true;
+ }
}
}
break;
*/
ClockVector * ModelExecution::get_cv(thread_id_t tid) const
{
- return get_parent_action(tid)->get_cv();
+ ModelAction *firstaction=get_parent_action(tid);
+ return firstaction != NULL ? firstaction->get_cv() : NULL;
}
bool valequals(uint64_t val1, uint64_t val2, int size) {
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
+ SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
/* Iterate over all threads */
for (i = 0;i < thrd_lists->size();i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ const ModelAction *act = *rit;
/* Only consider 'write' actions */
- if (!act->is_write() || act == curr)
+ if (!act->is_write()) {
+ if (act != curr && act->is_read() && act->happens_before(curr)) {
+ const ModelAction *tmp = act->get_reads_from();
+ if (((unsigned int) id_to_int(tmp->get_tid()))==i)
+ act = tmp;
+ else
+ break;
+ } else
+ continue;
+ }
+
+ if (act == curr)
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
/* Do not split atomic RMW */
if (curr->is_rmwr())
return get_thread(curr);
- if (curr->is_write()) {
- std::memory_order order = curr->get_mo();
- switch(order) {
- case std::memory_order_relaxed:
- return get_thread(curr);
- case std::memory_order_release:
- return get_thread(curr);
- default:
- return NULL;
- }
- }
-
/* Follow CREATE with the created thread */
/* which is not needed, because model.cc takes care of this */
if (curr->get_type() == THREAD_CREATE)
curr = check_current_action(curr);
ASSERT(curr);
+ // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() );
+ model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
+
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
projects / c11tester.git / blobdiff