Able to evaluate predicate expression against a 'context' and generate concrete predi...

diff --git a/funcnode.cc b/funcnode.cc
index e08ca1b850f8a0f3239bdef7fd785677acbd0745..d328a4c5d24f6753fe0faf9338e153bc7284072a 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -321,10 +321,9 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                if (branch->get_func_inst() != next_inst)
                        continue;
 
                if (branch->get_func_inst() != next_inst)
                        continue;
 

-               /* check against predicate expressions */
+               /* Check against predicate expressions */

                bool predicate_correct = true;
                PredExprSet * pred_expressions = branch->get_pred_expressions();
                bool predicate_correct = true;
                PredExprSet * pred_expressions = branch->get_pred_expressions();

-               PredExprSetIter * pred_expr_it = pred_expressions->iterator();

 
                /* Only read and rmw actions my have unset predicate expressions */
                if (pred_expressions->getSize() == 0) {
 
                /* Only read and rmw actions my have unset predicate expressions */
                if (pred_expressions->getSize() == 0) {


@@ -332,33 +331,26 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                        unset_predicates->push_back(branch);
                }
 
                        unset_predicates->push_back(branch);
                }
 

-               while (pred_expr_it->hasNext()) {
-                       pred_expr * pred_expression = pred_expr_it->next();
-                       uint64_t last_read, next_read;
+               SnapVector<struct concrete_pred_expr> concrete_exprs = branch->evaluate(inst_act_map);
+               for (uint i = 0; i < concrete_exprs.size(); i++) {
+                       struct concrete_pred_expr concrete = concrete_exprs[i];
+                       uint64_t next_read;

                        bool equality;
 
                        bool equality;
 

-                       switch(pred_expression->token) {
+                       switch (concrete.token) {

                                case NOPREDICATE:
                                        predicate_correct = true;
                                        break;
                                case EQUALITY:
                                case NOPREDICATE:
                                        predicate_correct = true;
                                        break;
                                case EQUALITY:

-                                       FuncInst * to_be_compared;
-                                       ModelAction * last_act;
-
-                                       to_be_compared = pred_expression->func_inst;
-                                       last_act = inst_act_map->get(to_be_compared);
-
-                                       last_read = last_act->get_reads_from_value();

                                        next_read = next_act->get_reads_from_value();
                                        next_read = next_act->get_reads_from_value();

-                                       equality = (last_read == next_read);
-                                       if (equality != pred_expression->value)
+                                       equality = (next_read == concrete.value);
+                                       if (equality != concrete.equality)

                                                predicate_correct = false;
                                                predicate_correct = false;

-

                                        break;
                                case NULLITY:
                                        next_read = next_act->get_reads_from_value();
                                        equality = ((void*)next_read == NULL);
                                        break;
                                case NULLITY:
                                        next_read = next_act->get_reads_from_value();
                                        equality = ((void*)next_read == NULL);

-                                       if (equality != pred_expression->value)
+                                       if (equality != concrete.equality)

                                                predicate_correct = false;
                                        break;
                                default:
                                                predicate_correct = false;
                                        break;
                                default:

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 98d56f2192fa7872364453fba10227cd04fb038e..4e0d69dbc44b26138844028fa732aeafef1d7dff 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -25,6 +25,8 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {

+//     return random() % rf_set->size();
+

        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 


@@ -46,8 +48,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                prune_writes(tid, selected_branch, rf_set, inst_act_map);
        }
 
                prune_writes(tid, selected_branch, rf_set, inst_act_map);
        }
 

-       // TODO: make this thread sleep if no write satisfies the chosen predicate
-       // if no read satisfies the selected predicate
+       // No write satisfies the selected predicate

        if ( rf_set->size() == 0 ) {
                Thread * read_thread = execution->get_thread(tid);
                model_print("the %d read action of thread %d is unsuccessful\n", read->get_seq_number(), read_thread->get_id());
        if ( rf_set->size() == 0 ) {
                Thread * read_thread = execution->get_thread(tid);
                model_print("the %d read action of thread %d is unsuccessful\n", read->get_seq_number(), read_thread->get_id());


@@ -56,7 +57,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                read_thread->set_pending(read);
                read->reset_seq_number();
                execution->restore_last_seq_num();
                read_thread->set_pending(read);
                read->reset_seq_number();
                execution->restore_last_seq_num();

-               
+

                conditional_sleep(read_thread);
                return -1;
 /*
                conditional_sleep(read_thread);
                return -1;
 /*


@@ -147,39 +148,30 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
 
        bool pruned = false;
        uint index = 0;
 
        bool pruned = false;
        uint index = 0;

+       SnapVector<struct concrete_pred_expr> concrete_exprs = pred->evaluate(inst_act_map);
+

        while ( index < rf_set->size() ) {
                ModelAction * write_act = (*rf_set)[index];
        while ( index < rf_set->size() ) {
                ModelAction * write_act = (*rf_set)[index];

+               uint64_t write_val = write_act->get_write_value();

                bool satisfy_predicate = true;
 
                bool satisfy_predicate = true;
 

-               PredExprSetIter * pred_expr_it = pred_expressions->iterator();
-               while (pred_expr_it->hasNext()) {
-                       struct pred_expr * expression = pred_expr_it->next();
-                       uint64_t write_val = write_act->get_write_value();
+               for (uint i = 0; i < concrete_exprs.size(); i++) {
+                       struct concrete_pred_expr concrete = concrete_exprs[i];

                        bool equality;
 
                        bool equality;
 

-                       // No predicate, return false
-                       if (expression->token == NOPREDICATE)
-                               return pruned;
-
-                       switch(expression->token) {
+                       switch (concrete.token) {
+                               case NOPREDICATE:
+                                       return false;

                                case EQUALITY:
                                case EQUALITY:

-                                       FuncInst * to_be_compared;
-                                       ModelAction * last_act;
-                                       uint64_t last_read;
-
-                                       to_be_compared = expression->func_inst;
-                                       last_act = inst_act_map->get(to_be_compared);
-                                       last_read = last_act->get_reads_from_value();
-
-                                       equality = (write_val == last_read);
-                                       if (equality != expression->value)
+                                       equality = (write_val == concrete.value);
+                                       if (equality != concrete.equality)

                                                satisfy_predicate = false;
                                        break;
                                case NULLITY:
                                        equality = ((void*)write_val == NULL);
                                                satisfy_predicate = false;
                                        break;
                                case NULLITY:
                                        equality = ((void*)write_val == NULL);

-                                       if (equality != expression->value)
-                                               satisfy_predicate = false;
-                                       break;
+                                        if (equality != concrete.equality)
+                                                satisfy_predicate = false;
+                                        break;

                                default:
                                        model_print("unknown predicate token\n");
                                        break;
                                default:
                                        model_print("unknown predicate token\n");
                                        break;


@@ -231,6 +223,7 @@ Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
        return model->get_thread(curr_tid);
 }
 
        return model->get_thread(curr_tid);
 }
 

+/* Force waking up one of threads paused by Fuzzer */

 void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
 {
        int random_index = random() % paused_thread_set.size();
 void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
 {
        int random_index = random() % paused_thread_set.size();


@@ -245,6 +238,12 @@ void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
        (*numthreads)++;
 }
 
        (*numthreads)++;
 }
 

+/* Notify one of conditional sleeping threads if the desired write is available */
+bool NewFuzzer::notify_conditional_sleep(Thread * thread)
+{
+
+}
+

 bool NewFuzzer::shouldWait(const ModelAction * act)
 {
        return random() & 1;
 bool NewFuzzer::shouldWait(const ModelAction * act)
 {
        return random() & 1;

diff --git a/newfuzzer.h b/newfuzzer.h
index db25cfd8744a8801ba4015de686c7c8199025cf4..d6fa3a4fba861915d0e6cd87e615405d38898158 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -6,16 +6,12 @@
 #include "mymemory.h"
 #include "stl-model.h"
 
 #include "mymemory.h"
 #include "stl-model.h"
 

-typedef HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map_t;
-

 class NewFuzzer : public Fuzzer {
 public:
        NewFuzzer();
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Predicate * get_selected_child_branch(thread_id_t tid);
 class NewFuzzer : public Fuzzer {
 public:
        NewFuzzer();
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Predicate * get_selected_child_branch(thread_id_t tid);

-       void conditional_sleep(Thread * thread);

        bool has_paused_threads();
        bool has_paused_threads();

-       void wake_up_paused_threads(int * threadlist, int * numthreads);

 
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
 
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);


@@ -42,6 +38,10 @@ private:
         * Only used by selectWrite;
         */
        SnapVector<Thread *> paused_thread_set;
         * Only used by selectWrite;
         */
        SnapVector<Thread *> paused_thread_set;

+
+       void conditional_sleep(Thread * thread);
+       void wake_up_paused_threads(int * threadlist, int * numthreads);
+       bool notify_conditional_sleep(Thread * thread);

 };
 
 #endif /* end of __NEWFUZZER_H__ */
 };
 
 #endif /* end of __NEWFUZZER_H__ */

diff --git a/predicate.cc b/predicate.cc
index 5cc0219c4b14e36033953d9d1bc37b8773f583ef..a5ba11c928f661176d47c9feb0e9abc5fe379ec2 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -58,6 +58,39 @@ void Predicate::copy_predicate_expr(Predicate * other)
        }
 }
 
        }
 }
 

+/* Evaluate predicate expressions against the given inst_act_map */
+SnapVector<struct concrete_pred_expr> Predicate::evaluate(inst_act_map_t * inst_act_map)
+{
+       SnapVector<struct concrete_pred_expr> concrete_exprs;
+       PredExprSetIter * it = pred_expressions.iterator();
+
+       while (it->hasNext()) {
+               struct pred_expr * ptr = it->next();
+               uint64_t value = 0;
+
+               switch(ptr->token) {
+                       case NOPREDICATE:
+                               break;
+                       case EQUALITY:
+                               FuncInst * to_be_compared;
+                               ModelAction * last_act;
+
+                               to_be_compared = ptr->func_inst;
+                               last_act = inst_act_map->get(to_be_compared);
+                               value = last_act->get_reads_from_value();
+                               break;
+                       case NULLITY:
+                               break;
+                       default:
+                               break;
+               }
+
+               concrete_exprs.push_back(concrete_pred_expr(ptr->token, value, ptr->value));
+       }
+
+       return concrete_exprs;
+}
+

 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);
 void Predicate::print_predicate()
 {
        model_print("\"%p\" [shape=box, label=\"\n", this);

diff --git a/predicate.h b/predicate.h
index 4243a0d88cc98bc47ece42b96f07839c1bf3fe4c..6c83683dddfdfeff4a3fe502625b77a13695a04e 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -44,6 +44,19 @@ struct half_pred_expr {
        SNAPSHOTALLOC
 };
 
        SNAPSHOTALLOC
 };
 

+struct concrete_pred_expr {
+       concrete_pred_expr(token_t token, uint64_t value, bool equality) :
+               token(token),
+               value(value),
+               equality(equality)
+       {}
+
+       token_t token;
+       uint64_t value;
+       bool equality;
+
+       SNAPSHOTALLOC
+};

 
 class Predicate {
 public:
 
 class Predicate {
 public:


@@ -70,6 +83,8 @@ public:
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
 
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
 

+       SnapVector<struct concrete_pred_expr> evaluate(inst_act_map_t * inst_act_map);
+

        void print_predicate();
        void print_pred_subtree();
 
        void print_predicate();
        void print_pred_subtree();