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();
- PredExprSetIter * pred_expr_it = pred_expressions->iterator();
/* Only read and rmw actions my have unset predicate expressions */
if (pred_expressions->getSize() == 0) {
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;
- switch(pred_expression->token) {
+ switch (concrete.token) {
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();
- equality = (last_read == next_read);
- if (equality != pred_expression->value)
+ equality = (next_read == concrete.value);
+ if (equality != concrete.equality)
predicate_correct = false;
-
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:
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);
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());
read_thread->set_pending(read);
read->reset_seq_number();
execution->restore_last_seq_num();
-
+
conditional_sleep(read_thread);
return -1;
/*
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];
+ uint64_t write_val = write_act->get_write_value();
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;
- // No predicate, return false
- if (expression->token == NOPREDICATE)
- return pruned;
-
- switch(expression->token) {
+ switch (concrete.token) {
+ case NOPREDICATE:
+ return false;
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);
- if (equality != expression->value)
- satisfy_predicate = false;
- break;
+ if (equality != concrete.equality)
+ satisfy_predicate = false;
+ break;
default:
model_print("unknown predicate token\n");
break;
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();
(*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;
#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);
- void conditional_sleep(Thread * thread);
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);
* 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__ */
}
}
+/* 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);
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:
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();