experiment with exponential decay model

diff --git a/execution.cc b/execution.cc
index 3a73e353358d52a8a1f307f809d117a746c31545..e1c5e2ddbb06767e13c51d55b230f553d5f2c67d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -300,8 +300,6 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
-               if (index == -1)// no feasible write exists
-                       return false;
 
                ModelAction *rf = (*rf_set)[index];
 
@@ -723,12 +721,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (curr->is_read() && !second_part_of_rmw) {
                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);
 

diff --git a/funcnode.cc b/funcnode.cc
index c1b277e8f26f2a57936a88fbe37e6f7a954104d0..663447bf17fed96f8eea6e8cb02e48d84595c828 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -6,6 +6,7 @@
 #include "concretepredicate.h"
 
 #include "model.h"
+#include <cmath>
 
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
@@ -20,7 +21,9 @@ FuncNode::FuncNode(ModelHistory * history) :
 {
        predicate_tree_entry = new Predicate(NULL, true);
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+
        predicate_tree_exit = new Predicate(NULL, false, true);
+       predicate_tree_exit->alloc_pre_exit_predicates();
        predicate_tree_exit->set_depth(MAX_DEPTH);
 
        /* Snapshot data structures below */
@@ -335,7 +338,10 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                curr_pred->incr_expl_count();
        }
 
-       curr_pred->set_exit(predicate_tree_exit);
+       if (curr_pred->get_exit() == NULL) {
+               // Exit predicate is unset yet
+               curr_pred->set_exit(predicate_tree_exit);
+       }
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
@@ -721,6 +727,67 @@ int FuncNode::compute_distance(FuncNode * target, int max_step)
        return -1;
 }
 
+void FuncNode::assign_base_score()
+{
+       SnapVector<Predicate *> leaves;
+       SnapList<Predicate *> queue;
+       queue.push_front(predicate_tree_entry);
+
+       // assign leaf score
+       while ( !queue.empty() ) {
+               Predicate * node = queue.back();
+               queue.pop_back();
+
+               ModelVector<Predicate *> * children = node->get_children();
+               if (children->empty()) {
+                       node->set_weight(1);
+                       leaves.push_back(node);
+               }
+
+               for (uint i = 0; i < children->size(); i++)
+                       queue.push_front( (*children)[i] );
+       }
+
+       // assign scores for internal nodes;
+       while ( !leaves.empty() ) {
+               Predicate * leaf = leaves.back();
+               leaves.pop_back();
+
+               Predicate * curr = leaf->get_parent();
+               while (curr != NULL) {
+                       if (curr->get_weight() != 0) {
+                               // Has been exlpored
+                               break;
+                       }
+
+                       ModelVector<Predicate *> * children = curr->get_children();
+                       double weight_sum = 0;
+                       bool has_unassigned_node = false;
+
+                       for (uint i = 0; i < children->size(); i++) {
+                               Predicate * child = (*children)[i];
+
+                               // If a child has unassigned weight
+                               double weight = child->get_weight();
+                               if (weight == 0) {
+                                       has_unassigned_node = true;
+                                       break;
+                               } else
+                                       weight_sum += weight;
+                       }
+
+                       if (!has_unassigned_node) {
+                               double average_weight = (double) weight_sum / (double) children->size();
+                               double weight = average_weight * pow(0.9, curr->get_depth());
+                               curr->set_weight(weight);
+                       } else
+                               break;
+
+                       curr = curr->get_parent();
+               }
+       }
+}
+
 void FuncNode::print_predicate_tree()
 {
        model_print("digraph function_%s {\n", func_name);
@@ -728,22 +795,3 @@ void FuncNode::print_predicate_tree()
        predicate_tree_exit->print_predicate();
        model_print("}\n");     // end of graph
 }
-
-void FuncNode::print_val_loc_map()
-{
-/*
-        value_set_iter * val_it = values_may_read_from->iterator();
-        while (val_it->hasNext()) {
-                uint64_t value = val_it->next();
-                model_print("val %llx: ", value);
-
-                loc_set_t * locations = val_loc_map->get(value);
-                loc_set_iter * loc_it = locations->iterator();
-                while (loc_it->hasNext()) {
-                        void * location = loc_it->next();
-                        model_print("%p ", location);
-                }
-                model_print("\n");
-        }
- */
-}

diff --git a/funcnode.h b/funcnode.h
index 473847337e60c5a9b85a8ad9ded6790edf779d14..ea0be0298d81b9a86b591f5666ce1005aa221dd2 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -60,9 +60,8 @@ public:
        ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
        int compute_distance(FuncNode * target, int max_step = MAX_DIST);
 
+       void assign_base_score();
        void print_predicate_tree();
-       void print_val_loc_map();
-       void print_last_read(thread_id_t tid);
 
        MEMALLOC
 private:

diff --git a/history.cc b/history.cc
index a5b437c512992793d6e550a90f2f3f497a5146da..67f873b67b282d3d98e45c4d45d90f77a58821f1 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -579,7 +579,9 @@ void ModelHistory::print_func_node()
        for (uint32_t i = 1;i < func_nodes.size();i++) {
                FuncNode * func_node = func_nodes[i];
 
+               func_node->assign_base_score();
                func_node->print_predicate_tree();
+
 /*
                 func_inst_list_mt * entry_insts = func_node->get_entry_insts();
                 model_print("function %s has entry actions\n", func_node->get_func_name());

diff --git a/predicate.cc b/predicate.cc
index 7710705174860433473b7f8d7a995e198d40a212..eb979f8868a9de8097ca5cbb6c4be24a0bbaa2f8 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -8,6 +8,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) :
        exit_predicate(is_exit),
        does_write(false),
        depth(0),
+       weight(0),
        exploration_count(0),
        store_visible_count(0),
        total_checking_count(0),
@@ -60,6 +61,22 @@ void Predicate::set_parent(Predicate * parent_pred)
        depth = parent_pred->get_depth() + 1;
 }
 
+void Predicate::set_exit(Predicate * exit_pred)
+{
+       exit = exit_pred;
+       exit_pred->add_pre_exit_predicate(this);
+}
+
+void Predicate::alloc_pre_exit_predicates()
+{
+       pre_exit_predicates = new ModelVector<Predicate *>();
+}
+
+void Predicate::add_pre_exit_predicate(Predicate * pred)
+{
+       pre_exit_predicates->push_back(pred);
+}
+
 void Predicate::copy_predicate_expr(Predicate * other)
 {
        PredExprSet * other_pred_expressions = other->get_pred_expressions();
@@ -136,7 +153,7 @@ void Predicate::print_predicate()
                return;
        }
 
-       model_print("depth: %d\n", depth);
+       model_print("depth: %u; weight: %g\n", depth, weight);
 
        func_inst->print();
 

diff --git a/predicate.h b/predicate.h
index 97e495de8a1024c6fe2d8e44dff7d93bbaa54d3a..0512835f6aadfbcab4ce7689dfd3e43ce689a863 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -23,8 +23,9 @@ public:
        void add_predicate_expr(token_t token, FuncInst * func_inst, bool value);
        void add_child(Predicate * child);
        void set_parent(Predicate * parent_pred);
-       void set_exit(Predicate * exit_pred) { exit = exit_pred; }
+       void set_exit(Predicate * exit_pred);
        void add_backedge(Predicate * back_pred) { backedges.add(back_pred); }
+       void set_weight(double weight_) { weight = weight_; }
        void copy_predicate_expr(Predicate * other);
 
        Predicate * get_single_child(FuncInst * inst);
@@ -32,10 +33,14 @@ public:
        Predicate * get_parent() { return parent; }
        Predicate * get_exit() { return exit; }
        PredSet * get_backedges() { return &backedges; }
+       double get_weight() { return weight; }
 
        bool is_entry_predicate() { return entry_predicate; }
        void set_entry_predicate() { entry_predicate = true; }
 
+       void alloc_pre_exit_predicates();
+       void add_pre_exit_predicate(Predicate * pred);
+
        /* Whether func_inst does write or not */
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
@@ -65,6 +70,7 @@ private:
 
        /* Height of this predicate node in the predicate tree */
        uint32_t depth;
+       double weight;
 
        uint32_t exploration_count;
        uint32_t store_visible_count;
@@ -78,6 +84,9 @@ private:
        Predicate * parent;
        Predicate * exit;
 
+       /* Predicates precede exit nodes. Only used by exit predicates */
+       ModelVector<Predicate *> * pre_exit_predicates;
+
        /* May have multiple back edges, e.g. nested loops */
        PredSet backedges;
 };