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
+ concretepredicate.o waitobj.o hashfunction.o pipe.o actionlist.o
CPPFLAGS += -Iinclude -I.
LDFLAGS := -ldl -lrt -rdynamic -lpthread
last_fence_release(NULL),
cv(NULL),
rf_cv(NULL),
- trace_ref(NULL),
- thrdmap_ref(NULL),
- action_ref(NULL),
value(value),
type(type),
order(order),
last_fence_release(NULL),
cv(NULL),
rf_cv(NULL),
- trace_ref(NULL),
- thrdmap_ref(NULL),
- action_ref(NULL),
value(value),
type(type),
order(order),
last_fence_release(NULL),
cv(NULL),
rf_cv(NULL),
- trace_ref(NULL),
- thrdmap_ref(NULL),
- action_ref(NULL),
value(value),
type(type),
order(order),
last_fence_release(NULL),
cv(NULL),
rf_cv(NULL),
- trace_ref(NULL),
- thrdmap_ref(NULL),
- action_ref(NULL),
value(value),
type(type),
order(order),
last_fence_release(NULL),
cv(NULL),
rf_cv(NULL),
- trace_ref(NULL),
- thrdmap_ref(NULL),
- action_ref(NULL),
value(value),
type(type),
order(order),
/* to accomodate pthread create and join */
Thread * thread_operand;
void set_thread_operand(Thread *th) { thread_operand = th; }
- void setTraceRef(sllnode<ModelAction *> *ref) { trace_ref = ref; }
- void setThrdMapRef(sllnode<ModelAction *> *ref) { thrdmap_ref = ref; }
- void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
- sllnode<ModelAction *> * getTraceRef() { return trace_ref; }
- sllnode<ModelAction *> * getThrdMapRef() { return thrdmap_ref; }
- sllnode<ModelAction *> * getActionRef() { return action_ref; }
SNAPSHOTALLOC
private:
*/
ClockVector *cv;
ClockVector *rf_cv;
- sllnode<ModelAction *> * trace_ref;
- sllnode<ModelAction *> * thrdmap_ref;
- sllnode<ModelAction *> * action_ref;
/** @brief The value written (for write or RMW; undefined for read) */
uint64_t value;
--- /dev/null
+#include "actionlist.h"
+#include "action.h"
+#include <string.h>
+#include "stl-model.h"
+#include <limits.h>
+
+actionlist::actionlist() :
+ _size(0)
+{
+}
+
+actionlist::~actionlist() {
+}
+
+allnode::allnode() :
+ count(0) {
+ bzero(children, sizeof(children));
+}
+
+allnode::~allnode() {
+ if (count != 0)
+ for(int i=0;i<ALLNODESIZE;i++) {
+ if (children[i] != NULL && !(((uintptr_t) children[i]) & ISACT))
+ delete children[i];
+ }
+}
+
+sllnode<ModelAction *> * allnode::findPrev(modelclock_t index) {
+ allnode * ptr = this;
+ modelclock_t increment = 1;
+ modelclock_t mask = ALLMASK;
+ int totalshift = 0;
+ index -= increment;
+
+ while(1) {
+ modelclock_t shiftclock = index >> totalshift;
+ modelclock_t currindex = shiftclock & ALLMASK;
+
+ //See if we went negative...
+ if (currindex != ALLMASK) {
+ if (ptr->children[currindex] == NULL) {
+ //need to keep searching at this level
+ index -= increment;
+ continue;
+ } else {
+ //found non-null...
+ if (totalshift != 0)
+ ptr = ptr->children[currindex];
+ //need to increment here...
+ increment = increment >> ALLBITS;
+ mask = mask >> ALLBITS;
+ totalshift -= ALLBITS;
+ break;
+ }
+ }
+ //If we get here, we already did the decrement earlier...no need to decrement again
+ ptr = ptr->parent;
+ increment = increment << ALLBITS;
+ mask = mask << ALLBITS;
+ totalshift += ALLBITS;
+
+ if (increment == 0) {
+ return NULL;
+ }
+ }
+
+ while(1) {
+ while(1) {
+ modelclock_t shiftclock = index >> totalshift;
+ modelclock_t currindex = shiftclock & ALLMASK;
+ if (ptr->children[currindex] != NULL) {
+ if (totalshift != 0) {
+ ptr = ptr->children[currindex];
+ } else {
+ allnode * act = ptr->children[currindex];
+ sllnode<ModelAction *> * node = reinterpret_cast<sllnode<ModelAction *>*>(((uintptr_t)act) & ALLMASK);
+ return node;
+ }
+ }
+ index -= increment;
+ }
+
+ increment = increment >> ALLBITS;
+ mask = mask >> ALLBITS;
+ totalshift -= ALLBITS;
+ }
+}
+
+void actionlist::addAction(ModelAction * act) {
+ _size++;
+ int shiftbits = MODELCLOCKBITS - ALLBITS;
+ modelclock_t clock = act->get_seq_number();
+
+ allnode * ptr = &root;
+ do {
+ int index = (clock >> shiftbits) & ALLMASK;
+ allnode * tmp = ptr->children[index];
+ if (shiftbits == 0) {
+ sllnode<ModelAction *> * llnode = new sllnode<ModelAction *>();
+ llnode->val = act;
+ if (tmp == NULL) {
+ ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t) llnode) | ISACT);
+ sllnode<ModelAction *> * llnodeprev = ptr->findPrev(index);
+ if (llnodeprev != NULL) {
+
+ llnode->next = llnodeprev->next;
+ llnode->prev = llnodeprev;
+
+ //see if we are the new tail
+ if (llnodeprev->next == NULL)
+ tail = llnode;
+ else
+ llnode->next->prev = llnode;
+
+ llnodeprev->next = llnode;
+ } else {
+ //We are the begining
+ llnode->next = head;
+ llnode->prev = NULL;
+ if (head != NULL) {
+ head->prev = llnode;
+ } else {
+ //we are the first node
+ tail = llnode;
+ }
+
+ head = llnode;
+ }
+ //need to find next link
+ ptr->count++;
+ } else {
+ //handle case where something else is here
+
+ sllnode<ModelAction *> * llnodeprev = reinterpret_cast<sllnode<ModelAction *>*>(((uintptr_t) llnode) & ALLMASK);
+ llnode->next = llnodeprev->next;
+ llnode->prev = llnodeprev;
+ llnode->next->prev = llnode;
+ llnodeprev->next = llnode;
+ ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t) llnode) | ISACT);
+ }
+ return;
+ } else if (tmp == NULL) {
+ tmp = new allnode();
+ ptr->children[index] = tmp;
+ tmp->parent=ptr;
+ ptr->count++;
+ }
+ shiftbits -= ALLBITS;
+ ptr = tmp;
+ } while(1);
+
+}
+
+void decrementCount(allnode * ptr) {
+ ptr->count--;
+ if (ptr->count == 0) {
+ if (ptr->parent != NULL) {
+ for(uint i=0;i<ALLNODESIZE;i++) {
+ if (ptr->parent->children[i]==ptr) {
+ ptr->parent->children[i] = NULL;
+ decrementCount(ptr->parent);
+ }
+ }
+ }
+ delete ptr;
+ }
+}
+
+void actionlist::removeAction(ModelAction * act) {
+ int shiftbits = MODELCLOCKBITS - ALLBITS;
+ modelclock_t clock = act->get_seq_number();
+ allnode * ptr = &root;
+ do {
+ int index = (clock >> shiftbits) & ALLMASK;
+ allnode * tmp = ptr->children[index];
+ if (shiftbits == 0) {
+ if (tmp == NULL) {
+ //not found
+ return;
+ } else {
+ sllnode<ModelAction *> * llnode = reinterpret_cast<sllnode<ModelAction *> *>(((uintptr_t) tmp) & ALLMASK);
+ bool first = true;
+ do {
+ if (llnode->val == act) {
+ //found node to remove
+ sllnode<ModelAction *> * llnodeprev = llnode->prev;
+ sllnode<ModelAction *> * llnodenext = llnode->next;
+ if (llnodeprev != NULL) {
+ llnodeprev->next = llnodenext;
+ } else {
+ head = llnodenext;
+ }
+ if (llnodenext != NULL) {
+ llnodenext->prev = llnodeprev;
+ } else {
+ tail = llnodeprev;
+ }
+ if (first) {
+ //see if previous node has same clock as us...
+ if (llnodeprev->val->get_seq_number() == clock) {
+ ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t)llnodeprev) | ISACT);
+ } else {
+ //remove ourselves and go up tree
+ ptr->children[index] = NULL;
+ decrementCount(ptr);
+ }
+ }
+ delete llnode;
+ _size--;
+ return;
+ }
+ llnode = llnode->prev;
+ first = false;
+ } while(llnode != NULL && llnode->val->get_seq_number() == clock);
+ //node not found in list... no deletion
+ return;
+ }
+ } else if (tmp == NULL) {
+ //not found
+ return;
+ }
+ shiftbits -= ALLBITS;
+ ptr = tmp;
+ } while(1);
+}
+
+void actionlist::clear() {
+ for(uint i = 0;i < ALLNODESIZE;i++) {
+ if (root.children[i] != NULL) {
+ delete root.children[i];
+ root.children[i] = NULL;
+ }
+ }
+
+ while(head != NULL) {
+ sllnode<ModelAction *> *tmp=head->next;
+ delete head;
+ head = tmp;
+ }
+ tail=NULL;
+
+ root.count = 0;
+ _size = 0;
+}
+
+bool actionlist::isEmpty() {
+ return root.count == 0;
+}
--- /dev/null
+#ifndef ACTIONLIST_H
+#define ACTIONLIST_H
+
+#include "classlist.h"
+#include "stl-model.h"
+
+#define ISACT 1
+#define ALLBITS 4
+#define ALLNODESIZE (1 << ALLBITS)
+#define ALLMASK ((1 << ALLBITS)-1)
+#define MODELCLOCKBITS 32
+
+class allnode;
+void decrementCount(allnode *);
+
+class allnode {
+public:
+ allnode();
+ ~allnode();
+ SNAPSHOTALLOC;
+
+private:
+ allnode * parent;
+ allnode * children[ALLNODESIZE];
+ int count;
+ sllnode<ModelAction *> * findPrev(modelclock_t index);
+ friend class actionlist;
+ friend void decrementCount(allnode *);
+};
+
+class actionlist {
+public:
+ actionlist();
+ ~actionlist();
+ void addAction(ModelAction * act);
+ void removeAction(ModelAction * act);
+ void clear();
+ bool isEmpty();
+ uint size() {return _size;}
+ sllnode<ModelAction *> * begin() {return head;}
+ sllnode<ModelAction *> * end() {return tail;}
+
+ SNAPSHOTALLOC;
+
+private:
+ allnode root;
+ sllnode<ModelAction *> * head;
+ sllnode<ModelAction* > * tail;
+
+ uint _size;
+};
+#endif
class Predicate;
class ConcretePredicate;
class WaitObj;
+class actionlist;
+
+#include "actionlist.h"
struct model_snapshot_members;
struct bug_message;
-typedef SnapList<ModelAction *> action_list_t;
+typedef actionlist action_list_t;
typedef SnapList<uint32_t> func_id_list_t;
typedef SnapList<FuncInst *> func_inst_list_t;
#define FORK_HANDLER_HACK
/** Enable smart fuzzer */
-#define NEWFUZZER
+//#define NEWFUZZER
/** Define semantics of volatile memory operations. */
#define memory_order_volatile_load memory_order_acquire
read_from(curr, rf);
get_thread(curr)->set_return_value(curr->get_return_value());
delete priorset;
+ //Update acquire fence clock vector
+ ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
+ if (hbcv != NULL)
+ get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
return canprune && (curr->get_type() == ATOMIC_READ);
}
priorset->clear();
state->locked = NULL;
/* disable this thread */
- get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+ get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
scheduler->sleep(get_thread(curr));
}
* @param curr The ModelAction to process
* @return True if synchronization was updated
*/
-bool ModelExecution::process_fence(ModelAction *curr)
+void ModelExecution::process_fence(ModelAction *curr)
{
/*
* fence-relaxed: no-op
* sequences
* fence-seq-cst: MO constraints formed in {r,w}_modification_order
*/
- bool updated = false;
if (curr->is_acquire()) {
- action_list_t *list = &action_trace;
- sllnode<ModelAction *> * rit;
- /* Find X : is_read(X) && X --sb-> curr */
- for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
- ModelAction *act = rit->getVal();
- if (act == curr)
- continue;
- if (act->get_tid() != curr->get_tid())
- continue;
- /* Stop at the beginning of the thread */
- if (act->is_thread_start())
- break;
- /* Stop once we reach a prior fence-acquire */
- if (act->is_fence() && act->is_acquire())
- break;
- if (!act->is_read())
- continue;
- /* read-acquire will find its own release sequences */
- if (act->is_acquire())
- continue;
-
- /* Establish hypothetical release sequences */
- ClockVector *cv = get_hb_from_write(act->get_reads_from());
- if (cv != NULL && curr->get_cv()->merge(cv))
- updated = true;
- }
+ curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
}
- return updated;
}
/**
int tid = id_to_int(act->get_tid());
if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- act->setActionRef(list->add_back(act));
+ list->addAction(act);
}
// Update action trace, a total order of all actions
- act->setTraceRef(action_trace.add_back(act));
+ action_trace.addAction(act);
// Update obj_thrd_map, a per location, per thread, order of actions
new (&(*vec)[i]) action_list_t();
}
if (!canprune && (act->is_read() || act->is_write()))
- act->setThrdMapRef((*vec)[tid].add_back(act));
+ (*vec)[tid].addAction(act);
// Update thrd_last_action, the last action taken by each thread
if ((int)thrd_last_action.size() <= tid)
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
+ get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
}
}
-sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
- sllnode<ModelAction*> * rit = list->end();
- modelclock_t next_seq = act->get_seq_number();
- if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
- return list->add_back(act);
- else {
- for(;rit != NULL;rit=rit->getPrev()) {
- if (rit->getVal()->get_seq_number() <= next_seq) {
- return list->insertAfter(rit, act);
- }
- }
- return list->add_front(act);
- }
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+ list->addAction(act);
}
-sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
- sllnode<ModelAction*> * rit = list->end();
- modelclock_t next_seq = act->get_seq_number();
- if (rit == NULL) {
- act->create_cv(NULL);
- return list->add_back(act);
- } else if (rit->getVal()->get_seq_number() <= next_seq) {
- act->create_cv(rit->getVal());
- return list->add_back(act);
- } else {
- for(;rit != NULL;rit=rit->getPrev()) {
- if (rit->getVal()->get_seq_number() <= next_seq) {
- act->create_cv(rit->getVal());
- return list->insertAfter(rit, act);
- }
- }
- return list->add_front(act);
- }
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+ act->create_cv(NULL);
+ list->addAction(act);
}
/**
void ModelExecution::add_normal_write_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
+ insertIntoActionListAndSetCV(&action_trace, act);
// Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
+ insertIntoActionList(&(*vec)[tid],act);
ModelAction * lastact = thrd_last_action[tid];
// Update thrd_last_action, the last action taken by each thrad
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- write->setActionRef((*vec)[tid].add_back(write));
+ (*vec)[tid].addAction(write);
}
/**
int length = 25;
int counter = 0;
SnapList<ModelAction *> list;
- for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+ for (it = action_trace.end();it != NULL;it = it->getPrev()) {
if (counter > length)
break;
void ModelExecution::removeAction(ModelAction *act) {
{
- sllnode<ModelAction *> * listref = act->getTraceRef();
- if (listref != NULL) {
- action_trace.erase(listref);
- }
+ action_trace.removeAction(act);
}
{
- sllnode<ModelAction *> * listref = act->getThrdMapRef();
- if (listref != NULL) {
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
- (*vec)[act->get_tid()].erase(listref);
- }
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].removeAction(act);
}
if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
- sllnode<ModelAction *> * listref = act->getActionRef();
- if (listref != NULL) {
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->erase(listref);
- }
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->removeAction(act);
} else if (act->is_wait()) {
- sllnode<ModelAction *> * listref = act->getActionRef();
- if (listref != NULL) {
- void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
- }
+ void *mutex_loc = (void *) act->get_value();
+ get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
} else if (act->is_free()) {
- sllnode<ModelAction *> * listref = act->getActionRef();
- if (listref != NULL) {
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
- (*vec)[act->get_tid()].erase(listref);
- }
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].removeAction(act);
+
//Clear it from last_sc_map
if (obj_last_sc_map.get(act->get_location()) == act) {
obj_last_sc_map.remove(act->get_location());
#include <condition_variable>
#include "classlist.h"
-typedef SnapList<ModelAction *> action_list_t;
-
struct PendingFutureValue {
PendingFutureValue(ModelAction *writer, ModelAction *reader) :
writer(writer), reader(reader)
bool initialize_curr_action(ModelAction **curr);
bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
void process_write(ModelAction *curr);
- bool process_fence(ModelAction *curr);
+ void process_fence(ModelAction *curr);
bool process_mutex(ModelAction *curr);
void process_thread_action(ModelAction *curr);
void read_from(ModelAction *act, ModelAction *rf);
while(random_index--)
it=it->getNext();
Thread *thread = model->get_thread(it->getVal());
- waiters->erase(it);
+ waiters->removeAction(it->getVal());
return thread;
}
#include "classlist.h"
#include "snapshot-interface.h"
-typedef SnapList<ModelAction *> action_list_t;
-
/** @brief Model checker execution stats */
struct execution_stats {
int num_total; /**< @brief Total number of executions */
#include "mymemory.h"
typedef unsigned int uint;
-
template<typename _Tp>
class mllnode {
public:
uint _size;
};
+class actionlist;
+
template<typename _Tp>
class sllnode {
public:
_Tp val;
template<typename T>
friend class SnapList;
+ friend class actionlist;
};
template<typename _Tp>
array[index] = item;
}
+ void remove(type item) {
+ for(uint i = 0;i < _size;i++) {
+ if (at(i) == item) {
+ removeAt(i);
+ return;
+ }
+ }
+ }
+
void removeAt(uint index) {
for (uint i = index;(i + 1) < _size;i++) {
set(i, at(i + 1));
bool is_model_thread() const { return model_thread; }
void * get_stack_addr() { return stack; }
+ ClockVector * get_acq_fence_cv() { return acq_fence_cv; }
friend void thread_startup();
#ifdef TLS
/** @brief The parent Thread which created this Thread */
Thread * const parent;
+ /** @brief Acquire fence cv */
+ ClockVector *acq_fence_cv;
+
/** @brief The THREAD_CREATE ModelAction which created this Thread */
ModelAction *creation;
#include "model.h"
#include "execution.h"
#include "schedule.h"
+#include "clockvector.h"
#ifdef TLS
#include <dlfcn.h>
*/
Thread::Thread(thread_id_t tid) :
parent(NULL),
+ acq_fence_cv(new ClockVector()),
creation(NULL),
pending(NULL),
start_routine(NULL),
*/
Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent) :
parent(parent),
+ acq_fence_cv(new ClockVector()),
creation(NULL),
pending(NULL),
start_routine(func),
*/
Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent) :
parent(parent),
+ acq_fence_cv(new ClockVector()),
creation(NULL),
pending(NULL),
start_routine(NULL),
{
if (!is_complete())
complete();
+
+ delete acq_fence_cv;
}
/** @return The thread_id_t corresponding to this Thread object. */
projects / c11tester.git / commitdiff