datarace.o impatomic.o cmodelint.o \
snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
- sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o newfuzzer.o \
- concretepredicate.o waitobj.o hashfunction.o pipe.o epoll.o actionlist.o
+ sleeps.o printf.o \
+ hashfunction.o pipe.o epoll.o actionlist.o
CPPFLAGS += -Iinclude -I.
LDFLAGS := -ldl -lrt -rdynamic -lpthread
Benchmarks
-------------------
-Many simple tests are located in the `test/` directory. These are
-manually instrumented and can just be run.
-
-You may also want to try the larger benchmarks (distributed
-separately). These require LLVM to instrument.
-
+The benchmarks are distributed separately. These require LLVM to instrument.
+You may also follow the steps in the Artifact Appendix of our paper (https://dl.acm.org/doi/abs/10.1145/3445814.3446711) to run the benchmarks.
Running your own code
---------------------
#include "model.h"
#include "execution.h"
#include "action.h"
-#include "history.h"
#include "cmodelint.h"
#include "snapshot-interface.h"
#include "threads-model.h"
*/
void cds_func_entry(const char * funcName) {
-#ifdef NEWFUZZER
- createModelIfNotExist();
- thread_id_t tid = thread_current_id();
- uint32_t func_id;
-
- ModelHistory *history = model->get_history();
- if ( !history->getFuncMap()->contains(funcName) ) {
- // add func id to func map
- func_id = history->get_func_counter();
- history->incr_func_counter();
- history->getFuncMap()->put(funcName, func_id);
-
- // add func id to reverse func map
- ModelVector<const char *> * func_map_rev = history->getFuncMapRev();
- if ( func_map_rev->size() <= func_id )
- func_map_rev->resize( func_id + 1 );
-
- func_map_rev->at(func_id) = funcName;
- } else {
- func_id = history->getFuncMap()->get(funcName);
- }
-
- history->enter_function(func_id, tid);
-#endif
}
void cds_func_exit(const char * funcName) {
-#ifdef NEWFUZZER
- createModelIfNotExist();
- thread_id_t tid = thread_current_id();
- uint32_t func_id;
-
- ModelHistory *history = model->get_history();
- func_id = history->getFuncMap()->get(funcName);
-/*
- * func_id not found; this could happen in the case where a function calls cds_func_entry
- * when the model has been defined yet, but then an atomic inside the function initializes
- * the model. And then cds_func_exit is called upon the function exiting.
- *
- */
- if (func_id == 0)
- return;
-
- history->exit_function(func_id, tid);
-#endif
}
+++ /dev/null
-#include "concretepredicate.h"
-
-ConcretePredicate::ConcretePredicate(thread_id_t tid) :
- tid(tid),
- expressions()
-{}
-
-void ConcretePredicate::add_expression(token_t token, uint64_t value, bool equality)
-{
- expressions.push_back(concrete_pred_expr(token, value, equality));
-}
+++ /dev/null
-#ifndef __CONCRETE_PREDICATE_H__
-#define __CONCRETE_PREDICATE_H__
-
-#include <inttypes.h>
-#include "modeltypes.h"
-#include "classlist.h"
-#include "predicatetypes.h"
-
-class ConcretePredicate {
-public:
- ConcretePredicate(thread_id_t tid);
- ~ConcretePredicate() {}
-
- void add_expression(token_t token, uint64_t value, bool equality);
- SnapVector<struct concrete_pred_expr> * getExpressions() { return &expressions; }
- void set_location(void * loc) { location = loc; }
- void * get_location() { return location; }
- thread_id_t get_tid() { return tid; }
-
- SNAPSHOTALLOC
-private:
- thread_id_t tid;
- void * location;
- SnapVector<struct concrete_pred_expr> expressions;
-};
-
-#endif /* __CONCRETE_PREDICATE_H */
#define SHADOWBASETABLES 4
/** Enable debugging assertions (via ASSERT()) */
-#define CONFIG_ASSERT
+//#define CONFIG_ASSERT
/** Enable mitigations against fork handlers that call into locks... */
#define FORK_HANDLER_HACK
//#define COLLECT_STAT
#define REPORT_DATA_RACES
+//#define PRINT_TRACE
+
#endif
#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
-#include "history.h"
#include "fuzzer.h"
-#include "newfuzzer.h"
#ifdef COLLECT_STAT
static unsigned int atomic_load_count = 0;
thrd_last_fence_release(),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
-#ifdef NEWFUZZER
- fuzzer(new NewFuzzer()),
-#else
fuzzer(new Fuzzer()),
-#endif
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
add_normal_write_to_lists(act);
add_write_to_lists(act);
w_modification_order(act);
-#ifdef NEWFUZZER
- model->get_history()->process_action(act, act->get_tid());
-#endif
return act;
}
ASSERT(curr);
/* Process this action in ModelHistory for records */
-#ifdef NEWFUZZER
- model->get_history()->process_action( curr, curr->get_tid() );
-#endif
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
+++ /dev/null
-#include "funcinst.h"
-#include "model.h"
-
-FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
- single_location(true),
- execution_number(0),
- associated_reads(),
- thrd_markers()
-{
- ASSERT(act);
- ASSERT(func_node);
- this->position = act->get_position();
- this->location = act->get_location();
- this->type = act->get_type();
- this->order = act->get_mo();
- this->func_node = func_node;
-}
-
-/* @param other Preceding FuncInst in the same execution trace
- * Add other to predecessors if it has been added
- *
- * @return false: other is already in predecessors
- * true : other is added to precedessors
- */
-bool FuncInst::add_pred(FuncInst * other)
-{
- mllnode<FuncInst*> * it;
- for (it = predecessors.begin();it != NULL;it=it->getNext()) {
- FuncInst * inst = it->getVal();
- if (inst == other)
- return false;
- }
-
- predecessors.push_back(other);
- return true;
-}
-
-bool FuncInst::add_succ(FuncInst * other)
-{
- mllnode<FuncInst*>* it;
- for (it = successors.begin();it != NULL;it=it->getNext()) {
- FuncInst * inst = it->getVal();
- if ( inst == other )
- return false;
- }
-
- successors.push_back(other);
- return true;
-}
-
-void FuncInst::set_associated_read(thread_id_t tid, int index, uint32_t marker, uint64_t read_val)
-{
- int thread_id = id_to_int(tid);
-
- if (associated_reads.size() < (uint) thread_id + 1) {
- int old_size = associated_reads.size();
- int new_size = thread_id + 1;
-
- associated_reads.resize(new_size);
- thrd_markers.resize(new_size);
-
- for (int i = old_size;i < new_size;i++ ) {
- associated_reads[i] = new ModelVector<uint64_t>();
- thrd_markers[i] = new ModelVector<uint32_t>();
- }
- }
-
- ModelVector<uint64_t> * read_values = associated_reads[thread_id];
- ModelVector<uint32_t> * markers = thrd_markers[thread_id];
- if (read_values->size() < (uint) index + 1) {
- int old_size = read_values->size();
-
- for (int i = old_size;i < index + 1;i++) {
- read_values->push_back(VALUE_NONE);
- markers->push_back(0);
- }
- }
-
- (*read_values)[index] = read_val;
- (*markers)[index] = marker;
-}
-
-uint64_t FuncInst::get_associated_read(thread_id_t tid, int index, uint32_t marker)
-{
- int thread_id = id_to_int(tid);
-
- if ( (*thrd_markers[thread_id])[index] == marker)
- return (*associated_reads[thread_id])[index];
- else
- return VALUE_NONE;
-}
-
-/* Search the FuncInst that has the same type as act in the collision list */
-FuncInst * FuncInst::search_in_collision(ModelAction *act)
-{
- action_type type = act->get_type();
-
- mllnode<FuncInst*> * it;
- for (it = collisions.begin();it != NULL;it = it->getNext()) {
- FuncInst * inst = it->getVal();
- if (inst->get_type() == type)
- return inst;
- }
- return NULL;
-}
-
-void FuncInst::add_to_collision(FuncInst * inst)
-{
- collisions.push_back(inst);
-}
-
-/* Note: is_read() is equivalent to ModelAction::is_read() */
-bool FuncInst::is_read() const
-{
- return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW;
-}
-
-/* Note: because of action type conversion in ModelExecution
- * is_write() <==> pure writes (excluding rmw) */
-bool FuncInst::is_write() const
-{
- return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == NONATOMIC_WRITE;
-}
-
-void FuncInst::print()
-{
- model_print("func inst - pos: %s, loc: %p, type: %d,\n", position, location, type);
-}
+++ /dev/null
-#ifndef __FUNCINST_H__
-#define __FUNCINST_H__
-
-#include "action.h"
-#include "classlist.h"
-#include "hashtable.h"
-#include "threads-model.h"
-
-typedef ModelList<FuncInst *> func_inst_list_mt;
-
-class FuncInst {
-public:
- FuncInst(ModelAction *act, FuncNode *func_node);
- ~FuncInst();
-
- const char * get_position() const { return position; }
-
- void * get_location() const { return location; }
- void set_location(void * loc) { location = loc; }
-
- action_type get_type() const { return type; }
- memory_order get_mo() const { return order; }
- FuncNode * get_func_node() const { return func_node; }
-
- bool add_pred(FuncInst * other);
- bool add_succ(FuncInst * other);
-
- FuncInst * search_in_collision(ModelAction *act);
- void add_to_collision(FuncInst * inst);
-
- func_inst_list_mt * get_preds() { return &predecessors; }
- func_inst_list_mt * get_succs() { return &successors; }
-
- bool is_read() const;
- bool is_write() const;
- bool is_single_location() { return single_location; }
- void not_single_location() { single_location = false; }
-
- void set_execution_number(int new_number) { execution_number = new_number; }
- int get_execution_number() { return execution_number; }
-
- void set_associated_read(thread_id_t tid, int index, uint32_t marker, uint64_t read_val);
- uint64_t get_associated_read(thread_id_t tid, int index, uint32_t marker);
-
- void print();
-
- MEMALLOC
-private:
- const char * position;
-
- /* Atomic operations with the same source line number may act at different
- * memory locations, such as the next field of the head pointer in ms-queue.
- * location only stores the memory location when this FuncInst was constructed.
- */
- void * location;
-
- /* NOTE: for rmw actions, func_inst and act may have different
- * action types because of action type conversion in ModelExecution */
- action_type type;
-
- memory_order order;
- FuncNode * func_node;
-
- bool single_location;
- int execution_number;
-
- ModelVector< ModelVector<uint64_t> * > associated_reads;
- ModelVector< ModelVector<uint32_t> * > thrd_markers;
-
- /**
- * Collisions store a list of FuncInsts with the same position
- * but different action types. For example,
- * <code>volatile int x; x++;</code> produces read and write
- * actions with the same position.
- */
- func_inst_list_mt collisions;
-
- func_inst_list_mt predecessors;
- func_inst_list_mt successors;
-};
-
-#endif /* __FUNCINST_H__ */
+++ /dev/null
-#include "action.h"
-#include "history.h"
-#include "funcnode.h"
-#include "funcinst.h"
-#include "predicate.h"
-#include "concretepredicate.h"
-
-#include "model.h"
-#include "execution.h"
-#include "newfuzzer.h"
-#include <cmath>
-
-FuncNode::FuncNode(ModelHistory * history) :
- func_id(0),
- func_name(NULL),
- history(history),
- inst_counter(1),
- marker(1),
- exit_count(0),
- thrd_markers(),
- thrd_recursion_depth(),
- func_inst_map(),
- inst_list(),
- entry_insts(),
- thrd_inst_pred_maps(),
- thrd_inst_id_maps(),
- thrd_loc_inst_maps(),
- likely_null_set(),
- thrd_predicate_tree_position(),
- thrd_predicate_trace(),
- edge_table(32),
- out_edges()
-{
- 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->set_depth(MAX_DEPTH);
-
- /* Snapshot data structures below */
- read_locations = new loc_set_t();
- write_locations = new loc_set_t();
- val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
- loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-
- //values_may_read_from = new value_set_t();
-}
-
-/* Reallocate snapshotted memories when new executions start */
-void FuncNode::set_new_exec_flag()
-{
- read_locations = new loc_set_t();
- write_locations = new loc_set_t();
- val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
- loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-
- //values_may_read_from = new value_set_t();
-}
-
-/* Check whether FuncInst with the same type, position, and location
- * as act has been added to func_inst_map or not. If not, add it.
- */
-void FuncNode::add_inst(ModelAction *act)
-{
- ASSERT(act);
- const char * position = act->get_position();
-
- /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
- * actions are not tagged with their source line numbers
- */
- if (position == NULL)
- return;
-
- FuncInst * func_inst = func_inst_map.get(position);
-
- /* This position has not been inserted into hashtable before */
- if (func_inst == NULL) {
- func_inst = create_new_inst(act);
- func_inst_map.put(position, func_inst);
- return;
- }
-
- /* Volatile variables that use ++ or -- syntax may result in read and write actions with the same position */
- if (func_inst->get_type() != act->get_type()) {
- FuncInst * collision_inst = func_inst->search_in_collision(act);
-
- if (collision_inst == NULL) {
- collision_inst = create_new_inst(act);
- func_inst->add_to_collision(collision_inst);
- return;
- } else {
- func_inst = collision_inst;
- }
- }
-
- ASSERT(func_inst->get_type() == act->get_type());
- int curr_execution_number = model->get_execution_number();
-
- /* Reset locations when new executions start */
- if (func_inst->get_execution_number() != curr_execution_number) {
- func_inst->set_location(act->get_location());
- func_inst->set_execution_number(curr_execution_number);
- }
-
- /* Mark the memory location of such inst as not unique */
- if (func_inst->get_location() != act->get_location())
- func_inst->not_single_location();
-}
-
-FuncInst * FuncNode::create_new_inst(ModelAction * act)
-{
- FuncInst * func_inst = new FuncInst(act, this);
- int exec_num = model->get_execution_number();
- func_inst->set_execution_number(exec_num);
-
- inst_list.push_back(func_inst);
-
- return func_inst;
-}
-
-
-/* Get the FuncInst with the same type, position, and location
- * as act
- *
- * @return FuncInst with the same type, position, and location as act */
-FuncInst * FuncNode::get_inst(ModelAction *act)
-{
- ASSERT(act);
- const char * position = act->get_position();
-
- /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
- * actions are not tagged with their source line numbers
- */
- if (position == NULL)
- return NULL;
-
- FuncInst * inst = func_inst_map.get(position);
- if (inst == NULL)
- return NULL;
-
- action_type inst_type = inst->get_type();
- action_type act_type = act->get_type();
-
- if (inst_type == act_type) {
- return inst;
- }
- /* RMWRCAS actions are converted to RMW or READ actions */
- else if (inst_type == ATOMIC_RMWRCAS &&
- (act_type == ATOMIC_RMW || act_type == ATOMIC_READ)) {
- return inst;
- }
- /* Return the FuncInst in the collision list */
- else {
- return inst->search_in_collision(act);
- }
-}
-
-void FuncNode::add_entry_inst(FuncInst * inst)
-{
- if (inst == NULL)
- return;
-
- mllnode<FuncInst *> * it;
- for (it = entry_insts.begin();it != NULL;it = it->getNext()) {
- if (inst == it->getVal())
- return;
- }
-
- entry_insts.push_back(inst);
-}
-
-void FuncNode::function_entry_handler(thread_id_t tid)
-{
- init_marker(tid);
- init_local_maps(tid);
- init_predicate_tree_data_structure(tid);
-}
-
-void FuncNode::function_exit_handler(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
-
- reset_local_maps(tid);
-
- thrd_recursion_depth[thread_id]--;
- thrd_markers[thread_id]->pop_back();
-
- Predicate * exit_pred = get_predicate_tree_position(tid);
- if (exit_pred->get_exit() == NULL) {
- // Exit predicate is unset yet
- exit_pred->set_exit(predicate_tree_exit);
- }
-
- update_predicate_tree_weight(tid);
- reset_predicate_tree_data_structure(tid);
-
- exit_count++;
- //model_print("exit count: %d\n", exit_count);
-
-// print_predicate_tree();
-}
-
-/**
- * @brief Convert ModelAdtion list to FuncInst list
- * @param act_list A list of ModelActions
- */
-void FuncNode::update_tree(ModelAction * act)
-{
- bool should_process = act->is_read() || act->is_write();
- if (!should_process)
- return;
-
- HashTable<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
-
- /* build inst_list from act_list for later processing */
-// func_inst_list_t inst_list;
-
- FuncInst * func_inst = get_inst(act);
- void * loc = act->get_location();
-
- if (func_inst == NULL)
- return;
-
-// inst_list.push_back(func_inst);
-
- if (act->is_write()) {
- if (!write_locations->contains(loc)) {
- write_locations->add(loc);
- history->update_loc_wr_func_nodes_map(loc, this);
- }
- }
-
- if (act->is_read()) {
- /* If func_inst may only read_from a single location, then:
- *
- * The first time an action reads from some location,
- * import all the values that have been written to this
- * location from ModelHistory and notify ModelHistory
- * that this FuncNode may read from this location.
- */
- if (!read_locations->contains(loc) && func_inst->is_single_location()) {
- read_locations->add(loc);
- value_set_t * write_values = write_history->get(loc);
- add_to_val_loc_map(write_values, loc);
- history->update_loc_rd_func_nodes_map(loc, this);
- }
-
- // Keep a has-been-zero-set record
- if ( likely_reads_from_null(act) )
- likely_null_set.put(func_inst, true);
- }
-
-// update_inst_tree(&inst_list); TODO
-
- update_predicate_tree(act);
-}
-
-/**
- * @brief Link FuncInsts in inst_list - add one FuncInst to another's predecessors and successors
- * @param inst_list A list of FuncInsts
- */
-void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
-{
- if (inst_list == NULL)
- return;
- else if (inst_list->size() == 0)
- return;
-
- /* start linking */
- sllnode<FuncInst *>* it = inst_list->begin();
- sllnode<FuncInst *>* prev;
-
- /* add the first instruction to the list of entry insts */
- FuncInst * entry_inst = it->getVal();
- add_entry_inst(entry_inst);
-
- it = it->getNext();
- while (it != NULL) {
- prev = it->getPrev();
-
- FuncInst * prev_inst = prev->getVal();
- FuncInst * curr_inst = it->getVal();
-
- prev_inst->add_succ(curr_inst);
- curr_inst->add_pred(prev_inst);
-
- it = it->getNext();
- }
-}
-
-void FuncNode::update_predicate_tree(ModelAction * next_act)
-{
- thread_id_t tid = next_act->get_tid();
- int thread_id = id_to_int(tid);
- uint32_t this_marker = thrd_markers[thread_id]->back();
- int recursion_depth = thrd_recursion_depth[thread_id];
-
- loc_inst_map_t * loc_inst_map = thrd_loc_inst_maps[thread_id]->back();
- inst_pred_map_t * inst_pred_map = thrd_inst_pred_maps[thread_id]->back();
- inst_id_map_t * inst_id_map = thrd_inst_id_maps[thread_id]->back();
-
- Predicate * curr_pred = get_predicate_tree_position(tid);
- NewFuzzer * fuzzer = (NewFuzzer *)model->get_execution()->getFuzzer();
- Predicate * selected_branch = fuzzer->get_selected_child_branch(tid);
-
- bool amended;
- while (true) {
- FuncInst * next_inst = get_inst(next_act);
-
- Predicate * unset_predicate = NULL;
- bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate);
-
- // A branch with unset predicate expression is detected
- if (!branch_found && unset_predicate != NULL) {
- amended = amend_predicate_expr(curr_pred, next_inst, next_act);
- if (amended)
- continue;
- else {
- curr_pred = unset_predicate;
- branch_found = true;
- }
- }
-
- // Detect loops
- if (!branch_found && inst_id_map->contains(next_inst)) {
- FuncInst * curr_inst = curr_pred->get_func_inst();
- uint32_t curr_id = inst_id_map->get(curr_inst);
- uint32_t next_id = inst_id_map->get(next_inst);
-
- if (curr_id >= next_id) {
- Predicate * old_pred = inst_pred_map->get(next_inst);
- Predicate * back_pred = old_pred->get_parent();
-
- // Add to the set of backedges
- curr_pred->add_backedge(back_pred);
- curr_pred = back_pred;
-
- continue;
- }
- }
-
- // Generate new branches
- if (!branch_found) {
- SnapVector<struct half_pred_expr *> half_pred_expressions;
- infer_predicates(next_inst, next_act, &half_pred_expressions);
- generate_predicates(curr_pred, next_inst, &half_pred_expressions);
- continue;
- }
-
- if (next_act->is_write()) {
- curr_pred->set_write(true);
- }
-
- if (next_act->is_read()) {
- /* Only need to store the locations of read actions */
- loc_inst_map->put(next_act->get_location(), next_inst);
- }
-
- inst_pred_map->put(next_inst, curr_pred);
- set_predicate_tree_position(tid, curr_pred);
-
- if (!inst_id_map->contains(next_inst))
- inst_id_map->put(next_inst, inst_counter++);
-
- curr_pred->incr_expl_count();
- add_predicate_to_trace(tid, curr_pred);
- if (next_act->is_read())
- next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
-
- break;
- }
-
- // A check
- if (next_act->is_read()) {
-// if (selected_branch != NULL && !amended)
-// ASSERT(selected_branch == curr_pred);
- }
-}
-
-/* Given curr_pred and next_inst, find the branch following curr_pred that
- * contains next_inst and the correct predicate.
- * @return true if branch found, false otherwise.
- */
-bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
- ModelAction * next_act, Predicate ** unset_predicate)
-{
- /* Check if a branch with func_inst and corresponding predicate exists */
- bool branch_found = false;
- thread_id_t tid = next_act->get_tid();
-
- ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
- for (uint i = 0;i < branches->size();i++) {
- Predicate * branch = (*branches)[i];
- if (branch->get_func_inst() != next_inst)
- continue;
-
- /* Check against predicate expressions */
- bool predicate_correct = true;
- PredExprSet * pred_expressions = branch->get_pred_expressions();
-
- /* Only read and rmw actions my have unset predicate expressions */
- if (pred_expressions->getSize() == 0) {
- predicate_correct = false;
-
- if (*unset_predicate == NULL)
- *unset_predicate = branch;
- else
- ASSERT(false);
-
- continue;
- }
-
- PredExprSetIter * pred_expr_it = pred_expressions->iterator();
- while (pred_expr_it->hasNext()) {
- pred_expr * pred_expression = pred_expr_it->next();
- uint64_t last_read, next_read;
- bool equality;
-
- switch(pred_expression->token) {
- case NOPREDICATE:
- predicate_correct = true;
- break;
- case EQUALITY:
- FuncInst * to_be_compared;
- to_be_compared = pred_expression->func_inst;
-
- last_read = get_associated_read(tid, to_be_compared);
- if (last_read == VALUE_NONE)
- predicate_correct = false;
- // ASSERT(last_read != VALUE_NONE);
-
- next_read = next_act->get_reads_from_value();
- equality = (last_read == next_read);
- if (equality != pred_expression->value)
- predicate_correct = false;
-
- break;
- case NULLITY:
- // TODO: implement likely to be null
- equality = likely_reads_from_null(next_act);
- if (equality != pred_expression->value)
- predicate_correct = false;
- break;
- default:
- predicate_correct = false;
- model_print("unkown predicate token\n");
- break;
- }
- }
-
- delete pred_expr_it;
-
- if (predicate_correct) {
- *curr_pred = branch;
- branch_found = true;
- break;
- }
- }
-
- return branch_found;
-}
-
-/* Infer predicate expressions, which are generated in FuncNode::generate_predicates */
-void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
- SnapVector<struct half_pred_expr *> * half_pred_expressions)
-{
- void * loc = next_act->get_location();
- int thread_id = id_to_int(next_act->get_tid());
- loc_inst_map_t * loc_inst_map = thrd_loc_inst_maps[thread_id]->back();
-
- if (next_inst->is_read()) {
- /* read + rmw */
- if ( loc_inst_map->contains(loc) ) {
- FuncInst * last_inst = loc_inst_map->get(loc);
- struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
- half_pred_expressions->push_back(expression);
- } else if ( next_inst->is_single_location() ) {
- loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
-
- if (loc_may_equal != NULL) {
- loc_set_iter * loc_it = loc_may_equal->iterator();
- while (loc_it->hasNext()) {
- void * neighbor = loc_it->next();
- if (loc_inst_map->contains(neighbor)) {
- FuncInst * last_inst = loc_inst_map->get(neighbor);
-
- struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
- half_pred_expressions->push_back(expression);
- }
- }
-
- delete loc_it;
- }
- }
-
- // next_inst is not single location and has been null
- bool likely_null = likely_null_set.contains(next_inst);
- if ( !next_inst->is_single_location() && likely_null ) {
- struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL);
- half_pred_expressions->push_back(expression);
- }
- } else {
- /* Pure writes */
- // TODO: do anything here?
- }
-}
-
-/* Able to generate complex predicates when there are multiple predciate expressions */
-void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst,
- SnapVector<struct half_pred_expr *> * half_pred_expressions)
-{
- if (half_pred_expressions->size() == 0) {
- Predicate * new_pred = new Predicate(next_inst);
- curr_pred->add_child(new_pred);
- new_pred->set_parent(curr_pred);
-
- /* entry predicates and predicates containing pure write actions
- * have no predicate expressions */
- if ( curr_pred->is_entry_predicate() )
- new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
- else if (next_inst->is_write()) {
- /* next_inst->is_write() <==> pure writes */
- new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
- }
-
- return;
- }
-
- SnapVector<Predicate *> predicates;
-
- struct half_pred_expr * half_expr = (*half_pred_expressions)[0];
- predicates.push_back(new Predicate(next_inst));
- predicates.push_back(new Predicate(next_inst));
-
- predicates[0]->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
- predicates[1]->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
-
- for (uint i = 1;i < half_pred_expressions->size();i++) {
- half_expr = (*half_pred_expressions)[i];
-
- uint old_size = predicates.size();
- for (uint j = 0;j < old_size;j++) {
- Predicate * pred = predicates[j];
- Predicate * new_pred = new Predicate(next_inst);
- new_pred->copy_predicate_expr(pred);
-
- pred->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
- new_pred->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
-
- predicates.push_back(new_pred);
- }
- }
-
- for (uint i = 0;i < predicates.size();i++) {
- Predicate * pred= predicates[i];
- curr_pred->add_child(pred);
- pred->set_parent(curr_pred);
- }
-
- /* Free memories allocated by infer_predicate */
- for (uint i = 0;i < half_pred_expressions->size();i++) {
- struct half_pred_expr * tmp = (*half_pred_expressions)[i];
- snapshot_free(tmp);
- }
-}
-
-/* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */
-bool FuncNode::amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act)
-{
- ModelVector<Predicate *> * children = curr_pred->get_children();
-
- Predicate * unset_pred = NULL;
- for (uint i = 0;i < children->size();i++) {
- Predicate * child = (*children)[i];
- if (child->get_func_inst() == next_inst) {
- unset_pred = child;
- break;
- }
- }
-
- bool likely_null = likely_null_set.contains(next_inst);
-
- // only generate NULLITY predicate when it is actually NULL.
- if ( !next_inst->is_single_location() && likely_null ) {
- Predicate * new_pred = new Predicate(next_inst);
-
- curr_pred->add_child(new_pred);
- new_pred->set_parent(curr_pred);
-
- unset_pred->add_predicate_expr(NULLITY, NULL, false);
- new_pred->add_predicate_expr(NULLITY, NULL, true);
-
- return true;
- }
-
- return false;
-}
-
-void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
-{
- loc_set_t * locations = val_loc_map->get(val);
-
- if (locations == NULL) {
- locations = new loc_set_t();
- val_loc_map->put(val, locations);
- }
-
- update_loc_may_equal_map(loc, locations);
- locations->add(loc);
- // values_may_read_from->add(val);
-}
-
-void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
-{
- if (values == NULL)
- return;
-
- value_set_iter * it = values->iterator();
- while (it->hasNext()) {
- uint64_t val = it->next();
- add_to_val_loc_map(val, loc);
- }
-
- delete it;
-}
-
-void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations)
-{
- if ( old_locations->contains(new_loc) )
- return;
-
- loc_set_t * neighbors = loc_may_equal_map->get(new_loc);
-
- if (neighbors == NULL) {
- neighbors = new loc_set_t();
- loc_may_equal_map->put(new_loc, neighbors);
- }
-
- loc_set_iter * loc_it = old_locations->iterator();
- while (loc_it->hasNext()) {
- // new_loc: { old_locations, ... }
- void * member = loc_it->next();
- neighbors->add(member);
-
- // for each i in old_locations, i : { new_loc, ... }
- loc_set_t * _neighbors = loc_may_equal_map->get(member);
- if (_neighbors == NULL) {
- _neighbors = new loc_set_t();
- loc_may_equal_map->put(member, _neighbors);
- }
- _neighbors->add(new_loc);
- }
-
- delete loc_it;
-}
-
-bool FuncNode::likely_reads_from_null(ModelAction * read)
-{
- uint64_t read_val = read->get_reads_from_value();
- if ( (void *)(read_val && 0xffffffff) == NULL )
- return true;
-
- return false;
-}
-
-void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
-{
- int thread_id = id_to_int(tid);
- ModelVector<Predicate *> * stack = thrd_predicate_tree_position[thread_id];
- (*stack)[stack->size() - 1] = pred;
-}
-
-/* @return The position of a thread in a predicate tree */
-Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- return thrd_predicate_tree_position[thread_id]->back();
-}
-
-void FuncNode::add_predicate_to_trace(thread_id_t tid, Predicate * pred)
-{
- int thread_id = id_to_int(tid);
- thrd_predicate_trace[thread_id]->back()->push_back(pred);
-}
-
-void FuncNode::init_marker(thread_id_t tid)
-{
- marker++;
-
- int thread_id = id_to_int(tid);
- int old_size = thrd_markers.size();
-
- if (old_size < thread_id + 1) {
- thrd_markers.resize(thread_id + 1);
-
- for (int i = old_size;i < thread_id + 1;i++) {
- thrd_markers[i] = new ModelVector<uint32_t>();
- thrd_recursion_depth.push_back(-1);
- }
- }
-
- thrd_markers[thread_id]->push_back(marker);
- thrd_recursion_depth[thread_id]++;
-}
-
-uint64_t FuncNode::get_associated_read(thread_id_t tid, FuncInst * inst)
-{
- int thread_id = id_to_int(tid);
- int recursion_depth = thrd_recursion_depth[thread_id];
- uint marker = thrd_markers[thread_id]->back();
-
- return inst->get_associated_read(tid, recursion_depth, marker);
-}
-
-/* Make sure elements of maps are initialized properly when threads enter functions */
-void FuncNode::init_local_maps(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int old_size = thrd_loc_inst_maps.size();
-
- if (old_size < thread_id + 1) {
- int new_size = thread_id + 1;
-
- thrd_loc_inst_maps.resize(new_size);
- thrd_inst_id_maps.resize(new_size);
- thrd_inst_pred_maps.resize(new_size);
-
- for (int i = old_size;i < new_size;i++) {
- thrd_loc_inst_maps[i] = new ModelVector<loc_inst_map_t *>;
- thrd_inst_id_maps[i] = new ModelVector<inst_id_map_t *>;
- thrd_inst_pred_maps[i] = new ModelVector<inst_pred_map_t *>;
- }
- }
-
- ModelVector<loc_inst_map_t *> * map = thrd_loc_inst_maps[thread_id];
- int index = thrd_recursion_depth[thread_id];
-
- // If there are recursive calls, push more hashtables into the vector.
- if (map->size() < (uint) index + 1) {
- thrd_loc_inst_maps[thread_id]->push_back(new loc_inst_map_t(64));
- thrd_inst_id_maps[thread_id]->push_back(new inst_id_map_t(64));
- thrd_inst_pred_maps[thread_id]->push_back(new inst_pred_map_t(64));
- }
-
- ASSERT(map->size() == (uint) index + 1);
-}
-
-/* Reset elements of maps when threads exit functions */
-void FuncNode::reset_local_maps(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int index = thrd_recursion_depth[thread_id];
-
- // When recursive call ends, keep only one hashtable in the vector
- if (index > 0) {
- delete thrd_loc_inst_maps[thread_id]->back();
- delete thrd_inst_id_maps[thread_id]->back();
- delete thrd_inst_pred_maps[thread_id]->back();
-
- thrd_loc_inst_maps[thread_id]->pop_back();
- thrd_inst_id_maps[thread_id]->pop_back();
- thrd_inst_pred_maps[thread_id]->pop_back();
- } else {
- thrd_loc_inst_maps[thread_id]->back()->reset();
- thrd_inst_id_maps[thread_id]->back()->reset();
- thrd_inst_pred_maps[thread_id]->back()->reset();
- }
-}
-
-void FuncNode::init_predicate_tree_data_structure(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int old_size = thrd_predicate_tree_position.size();
-
- if (old_size < thread_id + 1) {
- thrd_predicate_tree_position.resize(thread_id + 1);
- thrd_predicate_trace.resize(thread_id + 1);
-
- for (int i = old_size;i < thread_id + 1;i++) {
- thrd_predicate_tree_position[i] = new ModelVector<Predicate *>();
- thrd_predicate_trace[i] = new ModelVector<predicate_trace_t *>();
- }
- }
-
- thrd_predicate_tree_position[thread_id]->push_back(predicate_tree_entry);
- thrd_predicate_trace[thread_id]->push_back(new predicate_trace_t());
-}
-
-void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- thrd_predicate_tree_position[thread_id]->pop_back();
-
- // Free memories allocated in init_predicate_tree_data_structure
- delete thrd_predicate_trace[thread_id]->back();
- thrd_predicate_trace[thread_id]->pop_back();
-}
-
-/* Add FuncNodes that this node may follow */
-void FuncNode::add_out_edge(FuncNode * other)
-{
- if ( !edge_table.contains(other) ) {
- edge_table.put(other, OUT_EDGE);
- out_edges.push_back(other);
- return;
- }
-
- edge_type_t edge = edge_table.get(other);
- if (edge == IN_EDGE) {
- edge_table.put(other, BI_EDGE);
- out_edges.push_back(other);
- }
-}
-
-/* Compute the distance between this FuncNode and the target node.
- * Return -1 if the target node is unreachable or the actual distance
- * is greater than max_step.
- */
-int FuncNode::compute_distance(FuncNode * target, int max_step)
-{
- if (target == NULL)
- return -1;
- else if (target == this)
- return 0;
-
- // Be careful with memory
- SnapList<FuncNode *> queue;
- HashTable<FuncNode *, int, uintptr_t, 0> distances(128);
-
- queue.push_back(this);
- distances.put(this, 0);
-
- while (!queue.empty()) {
- FuncNode * curr = queue.front();
- queue.pop_front();
- int dist = distances.get(curr);
-
- if (max_step <= dist)
- return -1;
-
- ModelList<FuncNode *> * outEdges = curr->get_out_edges();
- mllnode<FuncNode *> * it;
- for (it = outEdges->begin();it != NULL;it = it->getNext()) {
- FuncNode * out_node = it->getVal();
-
- /* This node has not been visited before */
- if ( !distances.contains(out_node) ) {
- if (out_node == target)
- return dist + 1;
-
- queue.push_back(out_node);
- distances.put(out_node, dist + 1);
- }
- }
- }
-
- /* Target node is unreachable */
- return -1;
-}
-
-void FuncNode::update_predicate_tree_weight(thread_id_t tid)
-{
- predicate_trace_t * trace = thrd_predicate_trace[id_to_int(tid)]->back();
-
- // Update predicate weights based on prediate trace
- for (int i = trace->size() - 1;i >= 0;i--) {
- Predicate * node = (*trace)[i];
- ModelVector<Predicate *> * children = node->get_children();
-
- if (children->size() == 0) {
- double weight = 100.0 / sqrt(node->get_expl_count() + node->get_fail_count() + 1);
- node->set_weight(weight);
- } else {
- double weight_sum = 0.0;
- for (uint i = 0;i < children->size();i++) {
- Predicate * child = (*children)[i];
- double weight = child->get_weight();
- weight_sum += weight;
- }
-
- double average_weight = (double) weight_sum / (double) children->size();
- double weight = average_weight * pow(0.9, node->get_depth());
- node->set_weight(weight);
- }
- }
-}
-
-void FuncNode::print_predicate_tree()
-{
- model_print("digraph function_%s {\n", func_name);
- predicate_tree_entry->print_pred_subtree();
- predicate_tree_exit->print_predicate();
- model_print("}\n"); // end of graph
-}
+++ /dev/null
-#ifndef __FUNCNODE_H__
-#define __FUNCNODE_H__
-
-#include "hashset.h"
-#include "hashfunction.h"
-#include "classlist.h"
-#include "threads-model.h"
-
-#define MAX_DIST 10
-
-typedef ModelList<FuncInst *> func_inst_list_mt;
-typedef ModelVector<Predicate *> predicate_trace_t;
-
-typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
-typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
-typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map_t;
-
-typedef enum edge_type {
- IN_EDGE, OUT_EDGE, BI_EDGE
-} edge_type_t;
-
-class FuncNode {
-public:
- FuncNode(ModelHistory * history);
- ~FuncNode();
-
- uint32_t get_func_id() { return func_id; }
- const char * get_func_name() { return func_name; }
- void set_func_id(uint32_t id) { func_id = id; }
- void set_func_name(const char * name) { func_name = name; }
- void set_new_exec_flag();
-
- void add_inst(ModelAction *act);
- FuncInst * create_new_inst(ModelAction *act);
- FuncInst * get_inst(ModelAction *act);
-
- func_inst_list_mt * get_inst_list() { return &inst_list; }
- func_inst_list_mt * get_entry_insts() { return &entry_insts; }
- void add_entry_inst(FuncInst * inst);
-
- void function_entry_handler(thread_id_t tid);
- void function_exit_handler(thread_id_t tid);
-
- void update_tree(ModelAction * act);
-
- void add_to_val_loc_map(uint64_t val, void * loc);
- void add_to_val_loc_map(value_set_t * values, void * loc);
- void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations);
-
- Predicate * get_predicate_tree_position(thread_id_t tid);
-
- void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
-
- uint64_t get_associated_read(thread_id_t tid, FuncInst * inst);
-
- void add_out_edge(FuncNode * other);
- ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
- int compute_distance(FuncNode * target, int max_step = MAX_DIST);
-
- void print_predicate_tree();
-
- MEMALLOC
-private:
- uint32_t func_id;
- const char * func_name;
- ModelHistory * history;
- Predicate * predicate_tree_entry; // A dummy node whose children are the real entries
- Predicate * predicate_tree_exit; // A dummy node
-
- uint32_t inst_counter;
- uint32_t marker;
- uint32_t exit_count;
- ModelVector< ModelVector<uint32_t> *> thrd_markers;
- ModelVector<int> thrd_recursion_depth; // Recursion depth starts from 0 to match with vector indexes.
-
- void init_marker(thread_id_t tid);
-
- /* Use source line number as the key of hashtable, to check if
- * atomic operation with this line number has been added or not
- */
- HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> func_inst_map;
-
- /* List of all atomic actions in this function */
- func_inst_list_mt inst_list;
-
- /* Possible entry atomic actions in this function */
- func_inst_list_mt entry_insts;
-
- /* Map a FuncInst to the its predicate when updating predicate trees */
- ModelVector< ModelVector<inst_pred_map_t *> * > thrd_inst_pred_maps;
-
- /* Number FuncInsts to detect loops when updating predicate trees */
- ModelVector< ModelVector<inst_id_map_t *> *> thrd_inst_id_maps;
-
- /* Detect read actions at the same locations when updating predicate trees */
- ModelVector< ModelVector<loc_inst_map_t *> *> thrd_loc_inst_maps;
-
- void init_local_maps(thread_id_t tid);
- void reset_local_maps(thread_id_t tid);
-
- void update_inst_tree(func_inst_list_t * inst_list);
- void update_predicate_tree(ModelAction * act);
- bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
-
- void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
- void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
- bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);
-
- /* Set of locations read by this FuncNode */
- loc_set_t * read_locations;
-
- /* Set of locations written to by this FuncNode */
- loc_set_t * write_locations;
-
- /* Keeps track of locations that have the same values written to */
- HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash> * val_loc_map;
-
- /* Keeps track of locations that may share the same value as key, deduced from val_loc_map */
- HashTable<void *, loc_set_t *, uintptr_t, 0> * loc_may_equal_map;
-
- HashTable<FuncInst *, bool, uintptr_t, 0, model_malloc, model_calloc, model_free> likely_null_set;
-
- bool likely_reads_from_null(ModelAction * read);
- // value_set_t * values_may_read_from;
-
- /* Run-time position in the predicate tree for each thread
- * The inner vector is used to deal with recursive functions. */
- ModelVector< ModelVector<Predicate *> * > thrd_predicate_tree_position;
-
- ModelVector< ModelVector<predicate_trace_t *> * > thrd_predicate_trace;
-
- void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
-
- void init_predicate_tree_data_structure(thread_id_t tid);
- void reset_predicate_tree_data_structure(thread_id_t tid);
-
- /* Store the relation between this FuncNode and other FuncNodes */
- HashTable<FuncNode *, edge_type_t, uintptr_t, 0, model_malloc, model_calloc, model_free> edge_table;
-
- /* FuncNodes that follow this node */
- ModelList<FuncNode *> out_edges;
-
- void update_predicate_tree_weight(thread_id_t tid);
-};
-
-#endif /* __FUNCNODE_H__ */
+++ /dev/null
-#include <inttypes.h>
-#include "history.h"
-#include "action.h"
-#include "funcnode.h"
-#include "funcinst.h"
-#include "common.h"
-#include "concretepredicate.h"
-#include "waitobj.h"
-
-#include "model.h"
-#include "execution.h"
-#include "newfuzzer.h"
-
-/** @brief Constructor */
-ModelHistory::ModelHistory() :
- func_counter(1), /* function id starts with 1 */
- last_seq_number(INIT_SEQ_NUMBER),
- func_map(),
- func_map_rev(),
- func_nodes()
-{
- /* The following are snapshot data structures */
- write_history = new HashTable<void *, value_set_t *, uintptr_t, 0>();
- loc_rd_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
- loc_wr_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
- loc_waiting_writes_map = new HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0>();
- thrd_func_list = new SnapVector<func_id_list_t>();
- thrd_last_entered_func = new SnapVector<uint32_t>();
- thrd_waiting_write = new SnapVector<ConcretePredicate *>();
- thrd_wait_obj = new SnapVector<WaitObj *>();
-}
-
-ModelHistory::~ModelHistory()
-{
- // TODO: complete deconstructor; maybe not needed
- for (uint i = 0;i < thrd_wait_obj->size();i++)
- delete (*thrd_wait_obj)[i];
-}
-
-void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
-{
- //model_print("thread %d entering func %d\n", tid, func_id);
- uint id = id_to_int(tid);
-
- if ( thrd_func_list->size() <= id ) {
- uint oldsize = thrd_func_list->size();
- thrd_func_list->resize( id + 1 );
-
- for (uint i = oldsize;i < id + 1;i++) {
- // push 0 as a dummy function id to a void seg fault
- new (&(*thrd_func_list)[i]) func_id_list_t();
- (*thrd_func_list)[i].push_back(0);
- thrd_last_entered_func->push_back(0);
- }
- }
-
- uint32_t last_entered_func_id = (*thrd_last_entered_func)[id];
- (*thrd_last_entered_func)[id] = func_id;
- (*thrd_func_list)[id].push_back(func_id);
-
- if ( func_nodes.size() <= func_id )
- resize_func_nodes( func_id + 1 );
-
- FuncNode * func_node = func_nodes[func_id];
- func_node->function_entry_handler(tid);
-
- /* Add edges between FuncNodes */
- if (last_entered_func_id != 0) {
- FuncNode * last_func_node = func_nodes[last_entered_func_id];
- last_func_node->add_out_edge(func_node);
- }
-
- /* Monitor the statuses of threads waiting for tid */
- // monitor_waiting_thread(func_id, tid);
-}
-
-/* @param func_id a non-zero value */
-void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
-{
- uint32_t id = id_to_int(tid);
- uint32_t last_func_id = (*thrd_func_list)[id].back();
-
- if (last_func_id == func_id) {
- FuncNode * func_node = func_nodes[func_id];
- func_node->function_exit_handler(tid);
-
- (*thrd_func_list)[id].pop_back();
- } else {
- ASSERT(false);
- }
- //model_print("thread %d exiting func %d\n", tid, func_id);
-}
-
-void ModelHistory::resize_func_nodes(uint32_t new_size)
-{
- uint32_t old_size = func_nodes.size();
-
- if ( old_size < new_size )
- func_nodes.resize(new_size);
-
- for (uint32_t id = old_size;id < new_size;id++) {
- const char * func_name = func_map_rev[id];
- FuncNode * func_node = new FuncNode(this);
- func_node->set_func_id(id);
- func_node->set_func_name(func_name);
- func_nodes[id] = func_node;
- }
-}
-
-void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
-{
- uint32_t thread_id = id_to_int(tid);
- /* Return if thread tid has not entered any function that contains atomics */
- if ( thrd_func_list->size() <= thread_id )
- return;
-
- /* Monitor the statuses of threads waiting for tid */
- // monitor_waiting_thread_counter(tid);
-
- /* Every write action should be processed, including
- * nonatomic writes (which have no position) */
- if (act->is_write()) {
- void * location = act->get_location();
- uint64_t value = act->get_write_value();
- update_write_history(location, value);
-
- /* Notify FuncNodes that may read from this location */
- SnapVector<FuncNode *> * func_node_list = getRdFuncNodes(location);
- for (uint i = 0;i < func_node_list->size();i++) {
- FuncNode * func_node = (*func_node_list)[i];
- func_node->add_to_val_loc_map(value, location);
- }
-
- // check_waiting_write(act);
- }
-
- uint32_t func_id = (*thrd_func_list)[thread_id].back();
-
- /* The following does not care about actions that are not inside
- * any function that contains atomics or actions without a position */
- if (func_id == 0 || act->get_position() == NULL)
- return;
-
- if (skip_action(act))
- return;
-
- FuncNode * func_node = func_nodes[func_id];
- func_node->add_inst(act);
-
- func_node->update_tree(act);
- last_seq_number = act->get_seq_number();
-}
-
-/* Return the FuncNode given its func_id */
-FuncNode * ModelHistory::get_func_node(uint32_t func_id)
-{
- if (func_id == 0)
- return NULL;
-
- // This node has not been added to func_nodes
- if (func_nodes.size() <= func_id)
- return NULL;
-
- return func_nodes[func_id];
-}
-
-/* Return the current FuncNode when given a thread id */
-FuncNode * ModelHistory::get_curr_func_node(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- uint32_t func_id = (*thrd_func_list)[thread_id].back();
-
- if (func_id != 0) {
- return func_nodes[func_id];
- }
-
- return NULL;
-}
-
-void ModelHistory::update_write_history(void * location, uint64_t write_val)
-{
- value_set_t * write_set = write_history->get(location);
-
- if (write_set == NULL) {
- write_set = new value_set_t();
- write_history->put(location, write_set);
- }
-
- write_set->add(write_val);
-}
-
-void ModelHistory::update_loc_rd_func_nodes_map(void * location, FuncNode * node)
-{
- SnapVector<FuncNode *> * func_node_list = getRdFuncNodes(location);
- func_node_list->push_back(node);
-}
-
-void ModelHistory::update_loc_wr_func_nodes_map(void * location, FuncNode * node)
-{
- SnapVector<FuncNode *> * func_node_list = getWrFuncNodes(location);
- func_node_list->push_back(node);
-}
-
-SnapVector<FuncNode *> * ModelHistory::getRdFuncNodes(void * location)
-{
- SnapVector<FuncNode *> * func_node_list = loc_rd_func_nodes_map->get(location);
- if (func_node_list == NULL) {
- func_node_list = new SnapVector<FuncNode *>();
- loc_rd_func_nodes_map->put(location, func_node_list);
- }
-
- return func_node_list;
-}
-
-SnapVector<FuncNode *> * ModelHistory::getWrFuncNodes(void * location)
-{
- SnapVector<FuncNode *> * func_node_list = loc_wr_func_nodes_map->get(location);
- if (func_node_list == NULL) {
- func_node_list = new SnapVector<FuncNode *>();
- loc_wr_func_nodes_map->put(location, func_node_list);
- }
-
- return func_node_list;
-}
-
-/* When a thread is paused by Fuzzer, keep track of the condition it is waiting for */
-void ModelHistory::add_waiting_write(ConcretePredicate * concrete)
-{
- void * location = concrete->get_location();
- SnapVector<ConcretePredicate *> * waiting_conditions = loc_waiting_writes_map->get(location);
- if (waiting_conditions == NULL) {
- waiting_conditions = new SnapVector<ConcretePredicate *>();
- loc_waiting_writes_map->put(location, waiting_conditions);
- }
-
- /* waiting_conditions should not have duplications */
- waiting_conditions->push_back(concrete);
-
- int thread_id = id_to_int(concrete->get_tid());
- if (thrd_waiting_write->size() <= (uint) thread_id) {
- thrd_waiting_write->resize(thread_id + 1);
- }
-
- (*thrd_waiting_write)[thread_id] = concrete;
-}
-
-void ModelHistory::remove_waiting_write(thread_id_t tid)
-{
- ConcretePredicate * concrete = (*thrd_waiting_write)[ id_to_int(tid) ];
- void * location = concrete->get_location();
- SnapVector<ConcretePredicate *> * concrete_preds = loc_waiting_writes_map->get(location);
-
- /* Linear search should be fine because presumably not many ConcretePredicates
- * are at the same memory location */
- for (uint i = 0;i < concrete_preds->size();i++) {
- ConcretePredicate * current = (*concrete_preds)[i];
- if (concrete == current) {
- (*concrete_preds)[i] = concrete_preds->back();
- concrete_preds->pop_back();
- break;
- }
- }
-
- int thread_id = id_to_int( concrete->get_tid() );
- (*thrd_waiting_write)[thread_id] = NULL;
- delete concrete;
-}
-
-/* Check if any other thread is waiting for this write action. If so, "notify" them */
-void ModelHistory::check_waiting_write(ModelAction * write_act)
-{
- void * location = write_act->get_location();
- uint64_t value = write_act->get_write_value();
- SnapVector<ConcretePredicate *> * concrete_preds = loc_waiting_writes_map->get(location);
- if (concrete_preds == NULL)
- return;
-
- uint index = 0;
- while (index < concrete_preds->size()) {
- ConcretePredicate * concrete_pred = (*concrete_preds)[index];
- SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
- bool satisfy_predicate = true;
- /* Check if the written value satisfies every predicate expression */
- for (uint i = 0;i < concrete_exprs->size();i++) {
- struct concrete_pred_expr concrete = (*concrete_exprs)[i];
- bool equality = false;
- switch (concrete.token) {
- case EQUALITY:
- equality = (value == concrete.value);
- break;
- case NULLITY:
- equality = ((void*)value == NULL);
- break;
- default:
- model_print("unknown predicate token");
- break;
- }
-
- if (equality != concrete.equality) {
- satisfy_predicate = false;
- break;
- }
- }
-
- if (satisfy_predicate) {
- /* Wake up threads */
- thread_id_t tid = concrete_pred->get_tid();
- Thread * thread = model->get_thread(tid);
-
- //model_print("** thread %d is woken up\n", thread->get_id());
- ((NewFuzzer *)model->get_execution()->getFuzzer())->notify_paused_thread(thread);
- }
-
- index++;
- }
-}
-
-WaitObj * ModelHistory::getWaitObj(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int old_size = thrd_wait_obj->size();
- if (old_size <= thread_id) {
- thrd_wait_obj->resize(thread_id + 1);
- for (int i = old_size;i < thread_id + 1;i++) {
- (*thrd_wait_obj)[i] = new WaitObj( int_to_id(i) );
- }
- }
-
- return (*thrd_wait_obj)[thread_id];
-}
-
-void ModelHistory::add_waiting_thread(thread_id_t self_id,
- thread_id_t waiting_for_id, FuncNode * target_node, int dist)
-{
- WaitObj * self_wait_obj = getWaitObj(self_id);
- self_wait_obj->add_waiting_for(waiting_for_id, target_node, dist);
-
- /* Update waited-by relation */
- WaitObj * other_wait_obj = getWaitObj(waiting_for_id);
- other_wait_obj->add_waited_by(self_id);
-}
-
-/* Thread tid is woken up (or notified), so it is not waiting for others anymore */
-void ModelHistory::remove_waiting_thread(thread_id_t tid)
-{
- WaitObj * self_wait_obj = getWaitObj(tid);
- thrd_id_set_t * waiting_for = self_wait_obj->getWaitingFor();
-
- /* Remove tid from waited_by's */
- thrd_id_set_iter * iter = waiting_for->iterator();
- while (iter->hasNext()) {
- thread_id_t other_id = iter->next();
- WaitObj * other_wait_obj = getWaitObj(other_id);
- other_wait_obj->remove_waited_by(tid);
- }
-
- self_wait_obj->clear_waiting_for();
- delete iter;
-}
-
-void ModelHistory::stop_waiting_for_node(thread_id_t self_id,
- thread_id_t waiting_for_id, FuncNode * target_node)
-{
- WaitObj * self_wait_obj = getWaitObj(self_id);
- bool thread_removed = self_wait_obj->remove_waiting_for_node(waiting_for_id, target_node);
-
- // model_print("\t%d gives up %d on node %d\n", self_id, waiting_for_id, target_node->get_func_id());
-
- /* If thread self_id is not waiting for waiting_for_id anymore */
- if (thread_removed) {
- WaitObj * other_wait_obj = getWaitObj(waiting_for_id);
- other_wait_obj->remove_waited_by(self_id);
-
- thrd_id_set_t * self_waiting_for = self_wait_obj->getWaitingFor();
- if ( self_waiting_for->isEmpty() ) {
- // model_print("\tthread %d waits for nobody, wake up\n", self_id);
- ModelExecution * execution = model->get_execution();
- Thread * thread = execution->get_thread(self_id);
- ((NewFuzzer *)execution->getFuzzer())->notify_paused_thread(thread);
- }
- }
-}
-
-bool ModelHistory::skip_action(ModelAction * act)
-{
- bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
- modelclock_t curr_seq_number = act->get_seq_number();
-
- /* Skip actions that are second part of a read modify write */
- if (second_part_of_rmw)
- return true;
-
- /* Skip actions with the same sequence number */
- if (last_seq_number != INIT_SEQ_NUMBER && last_seq_number == curr_seq_number)
- return true;
-
- /* Skip actions that are paused by fuzzer (sequence number is 0) */
- if (curr_seq_number == 0)
- return true;
-
- return false;
-}
-
-/* Monitor thread tid and decide whether other threads (that are waiting for tid)
- * should keep waiting for this thread or not. Shall only be called when a thread
- * enters a function.
- *
- * Heuristics: If the distance from the current FuncNode to some target node
- * ever increases, stop waiting for this thread on this target node.
- */
-void ModelHistory::monitor_waiting_thread(uint32_t func_id, thread_id_t tid)
-{
- WaitObj * wait_obj = getWaitObj(tid);
- thrd_id_set_t * waited_by = wait_obj->getWaitedBy();
- FuncNode * curr_node = func_nodes[func_id];
-
- /* For each thread waiting for tid */
- thrd_id_set_iter * tid_iter = waited_by->iterator();
- while (tid_iter->hasNext()) {
- thread_id_t waited_by_id = tid_iter->next();
- WaitObj * other_wait_obj = getWaitObj(waited_by_id);
-
- node_set_t * target_nodes = other_wait_obj->getTargetNodes(tid);
- node_set_iter * node_iter = target_nodes->iterator();
- while (node_iter->hasNext()) {
- FuncNode * target = node_iter->next();
- int old_dist = other_wait_obj->lookup_dist(tid, target);
- int new_dist = curr_node->compute_distance(target, old_dist);
-
- if (new_dist == -1) {
- stop_waiting_for_node(waited_by_id, tid, target);
- }
- }
-
- delete node_iter;
- }
-
- delete tid_iter;
-}
-
-void ModelHistory::monitor_waiting_thread_counter(thread_id_t tid)
-{
- WaitObj * wait_obj = getWaitObj(tid);
- thrd_id_set_t * waited_by = wait_obj->getWaitedBy();
-
- // Thread tid has taken an action, update the counter for threads waiting for tid
- thrd_id_set_iter * tid_iter = waited_by->iterator();
- while (tid_iter->hasNext()) {
- thread_id_t waited_by_id = tid_iter->next();
- WaitObj * other_wait_obj = getWaitObj(waited_by_id);
-
- bool expire = other_wait_obj->incr_counter(tid);
- if (expire) {
-// model_print("thread %d stops waiting for thread %d\n", waited_by_id, tid);
- wait_obj->remove_waited_by(waited_by_id);
- other_wait_obj->remove_waiting_for(tid);
-
- thrd_id_set_t * other_waiting_for = other_wait_obj->getWaitingFor();
- if ( other_waiting_for->isEmpty() ) {
- // model_print("\tthread %d waits for nobody, wake up\n", self_id);
- ModelExecution * execution = model->get_execution();
- Thread * thread = execution->get_thread(waited_by_id);
- ((NewFuzzer *)execution->getFuzzer())->notify_paused_thread(thread);
- }
- }
- }
-
- delete tid_iter;
-}
-
-/* Reallocate some snapshotted memories when new executions start */
-void ModelHistory::set_new_exec_flag()
-{
- for (uint i = 1;i < func_nodes.size();i++) {
- FuncNode * func_node = func_nodes[i];
- func_node->set_new_exec_flag();
- }
-}
-
-void ModelHistory::dump_func_node_graph()
-{
- model_print("digraph func_node_graph {\n");
- for (uint i = 1;i < func_nodes.size();i++) {
- FuncNode * node = func_nodes[i];
- ModelList<FuncNode *> * out_edges = node->get_out_edges();
-
- model_print("\"%p\" [label=\"%s\"]\n", node, node->get_func_name());
- mllnode<FuncNode *> * it;
- for (it = out_edges->begin();it != NULL;it = it->getNext()) {
- FuncNode * other = it->getVal();
- model_print("\"%p\" -> \"%p\"\n", node, other);
- }
- }
- model_print("}\n");
-}
-
-void ModelHistory::print_func_node()
-{
- /* function id starts with 1 */
- for (uint32_t i = 1;i < func_nodes.size();i++) {
- FuncNode * func_node = func_nodes[i];
- 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());
-
- mllnode<FuncInst*>* it;
- for (it = entry_insts->begin();it != NULL;it=it->getNext()) {
- FuncInst *inst = it->getVal();
- model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
- }
- */
- }
-}
-
-void ModelHistory::print_waiting_threads()
-{
- ModelExecution * execution = model->get_execution();
- for (unsigned int i = 0;i < execution->get_num_threads();i++) {
- thread_id_t tid = int_to_id(i);
- WaitObj * wait_obj = getWaitObj(tid);
- wait_obj->print_waiting_for();
- }
-
- for (unsigned int i = 0;i < execution->get_num_threads();i++) {
- thread_id_t tid = int_to_id(i);
- WaitObj * wait_obj = getWaitObj(tid);
- wait_obj->print_waited_by();
- }
-}
+++ /dev/null
-#ifndef __HISTORY_H__
-#define __HISTORY_H__
-
-#include "common.h"
-#include "classlist.h"
-#include "hashtable.h"
-#include "threads-model.h"
-
-#define INIT_SEQ_NUMBER 0xffffffff
-
-class ModelHistory {
-public:
- ModelHistory();
- ~ModelHistory();
-
- void enter_function(const uint32_t func_id, thread_id_t tid);
- void exit_function(const uint32_t func_id, thread_id_t tid);
-
- uint32_t get_func_counter() { return func_counter; }
- void incr_func_counter() { func_counter++; }
-
- void resize_func_nodes(uint32_t max_func_id);
- void process_action(ModelAction *act, thread_id_t tid);
-
- HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncMap() { return &func_map; }
- ModelVector<const char *> * getFuncMapRev() { return &func_map_rev; }
-
- ModelVector<FuncNode *> * getFuncNodes() { return &func_nodes; }
- FuncNode * get_func_node(uint32_t func_id);
- FuncNode * get_curr_func_node(thread_id_t tid);
-
- void update_write_history(void * location, uint64_t write_val);
- HashTable<void *, value_set_t *, uintptr_t, 0> * getWriteHistory() { return write_history; }
- void update_loc_rd_func_nodes_map(void * location, FuncNode * node);
- void update_loc_wr_func_nodes_map(void * location, FuncNode * node);
- SnapVector<FuncNode *> * getRdFuncNodes(void * location);
- SnapVector<FuncNode *> * getWrFuncNodes(void * location);
-
- void add_waiting_write(ConcretePredicate * concrete);
- void remove_waiting_write(thread_id_t tid);
- void check_waiting_write(ModelAction * write_act);
- SnapVector<ConcretePredicate *> * getThrdWaitingWrite() { return thrd_waiting_write; }
-
- WaitObj * getWaitObj(thread_id_t tid);
- void add_waiting_thread(thread_id_t self_id, thread_id_t waiting_for_id, FuncNode * target_node, int dist);
- void remove_waiting_thread(thread_id_t tid);
- void stop_waiting_for_node(thread_id_t self_id, thread_id_t waiting_for_id, FuncNode * target_node);
-
- void set_new_exec_flag();
- void dump_func_node_graph();
- void print_func_node();
- void print_waiting_threads();
-
- MEMALLOC
-private:
- uint32_t func_counter;
- modelclock_t last_seq_number;
-
- /* Map function names to integer ids */
- HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> func_map;
-
- /* Map integer ids to function names */
- ModelVector<const char *> func_map_rev;
-
- ModelVector<FuncNode *> func_nodes;
-
- /* Map a location to a set of values that have been written to it */
- HashTable<void *, value_set_t *, uintptr_t, 0> * write_history;
-
- /* Map a location to FuncNodes that may read from it */
- HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0> * loc_rd_func_nodes_map;
-
- /* Map a location to FuncNodes that may write to it */
- HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0> * loc_wr_func_nodes_map;
-
- HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0> * loc_waiting_writes_map;
-
- /* thrd_func_list stores a list of function ids for each thread.
- * Each element in thrd_func_list stores the functions that
- * thread i has entered and yet to exit from
- */
- SnapVector<func_id_list_t> * thrd_func_list;
- SnapVector<uint32_t> * thrd_last_entered_func;
-
- /* The write values each paused thread is waiting for */
- SnapVector<ConcretePredicate *> * thrd_waiting_write;
- SnapVector<WaitObj *> * thrd_wait_obj;
-
- bool skip_action(ModelAction * act);
- void monitor_waiting_thread(uint32_t func_id, thread_id_t tid);
- void monitor_waiting_thread_counter(thread_id_t tid);
-
-};
-
-#endif /* __HISTORY_H__ */
extern "C" {
#endif
-void store_8(void *addr, uint8_t val);
-void store_16(void *addr, uint16_t val);
-void store_32(void *addr, uint32_t val);
-void store_64(void *addr, uint64_t val);
-
-uint8_t load_8(const void *addr);
-uint16_t load_16(const void *addr);
-uint32_t load_32(const void *addr);
-uint64_t load_64(const void *addr);
-
void cds_store8(void *addr);
void cds_store16(void *addr);
void cds_store32(void *addr);
+++ /dev/null
-/**
- * @file predicatetypes.h
- * @brief Define common predicate expression types
- */
-
-#ifndef __PREDICATE_TYPES_H__
-#define __PREDICATE_TYPES_H__
-
-typedef enum predicate_token {
- NOPREDICATE, EQUALITY, NULLITY
-} token_t;
-
-typedef enum predicate_sleep_result {
- SLEEP_FAIL_TYPE1, SLEEP_FAIL_TYPE2, SLEEP_FAIL_TYPE3,
- SLEEP_SUCCESS
-} sleep_result_t;
-
-/* If token is EQUALITY, then the predicate asserts whether
- * this load should read the same value as the last value
- * read at memory location specified in predicate_expr.
- */
-struct pred_expr {
- pred_expr(token_t token, FuncInst * inst, bool value) :
- token(token),
- func_inst(inst),
- value(value)
- {}
-
- token_t token;
- FuncInst * func_inst;
- bool value;
-
- MEMALLOC
-};
-
-/* Used by FuncNode to generate Predicates */
-struct half_pred_expr {
- half_pred_expr(token_t token, FuncInst * inst) :
- token(token),
- func_inst(inst)
- {}
-
- token_t token;
- FuncInst * func_inst;
-
- 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
-};
-
-#endif /* __PREDICATE_TYPES_H__ */
-
*/
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
{
+ createModelIfNotExist();
struct thread_params params = { start_routine, arg };
/* seq_cst is just a 'don't care' parameter */
model->switch_thread(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)¶ms));
int thrd_join(thrd_t t)
{
+ createModelIfNotExist();
Thread *th = t.priv;
model->switch_thread(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
return 0;
/** A no-op, for now */
void thrd_yield(void)
{
+ createModelIfNotExist();
model->switch_thread(new ModelAction(THREAD_YIELD, std::memory_order_seq_cst, thread_current(), VALUE_NONE));
}
thrd_t thrd_current(void)
{
+ createModelIfNotExist();
return thread_current()->get_thrd_t();
}
#include "output.h"
#include "traceanalysis.h"
#include "execution.h"
-#include "history.h"
#include "bugmessage.h"
#include "params.h"
#include "plugins.h"
ModelChecker *model = NULL;
int inside_model = 0;
+uint64_t get_nanotime()
+{
+ struct timespec currtime;
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+
+ return currtime.tv_nsec;
+}
+
void placeholder(void *) {
ASSERT(0);
}
/* Initialize default scheduler */
params(),
scheduler(new Scheduler()),
- history(new ModelHistory()),
execution(new ModelExecution(this, scheduler)),
execution_number(1),
curr_thread_num(MAIN_THREAD_ID),
}
model_print("\n");
+#ifdef PRINT_TRACE
execution->print_summary();
+#endif
}
/**
clear_program_output();
execution_number ++;
- history->set_new_exec_flag();
if (more_executions)
reset_to_initial_state();
void ModelChecker::startChecker() {
startExecution();
//Need to initial random number generator state to avoid resets on rollback
- initstate(423121, random_state, sizeof(random_state));
+ //initstate(423121, random_state, sizeof(random_state));
+ uint64_t seed = get_nanotime();
+ srandom(seed);
snapshot = take_snapshot();
//reset random number generator state
- setstate(random_state);
+ //setstate(random_state);
+ seed = get_nanotime();
+ srandom(seed);
install_trace_analyses(get_execution());
redirect_output();
void exit_model_checker();
ModelExecution * get_execution() const { return execution; }
- ModelHistory * get_history() const { return history; }
int get_execution_number() const { return execution_number; }
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
- ModelHistory * history;
ModelExecution *execution;
Thread * init_thread;
+++ /dev/null
-#include "newfuzzer.h"
-#include "threads-model.h"
-#include "action.h"
-#include "history.h"
-#include "funcnode.h"
-#include "funcinst.h"
-#include "concretepredicate.h"
-#include "waitobj.h"
-
-#include "model.h"
-#include "schedule.h"
-#include "execution.h"
-
-NewFuzzer::NewFuzzer() :
- thrd_last_read_act(),
- thrd_last_func_inst(),
- available_branches_tmp_storage(),
- thrd_selected_child_branch(),
- thrd_pruned_writes(),
- paused_thread_list(),
- paused_thread_table(128),
- dist_info_vec()
-{}
-
-/**
- * @brief Register the ModelHistory and ModelExecution engine
- */
-void NewFuzzer::register_engine(ModelChecker *_model, ModelExecution *execution)
-{
- this->history = _model->get_history();
- this->execution = execution;
-}
-
-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);
-
- if (thrd_last_read_act.size() <= (uint) thread_id) {
- thrd_last_read_act.resize(thread_id + 1);
- thrd_last_func_inst.resize(thread_id + 1);
- }
-
- // A new read action is encountered, select a random child branch of current predicate
- if (read != thrd_last_read_act[thread_id]) {
- FuncNode * func_node = history->get_curr_func_node(tid);
- Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
- FuncInst * read_inst = func_node->get_inst(read);
-
- if (curr_pred != NULL) {
- Predicate * selected_branch = NULL;
-
- if (check_branch_inst(curr_pred, read_inst, rf_set))
- selected_branch = selectBranch(tid, curr_pred, read_inst);
- else {
- // no child of curr_pred matches read_inst, check back edges
- PredSet * back_edges = curr_pred->get_backedges();
- PredSetIter * it = back_edges->iterator();
-
- while (it->hasNext()) {
- curr_pred = it->next();
- if (check_branch_inst(curr_pred, read_inst, rf_set)) {
- selected_branch = selectBranch(tid, curr_pred, read_inst);
- break;
- }
- }
-
- delete it;
- }
-
- thrd_selected_child_branch[thread_id] = selected_branch;
- prune_writes(tid, selected_branch, rf_set);
- }
-
- thrd_last_read_act[thread_id] = read;
- thrd_last_func_inst[thread_id] = read_inst;
- }
-
- // The chosen branch fails, reselect new branches
- while ( rf_set->size() == 0 ) {
- Predicate * selected_branch = get_selected_child_branch(tid);
- FuncNode * func_node = history->get_curr_func_node(tid);
-
- // Increment failure count
- selected_branch->incr_fail_count();
- func_node->add_predicate_to_trace(tid, selected_branch); // For updating predicate weight
-
- //model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
-
- SnapVector<ModelAction *> * pruned_writes = thrd_pruned_writes[thread_id];
- for (uint i = 0;i < pruned_writes->size();i++) {
- rf_set->push_back( (*pruned_writes)[i] );
- }
-
- // Reselect a predicate and prune writes
- Predicate * curr_pred = selected_branch->get_parent();
- FuncInst * read_inst = thrd_last_func_inst[thread_id];
- selected_branch = selectBranch(tid, curr_pred, read_inst);
- thrd_selected_child_branch[thread_id] = selected_branch;
-
- prune_writes(tid, selected_branch, rf_set);
-
- ASSERT(selected_branch);
- }
-
- int random_index = random() % rf_set->size();
-
- return random_index;
-}
-
-/* Check if children of curr_pred match read_inst.
- * @return False if no child matches read_inst
- */
-bool NewFuzzer::check_branch_inst(Predicate * curr_pred, FuncInst * read_inst,
- SnapVector<ModelAction *> * rf_set)
-{
- available_branches_tmp_storage.clear();
-
- ASSERT(!rf_set->empty());
- if (curr_pred == NULL || read_inst == NULL)
- return false;
-
- ModelVector<Predicate *> * children = curr_pred->get_children();
- bool any_child_match = false;
-
- /* Iterate over all predicate children */
- for (uint i = 0;i < children->size();i++) {
- Predicate * branch = (*children)[i];
-
- /* The children predicates may have different FuncInsts */
- if (branch->get_func_inst() == read_inst) {
- any_child_match = true;
- branch->incr_total_checking_count();
- available_branches_tmp_storage.push_back(branch);
- }
- }
-
- return any_child_match;
-}
-
-/* Select a random branch from the children of curr_pred
- * @return The selected branch
- */
-Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst)
-{
- int thread_id = id_to_int(tid);
- if ( thrd_selected_child_branch.size() <= (uint) thread_id)
- thrd_selected_child_branch.resize(thread_id + 1);
-
- if (curr_pred == NULL || read_inst == NULL) {
- thrd_selected_child_branch[thread_id] = NULL;
- return NULL;
- }
-
- // predicate children have not been generated
- if (available_branches_tmp_storage.size() == 0) {
- thrd_selected_child_branch[thread_id] = NULL;
- return NULL;
- }
-
- int index = choose_branch_index(&available_branches_tmp_storage);
- Predicate * selected_branch = available_branches_tmp_storage[ index ];
-
- /* Remove the chosen branch from vec in case that this
- * branch fails and need to choose another one */
- available_branches_tmp_storage[index] = available_branches_tmp_storage.back();
- available_branches_tmp_storage.pop_back();
-
- return selected_branch;
-}
-
-/**
- * @brief Select a branch from the given predicate branch
- */
-int NewFuzzer::choose_branch_index(SnapVector<Predicate *> * branches)
-{
- if (branches->size() == 1)
- return 0;
-
- double total_weight = 0;
- SnapVector<double> weights;
- for (uint i = 0;i < branches->size();i++) {
- Predicate * branch = (*branches)[i];
- double weight = branch->get_weight();
- total_weight += weight;
- weights.push_back(weight);
- }
-
- double prob = (double) random() / RAND_MAX;
- double prob_sum = 0;
- int index = 0;
-
- for (uint i = 0;i < weights.size();i++) {
- index = i;
- prob_sum += (double) (weights[i] / total_weight);
- if (prob_sum > prob) {
- break;
- }
- }
-
- return index;
-// return random() % branches->size();
-}
-
-Predicate * NewFuzzer::get_selected_child_branch(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- if (thrd_selected_child_branch.size() <= (uint) thread_id)
- return NULL;
-
- return thrd_selected_child_branch[thread_id];
-}
-
-/* Remove writes from the rf_set that do not satisfie the selected predicate,
- * and store them in thrd_pruned_writes
- *
- * @return true if rf_set is pruned
- */
-bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set)
-{
- if (pred == NULL)
- return false;
-
- PredExprSet * pred_expressions = pred->get_pred_expressions();
- if (pred_expressions->getSize() == 0) // unset predicates
- return false;
-
- int thread_id = id_to_int(tid);
- uint old_size = thrd_pruned_writes.size();
- if (thrd_pruned_writes.size() <= (uint) thread_id) {
- uint new_size = thread_id + 1;
- thrd_pruned_writes.resize(new_size);
- for (uint i = old_size;i < new_size;i++)
- thrd_pruned_writes[i] = new SnapVector<ModelAction *>();
- }
- SnapVector<ModelAction *> * pruned_writes = thrd_pruned_writes[thread_id];
- pruned_writes->clear(); // clear the old pruned_writes set
-
- bool pruned = false;
- uint rf_index = 0;
-
- while ( rf_index < rf_set->size() ) {
- ModelAction * write_act = (*rf_set)[rf_index];
- uint64_t write_val = write_act->get_write_value();
- bool no_predicate = false;
- bool satisfy_predicate = true;
-
- // Check if the write value satisfies the predicates
- PredExprSetIter * pred_expr_it = pred_expressions->iterator();
- while (pred_expr_it->hasNext()) {
- struct pred_expr * expression = pred_expr_it->next();
- bool equality;
-
- switch (expression->token) {
- case NOPREDICATE:
- no_predicate = true;
- break;
- case EQUALITY:
- FuncInst * to_be_compared;
- FuncNode * func_node;
- uint64_t last_read;
-
- to_be_compared = expression->func_inst;
- func_node = history->get_curr_func_node(tid);
- last_read = func_node->get_associated_read(tid, to_be_compared);
- ASSERT(last_read != VALUE_NONE);
-
- equality = (write_val == last_read);
- if (equality != expression->value)
- satisfy_predicate = false;
- break;
- case NULLITY:
- // TODO: implement likely to be null
- equality = ((void*) (write_val & 0xffffffff) == NULL);
- if (equality != expression->value)
- satisfy_predicate = false;
- break;
- default:
- model_print("unknown predicate token\n");
- break;
- }
-
- if (!satisfy_predicate)
- break;
- }
- delete pred_expr_it;
-
- if (no_predicate)
- return false;
-
- if (!satisfy_predicate) {
- ASSERT(rf_set != NULL);
- (*rf_set)[rf_index] = rf_set->back();
- rf_set->pop_back();
- pruned_writes->push_back(write_act);
- pruned = true;
- } else
- rf_index++;
- }
-
- return pruned;
-}
-
-/* @brief Put a thread to sleep because no writes in rf_set satisfies the selected predicate.
- *
- * @param thread A thread whose last action is a read
- */
-void NewFuzzer::conditional_sleep(Thread * thread)
-{
-/*
- int index = paused_thread_list.size();
-
- model->getScheduler()->add_sleep(thread);
- paused_thread_list.push_back(thread);
- paused_thread_table.put(thread, index); // Update table
-
- // Add the waiting condition to ModelHistory
- ModelAction * read = thread->get_pending();
- thread_id_t tid = thread->get_id();
- FuncNode * func_node = history->get_curr_func_node(tid);
- // inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
-
- Predicate * selected_branch = get_selected_child_branch(tid);
- // ConcretePredicate * concrete = selected_branch->evaluate(inst_act_map, tid);
- concrete->set_location(read->get_location());
-
- ASSERT(false);
-
- // history->add_waiting_write(concrete);
- // history->add_waiting_thread is already called in find_threads
- */
-}
-
-bool NewFuzzer::has_paused_threads()
-{
- return paused_thread_list.size() != 0;
-}
-
-Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
-{
- if (numthreads == 0 && has_paused_threads()) {
- wake_up_paused_threads(threadlist, &numthreads);
- //model_print("list size: %d, active t id: %d\n", numthreads, threadlist[0]);
- }
- int random_index = random() % numthreads;
- int thread = threadlist[random_index];
- thread_id_t curr_tid = int_to_id(thread);
- return execution->get_thread(curr_tid);
-}
-
-/* Force waking up one of threads paused by Fuzzer, because otherwise
- * the Fuzzer is not making progress
- */
-void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
-{
- int random_index = random() % paused_thread_list.size();
- Thread * thread = paused_thread_list[random_index];
- model->getScheduler()->remove_sleep(thread);
-
- Thread * last_thread = paused_thread_list.back();
- paused_thread_list[random_index] = last_thread;
- paused_thread_list.pop_back();
- paused_thread_table.put(last_thread, random_index); // Update table
- paused_thread_table.remove(thread);
-
- thread_id_t tid = thread->get_id();
- history->remove_waiting_write(tid);
- history->remove_waiting_thread(tid);
-
- threadlist[*numthreads] = tid;
- (*numthreads)++;
-
-/*--
- Predicate * selected_branch = get_selected_child_branch(tid);
- update_predicate_score(selected_branch, SLEEP_FAIL_TYPE3);
- */
-
- model_print("thread %d is woken up\n", tid);
-}
-
-/* Wake up conditional sleeping threads if the desired write is available */
-void NewFuzzer::notify_paused_thread(Thread * thread)
-{
- ASSERT(paused_thread_table.contains(thread));
-
- int index = paused_thread_table.get(thread);
- model->getScheduler()->remove_sleep(thread);
-
- Thread * last_thread = paused_thread_list.back();
- paused_thread_list[index] = last_thread;
- paused_thread_list.pop_back();
- paused_thread_table.put(last_thread, index); // Update table
- paused_thread_table.remove(thread);
-
- thread_id_t tid = thread->get_id();
- history->remove_waiting_write(tid);
- history->remove_waiting_thread(tid);
-
-/*--
- Predicate * selected_branch = get_selected_child_branch(tid);
- update_predicate_score(selected_branch, SLEEP_SUCCESS);
- */
-
- model_print("** thread %d is woken up\n", tid);
-}
-
-/* Find threads that may write values that the pending read action is waiting for.
- * Side effect: waiting thread related info are stored in dist_info_vec
- *
- * @return True if any thread is found
- */
-bool NewFuzzer::find_threads(ModelAction * pending_read)
-{
- ASSERT(pending_read->is_read());
-
- void * location = pending_read->get_location();
- thread_id_t self_id = pending_read->get_tid();
- bool finds_waiting_for = false;
-
- SnapVector<FuncNode *> * func_node_list = history->getWrFuncNodes(location);
- for (uint i = 0;i < func_node_list->size();i++) {
- FuncNode * target_node = (*func_node_list)[i];
- for (uint i = 1;i < execution->get_num_threads();i++) {
- thread_id_t tid = int_to_id(i);
- if (tid == self_id)
- continue;
-
- FuncNode * node = history->get_curr_func_node(tid);
- /* It is possible that thread tid is not in any FuncNode */
- if (node == NULL)
- continue;
-
- int distance = node->compute_distance(target_node);
- if (distance != -1) {
- finds_waiting_for = true;
- //model_print("thread: %d; distance from node %d to node %d: %d\n", tid, node->get_func_id(), target_node->get_func_id(), distance);
-
- dist_info_vec.push_back(node_dist_info(tid, target_node, distance));
- }
- }
- }
-
- return finds_waiting_for;
-}
+++ /dev/null
-#ifndef __NEWFUZZER_H__
-#define __NEWFUZZER_H__
-
-#include "fuzzer.h"
-#include "classlist.h"
-#include "mymemory.h"
-#include "stl-model.h"
-#include "predicate.h"
-
-struct node_dist_info {
- node_dist_info(thread_id_t tid, FuncNode * node, int distance) :
- tid(tid),
- target(node),
- dist(distance)
- {}
-
- thread_id_t tid;
- FuncNode * target;
- int dist;
-
- SNAPSHOTALLOC
-};
-
-class NewFuzzer : public Fuzzer {
-public:
- NewFuzzer();
- int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
- bool has_paused_threads();
- void notify_paused_thread(Thread * thread);
-
- Thread * selectThread(int * threadlist, int numthreads);
- Thread * selectNotify(simple_action_list_t * waiters);
- bool shouldSleep(const ModelAction * sleep);
- bool shouldWake(const ModelAction * sleep);
-
- void register_engine(ModelChecker * model, ModelExecution * execution);
- Predicate * get_selected_child_branch(thread_id_t tid);
-
- SNAPSHOTALLOC
-private:
- ModelHistory * history;
- ModelExecution * execution;
-
- SnapVector<ModelAction *> thrd_last_read_act;
- SnapVector<FuncInst *> thrd_last_func_inst;
-
- SnapVector<Predicate *> available_branches_tmp_storage;
- SnapVector<Predicate *> thrd_selected_child_branch;
- SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
-
- bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, SnapVector<ModelAction *> * rf_set);
- Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
- bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set);
- int choose_branch_index(SnapVector<Predicate *> * branches);
-
- /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
- */
- SnapVector<Thread *> paused_thread_list; //-- (not in use)
- HashTable<Thread *, int, uintptr_t, 0> paused_thread_table; //--
-
- SnapVector<struct node_dist_info> dist_info_vec; //--
-
- void conditional_sleep(Thread * thread); //--
- void wake_up_paused_threads(int * threadlist, int * numthreads); //--
-
- bool find_threads(ModelAction * pending_read); //--
-};
-
-#endif /* end of __NEWFUZZER_H__ */
+++ /dev/null
-#include "funcinst.h"
-#include "predicate.h"
-#include "concretepredicate.h"
-
-Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) :
- func_inst(func_inst),
- entry_predicate(is_entry),
- exit_predicate(is_exit),
- does_write(false),
- depth(0),
- weight(100),
- exploration_count(0),
- store_visible_count(0),
- total_checking_count(0),
- pred_expressions(16),
- children(),
- parent(NULL),
- exit(NULL),
- backedges(16)
-{}
-
-Predicate::~Predicate()
-{
- // parent and func_inst should not be deleted
- pred_expressions.reset();
- backedges.reset();
- children.clear();
-}
-
-unsigned int pred_expr_hash(struct pred_expr * expr)
-{
- return (unsigned int)((uintptr_t)expr);
-}
-
-bool pred_expr_equal(struct pred_expr * p1, struct pred_expr * p2)
-{
- if (p1->token != p2->token)
- return false;
- if (p1->token == EQUALITY && p1->func_inst != p2->func_inst)
- return false;
- if (p1->value != p2->value)
- return false;
- return true;
-}
-
-void Predicate::add_predicate_expr(token_t token, FuncInst * func_inst, bool value)
-{
- struct pred_expr *ptr = new pred_expr(token, func_inst, value);
- pred_expressions.add(ptr);
-}
-
-void Predicate::add_child(Predicate * child)
-{
- /* check duplication? */
- children.push_back(child);
-}
-
-void Predicate::set_parent(Predicate * parent_pred)
-{
- parent = parent_pred;
- depth = parent_pred->get_depth() + 1;
-}
-
-void Predicate::set_exit(Predicate * exit_pred)
-{
- exit = exit_pred;
-}
-
-void Predicate::copy_predicate_expr(Predicate * other)
-{
- PredExprSet * other_pred_expressions = other->get_pred_expressions();
- PredExprSetIter * it = other_pred_expressions->iterator();
-
- while (it->hasNext()) {
- struct pred_expr * ptr = it->next();
- struct pred_expr * copy = new pred_expr(ptr->token, ptr->func_inst, ptr->value);
- pred_expressions.add(copy);
- }
-
- delete it;
-}
-
-/* Evaluate predicate expressions against the given inst_act_map */
-ConcretePredicate * Predicate::evaluate(thread_id_t tid)
-{
- /*
- ConcretePredicate * concrete = new ConcretePredicate(tid);
- 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->add_expression(ptr->token, value, ptr->value);
- }
-
- delete it;
- return concrete;
- */
-
- return NULL;
-}
-
-void Predicate::print_predicate()
-{
- model_print("\"%p\" [shape=box, label=\"", this);
- if (entry_predicate) {
- model_print("entry node\"];\n");
- return;
- }
-
- if (exit_predicate) {
- model_print("exit node\"];\n");
- return;
- }
-
- model_print("depth: %u; weight: %g\n", depth, weight);
-
- func_inst->print();
-
- if (pred_expressions.getSize() == 0)
- model_print("predicate unset\n");
-
- PredExprSetIter * it = pred_expressions.iterator();
- while (it->hasNext()) {
- struct pred_expr * expr = it->next();
- FuncInst * inst = expr->func_inst;
- switch (expr->token) {
- case NOPREDICATE:
- break;
- case EQUALITY:
- model_print("predicate token: equality, position: %s, value: %d\n", inst->get_position(), expr->value);
- break;
- case NULLITY:
- model_print("predicate token: nullity, value: %d\n", expr->value);
- break;
- default:
- model_print("unknown predicate token\n");
- break;
- }
- }
-
- if (does_write) {
- model_print("Does write\n");
- }
-
- double prob = (double) store_visible_count / total_checking_count;
- model_print("Total checks: %d, visible count: %d; prob: %f\n", total_checking_count, store_visible_count, prob);
- model_print("Exploration count: %d, failure count: %d", exploration_count, failure_count);
- model_print("\"];\n");
-
- delete it;
-}
-
-void Predicate::print_pred_subtree()
-{
- print_predicate();
- for (uint i = 0;i < children.size();i++) {
- Predicate * child = children[i];
- child->print_pred_subtree();
- model_print("\"%p\" -> \"%p\"\n", this, child);
- }
-
- PredSetIter * it = backedges.iterator();
- while (it->hasNext()) {
- Predicate * backedge = it->next();
- model_print("\"%p\" -> \"%p\"[style=dashed, color=grey]\n", this, backedge);
- }
-
- if (exit) {
- model_print("\"%p\" -> \"%p\"[style=dashed, color=red]\n", this, exit);
- }
-
- delete it;
-}
+++ /dev/null
-#ifndef __PREDICATE_H__
-#define __PREDICATE_H__
-
-#include "hashset.h"
-#include "predicatetypes.h"
-#include "classlist.h"
-
-#define MAX_DEPTH 0x7fffffff
-
-unsigned int pred_expr_hash (struct pred_expr *);
-bool pred_expr_equal(struct pred_expr *, struct pred_expr *);
-typedef HashSet<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSet;
-typedef HSIterator<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSetIter;
-
-class Predicate {
-public:
- Predicate(FuncInst * func_inst, bool is_entry = false, bool is_exit = false);
- ~Predicate();
-
- FuncInst * get_func_inst() { return func_inst; }
- PredExprSet * get_pred_expressions() { return &pred_expressions; }
-
- 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);
- void add_backedge(Predicate * back_pred) { backedges.add(back_pred); }
- void set_weight(double weight_) { weight = weight_; }
- void copy_predicate_expr(Predicate * other);
-
- Predicate * follow_write_child(FuncInst * inst);
- ModelVector<Predicate *> * get_children() { return &children; }
- 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; }
-
- /* Whether func_inst does write or not */
- bool is_write() { return does_write; }
- void set_write(bool is_write) { does_write = is_write; }
-
- ConcretePredicate * evaluate(thread_id_t tid);
-
- uint32_t get_expl_count() { return exploration_count; }
- uint32_t get_fail_count() { return failure_count; }
- uint32_t get_store_visible_count() { return store_visible_count; }
- uint32_t get_total_checking_count() { return total_checking_count; }
-
- void incr_expl_count() { exploration_count++; }
- void incr_fail_count() { failure_count++; }
- void incr_store_visible_count() { store_visible_count++; }
- void incr_total_checking_count() { total_checking_count++; }
-
- uint32_t get_depth() { return depth; }
- void set_depth(uint32_t depth_) { depth = depth_; }
-
- void print_predicate();
- void print_pred_subtree();
-
- MEMALLOC
-private:
- FuncInst * func_inst;
- bool entry_predicate;
- bool exit_predicate;
- bool does_write;
-
- /* Height of this predicate node in the predicate tree */
- uint32_t depth;
- double weight;
-
- uint32_t exploration_count;
- uint32_t failure_count;
- uint32_t store_visible_count;
- uint32_t total_checking_count; /* The number of times the store visibility is checked */
-
- /* May have multiple predicate expressions */
- PredExprSet pred_expressions;
- ModelVector<Predicate *> children;
-
- /* Only a single parent may exist */
- Predicate * parent;
- Predicate * exit;
-
- /* May have multiple back edges, e.g. nested loops */
- PredSet backedges;
-};
-
-#endif /* __PREDICATE_H__ */
+++ /dev/null
-#include "waitobj.h"
-#include "threads-model.h"
-#include "funcnode.h"
-
-#define COUNTER_THRESHOLD 1000
-
-WaitObj::WaitObj(thread_id_t tid) :
- tid(tid),
- waiting_for(32),
- waited_by(32),
- thrd_dist_maps(),
- thrd_target_nodes(),
- thrd_action_counters()
-{}
-
-WaitObj::~WaitObj()
-{
- for (uint i = 0;i < thrd_dist_maps.size();i++)
- delete thrd_dist_maps[i];
-
- for (uint i = 0;i < thrd_target_nodes.size();i++)
- delete thrd_target_nodes[i];
-}
-
-void WaitObj::add_waiting_for(thread_id_t other, FuncNode * node, int dist)
-{
- waiting_for.add(other);
-
- dist_map_t * dist_map = getDistMap(other);
- dist_map->put(node, dist);
-
- node_set_t * target_nodes = getTargetNodes(other);
- target_nodes->add(node);
-}
-
-void WaitObj::add_waited_by(thread_id_t other)
-{
- waited_by.add(other);
-}
-
-/**
- * Stop waiting for the thread to reach the target node
- *
- * @param other The thread to be removed
- * @param node The target node
- * @return true if "other" is removed from waiting_for set
- * false if only a target node of "other" is removed
- */
-bool WaitObj::remove_waiting_for_node(thread_id_t other, FuncNode * node)
-{
- dist_map_t * dist_map = getDistMap(other);
- dist_map->remove(node);
-
- node_set_t * target_nodes = getTargetNodes(other);
- target_nodes->remove(node);
-
- /* The thread has no nodes to reach */
- if (target_nodes->isEmpty()) {
- int index = id_to_int(other);
- thrd_action_counters[index] = 0;
- waiting_for.remove(other);
-
- return true;
- }
-
- return false;
-}
-
-/* Stop waiting for the thread */
-void WaitObj::remove_waiting_for(thread_id_t other)
-{
- waiting_for.remove(other);
-
- // TODO: clear dist_map or not?
- /* dist_map_t * dist_map = getDistMap(other);
- dist_map->reset(); */
-
- node_set_t * target_nodes = getTargetNodes(other);
- target_nodes->reset();
-
- int index = id_to_int(other);
- thrd_action_counters[index] = 0;
-}
-
-void WaitObj::remove_waited_by(thread_id_t other)
-{
- waited_by.remove(other);
-}
-
-int WaitObj::lookup_dist(thread_id_t tid, FuncNode * target)
-{
- dist_map_t * map = getDistMap(tid);
- node_set_t * node_set = getTargetNodes(tid);
-
- /* thrd_dist_maps is not reset when clear_waiting_for is called,
- * so node_set should be checked */
- if (node_set->contains(target) && map->contains(target))
- return map->get(target);
-
- return -1;
-}
-
-dist_map_t * WaitObj::getDistMap(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int old_size = thrd_dist_maps.size();
-
- if (old_size <= thread_id) {
- thrd_dist_maps.resize(thread_id + 1);
- for (int i = old_size;i < thread_id + 1;i++) {
- thrd_dist_maps[i] = new dist_map_t(16);
- }
- }
-
- return thrd_dist_maps[thread_id];
-}
-
-node_set_t * WaitObj::getTargetNodes(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
- int old_size = thrd_target_nodes.size();
-
- if (old_size <= thread_id) {
- thrd_target_nodes.resize(thread_id + 1);
- for (int i = old_size;i < thread_id + 1;i++) {
- thrd_target_nodes[i] = new node_set_t(16);
- }
- }
-
- return thrd_target_nodes[thread_id];
-}
-
-/**
- * Increment action counter for thread tid
- * @return true if the counter for tid expires
- */
-bool WaitObj::incr_counter(thread_id_t tid)
-{
- int thread_id = id_to_int(tid);
-
- /* thrd_action_counters.resize does not work here */
- while (thrd_action_counters.size() <= (uint) thread_id) {
- thrd_action_counters.push_back(0);
- }
-
- thrd_action_counters[thread_id]++;
- if (thrd_action_counters[thread_id] > COUNTER_THRESHOLD) {
- thrd_action_counters[thread_id] = 0;
- return true;
- }
-
- return false;
-}
-
-void WaitObj::clear_waiting_for()
-{
- thrd_id_set_iter * iter = waiting_for.iterator();
- while (iter->hasNext()) {
- thread_id_t tid = iter->next();
- int index = id_to_int(tid);
- thrd_action_counters[index] = 0;
-
- /* thrd_dist_maps are not reset because distances
- * will be overwritten when node targets are added
- * thrd_dist_maps[index]->reset(); */
-
- node_set_t * target_nodes = getTargetNodes(tid);
- target_nodes->reset();
- }
-
- delete iter;
-
- waiting_for.reset();
- /* waited_by relation should be kept */
-}
-
-void WaitObj::print_waiting_for(bool verbose)
-{
- if (waiting_for.getSize() == 0)
- return;
-
- model_print("thread %d is waiting for: ", tid);
- thrd_id_set_iter * it = waiting_for.iterator();
-
- while (it->hasNext()) {
- thread_id_t waiting_for_id = it->next();
- model_print("%d ", waiting_for_id);
- }
- model_print("\n");
- delete it;
-
- if (verbose) {
- /* Print out the distances from each thread to target nodes */
- model_print("\t");
- for (uint i = 0;i < thrd_target_nodes.size();i++) {
- dist_map_t * dist_map = getDistMap(i);
- node_set_t * node_set = getTargetNodes(i);
- node_set_iter * node_iter = node_set->iterator();
-
- if (!node_set->isEmpty()) {
- model_print("[thread %d](", int_to_id(i));
-
- while (node_iter->hasNext()) {
- FuncNode * node = node_iter->next();
- int dist = dist_map->get(node);
- model_print("node %d: %d, ", node->get_func_id(), dist);
- }
- model_print(") ");
- }
-
- delete node_iter;
- }
- model_print("\n");
- }
-}
-
-void WaitObj::print_waited_by()
-{
- if (waited_by.getSize() == 0)
- return;
-
- model_print("thread %d is waited by: ", tid);
- thrd_id_set_iter * it = waited_by.iterator();
-
- while (it->hasNext()) {
- thread_id_t thread_id = it->next();
- model_print("%d ", thread_id);
- }
- model_print("\n");
-
- delete it;
-}
+++ /dev/null
-#ifndef __WAITOBJ_H__
-#define __WAITOBJ_H__
-
-#include "classlist.h"
-#include "modeltypes.h"
-
-typedef HashTable<FuncNode *, int, uintptr_t, 0> dist_map_t;
-typedef HashSet<FuncNode *, uintptr_t, 0> node_set_t;
-typedef HSIterator<FuncNode *, uintptr_t, 0> node_set_iter;
-
-class WaitObj {
-public:
- WaitObj(thread_id_t);
- ~WaitObj();
-
- thread_id_t get_tid() { return tid; }
-
- void add_waiting_for(thread_id_t other, FuncNode * node, int dist);
- void add_waited_by(thread_id_t other);
- bool remove_waiting_for_node(thread_id_t other, FuncNode * node);
- void remove_waiting_for(thread_id_t other);
- void remove_waited_by(thread_id_t other);
-
- thrd_id_set_t * getWaitingFor() { return &waiting_for; }
- thrd_id_set_t * getWaitedBy() { return &waited_by; }
-
- node_set_t * getTargetNodes(thread_id_t tid);
- int lookup_dist(thread_id_t tid, FuncNode * target);
-
- bool incr_counter(thread_id_t tid);
-
- void clear_waiting_for();
-
- void print_waiting_for(bool verbose = false);
- void print_waited_by();
-
- SNAPSHOTALLOC
-private:
- thread_id_t tid;
-
- /* The set of threads this thread (tid) is waiting for */
- thrd_id_set_t waiting_for;
-
- /* The set of threads waiting for this thread */
- thrd_id_set_t waited_by;
-
- SnapVector<dist_map_t *> thrd_dist_maps;
- SnapVector<node_set_t *> thrd_target_nodes;
-
- /* Count the number of actions for threads that
- * this thread is waiting for */
- SnapVector<uint32_t> thrd_action_counters;
-
- dist_map_t * getDistMap(thread_id_t tid);
-};
-
-#endif
projects / c11tester.git / commitdiff