/**
- * @brief Construct a new ModelAction
+ * @brief Construct a new ModelAction for sleep actions
*
- * @param type The type of action
+ * @param type The type of action: THREAD_SLEEP
* @param order The memory order of this action. A "don't care" for non-ATOMIC
* actions (e.g., THREAD_* or MODEL_* actions).
* @param loc The location that this action acts upon
- * @param value (optional) A value associated with the action (e.g., the value
- * read or written). Defaults to a given macro constant, for debugging purposes.
- * @param thread (optional) The Thread in which this action occurred. If NULL
- * (default), then a Thread is assigned according to the scheduler.
+ * @param value The time duration a thread is scheduled to sleep.
+ * @param _time The this sleep action is constructed
*/
ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t _time) :
location(NULL),
*/
void cds_func_entry(const char * funcName) {
- if (!model) return;
-
+ ensureModel();
Thread * th = thread_current();
uint32_t func_id;
}
void cds_func_exit(const char * funcName) {
- if (!model) return;
-
+ ensureModel();
Thread * th = thread_current();
uint32_t func_id;
mo_graph(new CycleGraph()),
fuzzer(new Fuzzer()),
thrd_func_list(),
- thrd_func_inst_lists(),
+ thrd_func_act_lists(),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
ASSERT(curr);
/* Process this action in ModelHistory for records*/
- // model->get_history()->process_action( curr, curr->get_tid() );
+ model->get_history()->process_action( curr, curr->get_tid() );
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
ModelAction * check_current_action(ModelAction *curr);
SnapVector<func_id_list_t> * get_thrd_func_list() { return &thrd_func_list; }
- SnapVector< SnapList<func_inst_list_t *> *> * get_thrd_func_inst_lists() { return &thrd_func_inst_lists; }
+ SnapVector< SnapList<action_list_t *> *> * get_thrd_func_act_lists() { return &thrd_func_act_lists; }
bool isFinished() {return isfinished;}
void setFinished() {isfinished = true;}
*
* This data structure is handled by ModelHistory
*/
- SnapVector< SnapList< func_inst_list_t *> *> thrd_func_inst_lists;
+ SnapVector< SnapList<action_list_t *> *> thrd_func_act_lists;
bool isfinished;
};
#include "funcnode.h"
-#include "predicate.h"
FuncNode::FuncNode() :
+ predicate_tree_initialized(false),
func_inst_map(),
inst_list(),
entry_insts(),
- thrd_read_map(),
- read_locations()
+ thrd_read_map()
{}
/* Check whether FuncInst with the same type, position, and location
* if not, add it and return it.
*
* @return FuncInst with the same type, position, and location as act */
-FuncInst * FuncNode::get_or_add_action(ModelAction *act)
+FuncInst * FuncNode::get_or_add_inst(ModelAction *act)
{
ASSERT(act);
const char * position = act->get_position();
return;
mllnode<FuncInst*>* it;
- for (it = entry_insts.begin();it != NULL;it=it->getNext()) {
+ for (it = entry_insts.begin(); it != NULL; it = it->getNext()) {
if (inst == it->getVal())
return;
}
entry_insts.push_back(inst);
}
-/* @param inst_list a list of FuncInsts; this argument comes from ModelExecution
- * Link FuncInsts in a list - add one FuncInst to another's predecessors and successors
+/* @param act_list a list of ModelActions; this argument comes from ModelExecution
+ * convert act_inst to inst_list do linking - add one FuncInst to another's predecessors and successors
*/
-void FuncNode::link_insts(func_inst_list_t * inst_list)
+void FuncNode::update_inst_tree(action_list_t * act_list)
{
- if (inst_list == NULL)
+ if (act_list == NULL)
+ return;
+ else if (act_list->size() == 0)
return;
- sllnode<FuncInst *>* it = inst_list->begin();
- sllnode<FuncInst *>* prev;
+ /* build inst_list from act_list for later processing */
+ func_inst_list_t inst_list;
+ for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
+ ModelAction * act = it->getVal();
+ FuncInst * func_inst = get_or_add_inst(act);
- if (inst_list->size() == 0)
- return;
+ if (func_inst != NULL)
+ inst_list.push_back(func_inst);
+ }
+
+ /* 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();
+ it = it->getNext();
while (it != NULL) {
- prev = it;
prev = it->getPrev();
FuncInst * prev_inst = prev->getVal();
prev_inst->add_succ(curr_inst);
curr_inst->add_pred(prev_inst);
- it=it->getNext();
+ it = it->getNext();
}
}
uint32_t old_size = thrd_read_map.size();
if (old_size <= tid) {
thrd_read_map.resize(tid + 1);
- for (uint32_t i = old_size;i < tid + 1;i++)
+ for (uint32_t i = old_size; i < tid + 1;i++)
thrd_read_map[i] = new read_map_t();
}
read_map->put(location, read_from_val);
/* Store the memory locations where atomic reads happen */
- bool push_loc = true;
- mllnode<void *> * it;
- for (it = read_locations.begin();it != NULL;it=it->getNext()) {
- if (location == it->getVal()) {
- push_loc = false;
- break;
- }
- }
-
- if (push_loc)
- read_locations.push_back(location);
+ // read_locations.add(location);
}
uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
thrd_read_map[tid]->reset();
}
+void FuncNode::init_predicate_tree(func_inst_list_t * inst_list)
+{
+ if (inst_list == NULL || inst_list->size() == 0)
+ return;
+
+ if (predicate_tree_initialized)
+ return;
+
+ predicate_tree_initialized = true;
+
+ // maybe restrict the size of hashtable to save calloc time
+ HashTable<void *, FuncInst *, uintptr_t, 4> loc_inst_map;
+
+ sllnode<FuncInst *> *it = inst_list->begin();
+ sllnode<FuncInst *> *prev;
+
+ FuncInst * entry_inst = it->getVal();
+
+ /* entry instruction has no predicate expression */
+ Predicate * pred_entry = new Predicate(entry_inst);
+ loc_inst_map.put(entry_inst->get_location(), entry_inst);
+
+ it = it->getNext();
+ while (it != NULL) {
+ prev = it->getPrev();
+
+ FuncInst * curr_inst = it->getVal();
+ FuncInst * prev_inst = prev->getVal();
+
+ if ( loc_inst_map.contains(curr_inst->get_location()) ) {
+ Predicate * pred1 = new Predicate(curr_inst);
+ pred1->add_predicate(EQUALITY, curr_inst->get_location(), 0);
+
+ Predicate * pred2 = new Predicate(curr_inst);
+ pred2->add_predicate(EQUALITY, curr_inst->get_location(), 1);
+ }
+
+ loc_inst_map.put(curr_inst->get_location(), curr_inst);
+
+ it = it->getNext();
+ }
+}
+
+
void FuncNode::generate_predicate(FuncInst *func_inst)
{
{
ASSERT(thrd_read_map.size() > tid);
read_map_t * read_map = thrd_read_map[tid];
-
+/*
mllnode<void *> * it;
for (it = read_locations.begin();it != NULL;it=it->getNext()) {
if ( !read_map->contains(it->getVal()) )
uint64_t read_val = read_map->get(it->getVal());
model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val);
}
+*/
}
#include "action.h"
#include "funcinst.h"
#include "hashtable.h"
+#include "hashset.h"
+#include "predicate.h"
typedef ModelList<FuncInst *> func_inst_list_mt;
typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
void set_func_id(uint32_t id) { func_id = id; }
void set_func_name(const char * name) { func_name = name; }
- FuncInst * get_or_add_action(ModelAction *act);
+ FuncInst * get_or_add_inst(ModelAction *act);
HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }
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 link_insts(func_inst_list_t * inst_list);
+ void update_inst_tree(action_list_t * act_list);
void store_read(ModelAction * act, uint32_t tid);
uint64_t query_last_read(void * location, uint32_t tid);
void clear_read_map(uint32_t tid);
/* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
+ void init_predicate_tree(func_inst_list_t * inst_list);
void generate_predicate(FuncInst * func_inst);
void print_last_read(uint32_t tid);
private:
uint32_t func_id;
const char * func_name;
+ bool predicate_tree_initialized;
/* Use source line number as the key of hashtable, to check if
* atomic operation with this line number has been added or not
/* Store the values read by atomic read actions per memory location for each thread */
ModelVector<read_map_t *> thrd_read_map;
- ModelList<void *> read_locations;
+
+ /* TODO: how to guarantee unique predicate? Or add an equal function */
+ HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> predicate_tree_entry;
};
-#endif /* __FUNCNODE_H__ */
+#endif /* __FUNCNODE_H__ */
func_map(),
func_map_rev(),
func_nodes(),
- write_history()
+ write_history(),
+ write_locations()
{}
void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
//model_print("thread %d entering func %d\n", tid, func_id);
uint32_t id = id_to_int(tid);
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
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++) {
+ for (uint i = oldsize; i < id + 1; i++) {
new(&(*thrd_func_list)[i]) func_id_list_t();
+ // push 0 as a dummy function id to a void seg fault
+ (*thrd_func_list)[i].push_back(0);
}
- thrd_func_inst_lists->resize( id + 1 );
+
+ thrd_func_act_lists->resize( id + 1 );
}
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ SnapList<action_list_t *> * func_act_lists = thrd_func_act_lists->at(id);
- if (func_inst_lists == NULL) {
- func_inst_lists = new SnapList< func_inst_list_t *>();
- thrd_func_inst_lists->at(id) = func_inst_lists;
+ if (func_act_lists == NULL) {
+ func_act_lists = new SnapList<action_list_t *>();
+ thrd_func_act_lists->at(id) = func_act_lists;
}
(*thrd_func_list)[id].push_back(func_id);
- func_inst_lists->push_back( new func_inst_list_t() );
+ func_act_lists->push_back( new action_list_t() );
if ( func_nodes.size() <= func_id )
resize_func_nodes( func_id + 1 );
{
uint32_t id = id_to_int(tid);
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ SnapList<action_list_t *> * func_act_lists = thrd_func_act_lists->at(id);
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->clear_read_map(tid);
- func_inst_list_t * curr_inst_list = func_inst_lists->back();
- func_node->link_insts(curr_inst_list);
+ action_list_t * curr_act_list = func_act_lists->back();
+ func_node->update_inst_tree(curr_act_list);
(*thrd_func_list)[id].pop_back();
- func_inst_lists->pop_back();
+ func_act_lists->pop_back();
} else {
model_print("trying to exit with a wrong function id\n");
model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
/* return if thread i has not entered any function or has exited
from all functions */
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
uint32_t id = id_to_int(tid);
if ( thrd_func_list->size() <= id )
/* get the function id that thread i is currently in */
uint32_t func_id = (*thrd_func_list)[id].back();
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ SnapList<action_list_t *> * func_act_lists = thrd_func_act_lists->at(id);
- if ( func_nodes.size() <= func_id )
+ if (func_id == 0)
+ return;
+ else if ( func_nodes.size() <= func_id )
resize_func_nodes( func_id + 1 );
FuncNode * func_node = func_nodes[func_id];
ASSERT (func_node != NULL);
- /* add corresponding FuncInst to func_node */
- FuncInst * inst = func_node->get_or_add_action(act);
-
- if (inst == NULL)
+ /* do not care actions without a position */
+ if (act->get_position() == NULL)
return;
- // if (inst->is_read())
- // func_node->store_read(act, tid);
+ if (act->is_read())
+ func_node->store_read(act, tid);
- if (inst->is_write())
+ if (act->is_write())
add_to_write_history(act->get_location(), act->get_write_value());
/* add to curr_inst_list */
- func_inst_list_t * curr_inst_list = func_inst_lists->back();
- ASSERT(curr_inst_list != NULL);
- curr_inst_list->push_back(inst);
+ action_list_t * curr_act_list = func_act_lists->back();
+ ASSERT(curr_act_list != NULL);
+ curr_act_list->push_back(act);
}
/* return the FuncNode given its func_id */
void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
{
- if ( !write_history.contains(location) )
- write_history.put(location, new write_set_t() );
-
write_set_t * write_set = write_history.get(location);
+
+ if (write_set == NULL) {
+ write_set = new write_set_t();
+ write_history.put(location, write_set);
+ }
+
write_set->add(write_val);
+ write_locations.add(location);
+}
+
+void ModelHistory::print_write()
+{
}
-void ModelHistory::print()
+void ModelHistory::print_func_node()
{
/* function id starts with 1 */
- for (uint32_t i = 1;i < func_nodes.size();i++) {
+ for (uint32_t i = 1; i < func_nodes.size(); i++) {
FuncNode * func_node = func_nodes[i];
func_inst_list_mt * entry_insts = func_node->get_entry_insts();
FuncInst *inst = it->getVal();
model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
}
-
/*
func_inst_list_mt * inst_list = funcNode->get_inst_list();
FuncInst *inst = *it;
model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
}
- */
+*/
}
}
void add_to_write_history(void * location, uint64_t write_val);
- void print();
+ void print_write();
+ void print_func_node();
MEMALLOC
private:
ModelVector<const char *> func_map_rev;
ModelVector<FuncNode *> func_nodes;
+
HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
+ HashSet<void *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_locations;
};
#endif /* __HISTORY_H__ */
int user_main(int, char**);
}
-void check();
#endif
#include "predicate.h"
-inline bool operator==(const predicate_expr& expr_A, const predicate_expr& expr_B)
+Predicate::Predicate(FuncInst * func_inst) :
+ func_inst(func_inst)
+{}
+
+unsigned int pred_expr_hash(struct pred_expr * expr) {
+ return (unsigned int)((uintptr_t)hash);
+}
+
+bool pred_expr_equal(struct pred_expr * p1, struct pred_expr * p2)
{
- if (expr_A.token != expr_B.token)
+ if (p1->token != p2->token)
return false;
-
- if (expr_A.token == EQUALITY && expr_A.location != expr_B.location)
+ if (p1->token == EQUALITY && p1->location != p2->location)
return false;
-
- if (expr_A.value != expr_B.value)
+ if (p1->value != p2->value)
return false;
-
return true;
}
-void Predicate::add_predicate(predicate_expr predicate)
+void Predicate::add_predicate(token_t token, void * location, bool value)
{
- ModelList<predicate_expr>::iterator it;
- for (it = predicates.begin();it != predicates.end();it++) {
- if (predicate == *it)
- return;
- }
-
- predicates.push_back(predicate);
+ struct pred_expr = {token, location, value};
+ predicates.add(&predicate);
}
+#ifndef __PREDICTAE_H__
+#define __PREDICATE_H__
+
#include "funcinst.h"
+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> PredicateSet;
+
typedef enum predicate_token {
EQUALITY, NULLITY
} token_t;
* this load should read the same value as the last value
* read at memory location specified in predicate_expr.
*/
-struct predicate_expr {
+struct pred_expr {
token_t token;
void * location;
bool value;
};
+
class Predicate {
public:
- Predicate();
+ Predicate(FuncInst * func_inst);
~Predicate();
FuncInst * get_func_inst() { return func_inst; }
- ModelList<predicate_expr> * get_predicates() { return &predicates; }
- void add_predicate(predicate_expr predicate);
+ PredicateSet * get_predicates() { return &predicates; }
+ void add_predicate(token_t token, void * location, bool value);
MEMALLOC
private:
FuncInst * func_inst;
/* may have multiple precicates */
- ModelList<predicate_expr> predicates;
+ PredicateSet predicates;
+ ModelVector<Predicate *> children;
};
+
+#endif /* __PREDICATE_H__ */
#include "mutex.h"
#include <condition_variable>
-#include <assert.h>
/* global "model" object */
#include "model.h"
}
int pthread_join(pthread_t t, void **value_ptr) {
-// Thread *th = model->get_pthread(t);
ModelExecution *execution = model->get_execution();
Thread *th = execution->get_pthread(t);
}
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
- cdsc::snapmutex *m = new cdsc::snapmutex();
-
if (!model) {
snapshot_system_init(10000, 1024, 1024, 40000);
model = new ModelChecker();
model->startChecker();
}
+ cdsc::snapmutex *m = new cdsc::snapmutex();
ModelExecution *execution = model->get_execution();
execution->getMutexMap()->put(p_mutex, m);
model->startChecker();
}
-
ModelExecution *execution = model->get_execution();
/* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
pthread_mutex_init(p_mutex, NULL);
cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
- // cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
+// cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v));
// v->wait(*m);
v->notify_all();
return 0;
}
+
+int pthread_cond_destroy(pthread_cond_t *p_cond) {
+ ModelExecution *execution = model->get_execution();
+
+ if (execution->getCondMap()->contains(p_cond)) {
+ cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
+ delete v;
+ execution->getCondMap()->remove(p_cond);
+ }
+ return 0;
+}