# Note that relative paths are relative to the directory from which doxygen is
# run.
-EXCLUDE =
+EXCLUDE = malloc.c
# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or
# directories that are symbolic links (a Unix file system feature) are excluded
USER_O=userprog.o
USER_H=libthreads.h libatomic.h
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc cyclegraph.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h cyclegraph.h hashtable.h
SHMEM_CC=snapshot.cc malloc.c mymemory.cc
SHMEM_O=snapshot.o malloc.o mymemory.o
mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib
mac: all
-docs:
+docs: *.c *.cc *.h
doxygen
$(BIN): $(USER_O) $(LIB_SO)
delete cv;
}
-bool ModelAction::is_read()
+bool ModelAction::is_read() const
{
return type == ATOMIC_READ;
}
-bool ModelAction::is_write()
+bool ModelAction::is_write() const
{
return type == ATOMIC_WRITE;
}
-bool ModelAction::is_rmw()
+bool ModelAction::is_rmw() const
{
return type == ATOMIC_RMW;
}
-bool ModelAction::is_acquire()
+bool ModelAction::is_acquire() const
{
switch (order) {
case memory_order_acquire:
}
}
-bool ModelAction::is_release()
+bool ModelAction::is_release() const
{
switch (order) {
case memory_order_release:
}
}
-bool ModelAction::is_seqcst()
+bool ModelAction::is_seqcst() const
{
return order==memory_order_seq_cst;
}
-bool ModelAction::same_var(ModelAction *act)
+bool ModelAction::same_var(const ModelAction *act) const
{
return location == act->location;
}
-bool ModelAction::same_thread(ModelAction *act)
+bool ModelAction::same_thread(const ModelAction *act) const
{
return tid == act->tid;
}
* @return tells whether we have to explore a reordering.
*/
-bool ModelAction::is_synchronizing(ModelAction *act)
+bool ModelAction::is_synchronizing(const ModelAction *act) const
{
//Same thread can't be reordered
if (same_thread(act))
void ModelAction::create_cv(ModelAction *parent)
{
- if (cv)
- return;
+ ASSERT(cv == NULL);
if (parent)
cv = new ClockVector(parent->cv, this);
value = act->value;
}
+/**
+ * Check whether 'this' happens before act, according to the memory-model's
+ * happens before relation. This is checked via the ClockVector constructs.
+ * @return true if this action's thread has synchronized with act's thread
+ * since the execution of act, false otherwise.
+ */
+bool ModelAction::happens_before(ModelAction *act)
+{
+ return act->cv->synchronized_since(this);
+}
+
void ModelAction::print(void)
{
const char *type_str;
~ModelAction();
void print(void);
- thread_id_t get_tid() { return tid; }
- action_type get_type() { return type; }
- memory_order get_mo() { return order; }
- void * get_location() { return location; }
+ thread_id_t get_tid() const { return tid; }
+ action_type get_type() const { return type; }
+ memory_order get_mo() const { return order; }
+ void * get_location() const { return location; }
int get_seq_number() const { return seq_number; }
- Node * get_node() { return node; }
+ Node * get_node() const { return node; }
void set_node(Node *n) { node = n; }
- bool is_read();
- bool is_write();
- bool is_rmw();
- bool is_acquire();
- bool is_release();
- bool is_seqcst();
- bool same_var(ModelAction *act);
- bool same_thread(ModelAction *act);
- bool is_synchronizing(ModelAction *act);
+ bool is_read() const;
+ bool is_write() const;
+ bool is_rmw() const;
+ bool is_acquire() const;
+ bool is_release() const;
+ bool is_seqcst() const;
+ bool same_var(const ModelAction *act) const;
+ bool same_thread(const ModelAction *act) const;
+ bool is_synchronizing(const ModelAction *act) const;
void create_cv(ModelAction *parent = NULL);
+ ClockVector * get_cv() const { return cv; }
void read_from(ModelAction *act);
+ bool happens_before(ModelAction *act);
+
inline bool operator <(const ModelAction& act) const {
return get_seq_number() < act.get_seq_number();
}
clock = clk;
}
-bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+/**
+ *
+ * @return true if this ClockVector's thread has synchronized with act's
+ * thread, false otherwise. That is, this function returns:
+ * <BR><CODE>act <= cv[act->tid]</CODE>
+ */
+bool ClockVector::synchronized_since(ModelAction *act)
{
- int i = id_to_int(id);
+ int i = id_to_int(act->get_tid());
if (i < num_threads)
- return act->get_seq_number() < clock[i];
+ return act->get_seq_number() <= clock[i];
return false;
}
ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
~ClockVector();
void merge(ClockVector *cv);
- bool happens_before(ModelAction *act, thread_id_t id);
+ bool synchronized_since(ModelAction *act);
void print();
--- /dev/null
+#include "cyclegraph.h"
+
+CycleGraph::CycleGraph() {
+ hasCycles=false;
+}
+
+CycleNode * CycleGraph::getNode(ModelAction * action) {
+ CycleNode *node=actionToNode.get(action);
+ if (node==NULL) {
+ node=new CycleNode(action);
+ actionToNode.put(action, node);
+ }
+ return node;
+}
+
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to) {
+ CycleNode *fromnode=getNode(from);
+ CycleNode *tonode=getNode(to);
+ if (!hasCycles) {
+ // Check for Cycles
+ hasCycles=checkReachable(fromnode, tonode);
+ }
+ fromnode->addEdge(tonode);
+}
+
+bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
+ std::vector<class CycleNode *> queue;
+ HashTable<class CycleNode *, class CycleNode *, uintptr_t, 4> discovered;
+
+ queue.push_back(from);
+ discovered.put(from, from);
+ while(!queue.empty()) {
+ class CycleNode * node=queue.back();
+ queue.pop_back();
+ if (node==to)
+ return true;
+
+ for(unsigned int i=0;i<node->getEdges()->size();i++) {
+ CycleNode *next=(*node->getEdges())[i];
+ if (!discovered.contains(next)) {
+ discovered.put(next,next);
+ queue.push_back(next);
+ }
+ }
+ }
+ return false;
+}
+
+CycleNode::CycleNode(ModelAction *modelaction) {
+ action=modelaction;
+}
+
+std::vector<class CycleNode *> * CycleNode::getEdges() {
+ return &edges;
+}
+
+void CycleNode::addEdge(CycleNode * node) {
+ edges.push_back(node);
+}
--- /dev/null
+#ifndef CYCLEGRAPH_H
+#define CYCLEGRAPH_H
+
+#include "hashtable.h"
+#include "action.h"
+#include <vector>
+#include <inttypes.h>
+
+class CycleNode;
+
+/** @brief A graph of Model Actions for tracking cycles. */
+class CycleGraph {
+ public:
+ CycleGraph();
+ void addEdge(ModelAction *from, ModelAction *to);
+ bool checkForCycles();
+
+ private:
+ CycleNode * getNode(ModelAction *);
+ HashTable<class ModelAction *, class CycleNode *, uintptr_t, 4> actionToNode;
+ bool checkReachable(CycleNode *from, CycleNode *to);
+
+ bool hasCycles;
+
+};
+
+class CycleNode {
+ public:
+ CycleNode(ModelAction *action);
+ void addEdge(CycleNode * node);
+ std::vector<class CycleNode *> * getEdges();
+
+ private:
+ ModelAction *action;
+ std::vector<class CycleNode *> edges;
+};
+
+#endif
--- /dev/null
+#ifndef HASHTABLE_H
+#define HASHTABLE_H
+
+#include <stdlib.h>
+#include <stdio.h>
+
+template<typename _Key, typename _Val>
+ struct hashlistnode {
+ _Key key;
+ _Val val;
+ struct hashlistnode<_Key,_Val> *next;
+ };
+
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
+ class HashTable {
+ public:
+ HashTable(unsigned int initialcapacity=1024, double factor=0.5) {
+ // Allocate space for the hash table
+ table = (struct hashlistnode<_Key,_Val> **) calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val> *));
+ loadfactor = factor;
+ capacity = initialcapacity;
+ threshold = initialcapacity*loadfactor;
+ mask = (capacity << _Shift)-1;
+ size = 0; // Initial number of elements in the hash
+ }
+
+ ~HashTable() {
+ for(unsigned int i=0;i<capacity;i++) {
+ struct hashlistnode<_Key,_Val> * bin = table[i];
+ while(bin!=NULL) {
+ struct hashlistnode<_Key,_Val> * next=bin->next;
+ free(bin);
+ bin=next;
+ }
+ }
+ free(table);
+ }
+
+ void reset() {
+ for(int i=0;i<capacity;i++) {
+ struct hashlistnode<_Key,_Val> * bin = table[i];
+ while(bin!=NULL) {
+ struct hashlistnode<_Key,_Val> * next=bin->next;
+ free(bin);
+ bin=next;
+ }
+ }
+ memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val> *));
+ size=0;
+ }
+
+ void put(_Key key, _Val val) {
+ if(size > threshold) {
+ //Resize
+ unsigned int newsize = capacity << 1;
+ resize(newsize);
+ }
+
+ struct hashlistnode<_Key,_Val> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
+ size++;
+ struct hashlistnode<_Key,_Val> *search = ptr;
+
+ while(search!=NULL) {
+ if (search->key==key) {
+ search->val=val;
+ return;
+ }
+ search=search->next;
+ }
+
+ struct hashlistnode<_Key,_Val> *newptr=(struct hashlistnode<_Key,_Val> *)malloc(sizeof(struct hashlistnode<_Key,_Val>));
+ newptr->key=key;
+ newptr->val=val;
+ newptr->next=ptr;
+ table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+ }
+
+ _Val get(_Key key) {
+ struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+
+ while(search!=NULL) {
+ if (search->key==key) {
+ return search->val;
+ }
+ search=search->next;
+ }
+ return (_Val)0;
+ }
+
+ bool contains(_Key key) {
+ struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+
+ while(search!=NULL) {
+ if (search->key==key) {
+ return true;
+ }
+ search=search->next;
+ }
+ return false;
+ }
+
+ void resize(unsigned int newsize) {
+ struct hashlistnode<_Key,_Val> ** oldtable = table;
+ struct hashlistnode<_Key,_Val> ** newtable;
+ unsigned int oldcapacity = capacity;
+
+ if((newtable = (struct hashlistnode<_Key,_Val> **) calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) {
+ printf("Calloc error %s %d\n", __FILE__, __LINE__);
+ exit(-1);
+ }
+
+ table = newtable; //Update the global hashtable upon resize()
+ capacity = newsize;
+ threshold = newsize * loadfactor;
+ mask = (newsize << _Shift)-1;
+
+ for(unsigned int i = 0; i < oldcapacity; i++) {
+ struct hashlistnode<_Key, _Val> * bin = oldtable[i];
+
+ while(bin!=NULL) {
+ _Key key=bin->key;
+ struct hashlistnode<_Key, _Val> * next=bin->next;
+
+ unsigned int index = (((_KeyInt)key) & mask) >>_Shift;
+ struct hashlistnode<_Key, _Val> * tmp=newtable[index];
+ bin->next=tmp;
+ newtable[index]=bin;
+ bin = next;
+ }
+ }
+
+ free(oldtable); //Free the memory of the old hash table
+ }
+
+ private:
+ struct hashlistnode<_Key,_Val> **table;
+ unsigned int capacity;
+ _KeyInt mask;
+ unsigned int size;
+ unsigned int threshold;
+ double loadfactor;
+};
+#endif
#include "schedule.h"
#include "snapshot-interface.h"
#include "common.h"
+#include "clockvector.h"
#define INITIAL_THREAD_ID 0
ModelChecker *model;
+/** @brief Constructor */
ModelChecker::ModelChecker()
:
/* Initialize default scheduler */
{
}
+/** @brief Destructor */
ModelChecker::~ModelChecker()
{
std::map<int, class Thread *>::iterator it;
delete scheduler;
}
+/**
+ * Restores user program to initial state and resets all model-checker data
+ * structures.
+ */
void ModelChecker::reset_to_initial_state()
{
DEBUG("+++ Resetting to initial state +++\n");
snapshotObject->backTrackBeforeStep(0);
}
+/** @returns a thread ID for a new Thread */
thread_id_t ModelChecker::get_next_id()
{
return next_thread_id++;
}
+/** @returns the number of user threads created during this execution */
int ModelChecker::get_num_threads()
{
return next_thread_id;
}
+/** @returns a sequence number for a new ModelAction */
int ModelChecker::get_next_seq_num()
{
return ++used_sequence_numbers;
}
+/**
+ * Performs the "scheduling" for the model-checker. That is, it checks if the
+ * model-checker has selected a "next thread to run" and returns it, if
+ * available. This function should be called from the Scheduler routine, where
+ * the Scheduler falls back to a default scheduling routine if needed.
+ *
+ * @return The next thread chosen by the model-checker. If the model-checker
+ * makes no selection, retuns NULL.
+ */
Thread * ModelChecker::schedule_next_thread()
{
Thread *t;
}
/**
- * get_next_replay_thread() - Choose the next thread in the replay sequence
+ * Choose the next thread in the replay sequence.
*
- * If we've reached the 'diverge' point, then we pick a thread from the
- * backtracking set.
- * Otherwise, we simply return the next thread in the sequence.
+ * If the replay sequence has reached the 'diverge' point, returns a thread
+ * from the backtracking set. Otherwise, simply returns the next thread in the
+ * sequence that is being replayed.
*/
thread_id_t ModelChecker::get_next_replay_thread()
{
return tid;
}
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
bool ModelChecker::next_execution()
{
DBG();
Node *currnode;
ModelAction *curr = this->current_action;
+ ModelAction *tmp;
current_action = NULL;
if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
- curr = node_stack->explore_action(curr);
- curr->create_cv(get_parent_action(curr->get_tid()));
+ tmp = node_stack->explore_action(curr);
+ if (tmp) {
+ /* Discard duplicate ModelAction; use action from NodeStack */
+ delete curr;
+ curr = tmp;
+ } else {
+ /*
+ * Perform one-time actions when pushing new ModelAction onto
+ * NodeStack
+ */
+ curr->create_cv(get_parent_action(curr->get_tid()));
+ /* Build may_read_from set */
+ if (curr->is_read())
+ build_reads_from_past(curr);
+ }
/* Assign 'creation' parent */
if (curr->get_type() == THREAD_CREATE) {
add_action_to_lists(curr);
}
+
+/**
+ * Adds an action to the per-object, per-thread action vector.
+ * @param act is the ModelAction to add.
+ */
+
void ModelChecker::add_action_to_lists(ModelAction *act)
{
action_trace->push_back(act);
return parent;
}
+/**
+ * Build up an initial set of all past writes that this 'read' action may read
+ * from. This set is determined by the clock vector's "happens before"
+ * relationship.
+ * @param curr is the current ModelAction that we are exploring; it must be a
+ * 'read' operation.
+ */
+void ModelChecker::build_reads_from_past(ModelAction *curr)
+{
+ std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+ unsigned int i;
+
+ ASSERT(curr->is_read());
+
+ for (i = 0; i < thrd_lists->size(); i++) {
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ /* Only consider 'write' actions */
+ if (!act->is_write())
+ continue;
+
+ DEBUG("Adding action to may_read_from:\n");
+ if (DBG_ENABLED()) {
+ act->print();
+ curr->print();
+ }
+ curr->get_node()->add_read_from(act);
+
+ /* Include at most one act that "happens before" curr */
+ if (act->happens_before(curr))
+ break;
+ }
+ }
+}
+
void ModelChecker::print_summary(void)
{
printf("\n");
/* Forward declaration */
class NodeStack;
+/** @brief The central structure for model-checking */
class ModelChecker {
public:
ModelChecker();
~ModelChecker();
+
+ /** The scheduler to use: tracks the running/ready Threads */
class Scheduler *scheduler;
+ /** Stores the context for the main model-checking system thread (call
+ * once)
+ * @param ctxt The system context structure
+ */
void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
+
+ /** @returns the context for the main model-checking system thread */
ucontext_t * get_system_context(void) { return system_context; }
+ /**
+ * Stores the ModelAction for the current thread action. Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
void set_current_action(ModelAction *act) { current_action = act; }
void check_current_action(void);
void print_summary(void);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
ModelAction * get_parent_action(thread_id_t tid);
+ void build_reads_from_past(ModelAction *curr);
void print_list(action_list_t *list);
void system_free( void * ptr );
void *system_malloc( size_t size );
-/** @brief Provides a non-snapshotting allocators for a STL class.
+/** @brief Provides a non-snapshotting allocator for use in STL classes.
*
* The code was adapted from a code example from the book The C++
* Standard Library - A Tutorial and Reference by Nicolai M. Josuttis,
#include "common.h"
#include "model.h"
+/** @brief Node constructor */
Node::Node(ModelAction *act, int nthreads)
: action(act),
num_threads(nthreads),
explored_children(num_threads),
- backtrack(num_threads)
+ backtrack(num_threads),
+ numBacktracks(0),
+ may_read_from()
{
}
+/** @brief Node desctructor */
Node::~Node()
{
if (action)
delete action;
}
+/** Prints debugging info for the ModelAction associated with this Node */
void Node::print()
{
if (action)
printf("******** empty action ********\n");
}
+/**
+ * Checks if the Thread associated with this thread ID has been explored from
+ * this Node already.
+ * @param tid is the thread ID to check
+ * @return true if this thread choice has been explored already, false
+ * otherwise
+ */
bool Node::has_been_explored(thread_id_t tid)
{
int id = id_to_int(tid);
return explored_children[id];
}
+/**
+ * Checks if the backtracking set is empty.
+ * @return true if the backtracking set is empty
+ */
bool Node::backtrack_empty()
{
- unsigned int i;
- for (i = 0; i < backtrack.size(); i++)
- if (backtrack[i] == true)
- return false;
- return true;
+ return numBacktracks == 0;
}
+/**
+ * Explore a child Node using a given ModelAction. This updates both the
+ * Node-internal and the ModelAction data to associate the ModelAction with
+ * this Node.
+ * @param act is the ModelAction to explore
+ */
void Node::explore_child(ModelAction *act)
{
act->set_node(this);
explore(act->get_tid());
}
+/**
+ * Records a backtracking reference for a thread choice within this Node.
+ * Provides feedback as to whether this thread choice is already set for
+ * backtracking.
+ * @return false if the thread was already set to be backtracked, true
+ * otherwise
+ */
bool Node::set_backtrack(thread_id_t id)
{
int i = id_to_int(id);
if (backtrack[i])
return false;
backtrack[i] = true;
+ numBacktracks++;
return true;
}
if (i >= backtrack.size())
return THREAD_ID_T_NONE;
backtrack[i] = false;
+ numBacktracks--;
return int_to_id(i);
}
return id_to_int(t->get_id()) < num_threads;
}
+/**
+ * Add an action to the may_read_from set.
+ * @param act is the action to add
+ */
+void Node::add_read_from(ModelAction *act)
+{
+ may_read_from.insert(act);
+}
+
void Node::explore(thread_id_t tid)
{
int i = id_to_int(tid);
- backtrack[i] = false;
+ if (backtrack[i]) {
+ backtrack[i] = false;
+ numBacktracks--;
+ }
explored_children[i] = true;
}
ASSERT(!node_list.empty());
if (get_head()->has_been_explored(act->get_tid())) {
- /* Discard duplicate ModelAction */
- delete act;
- iter++;
- } else { /* Diverging from previous execution */
- /* Clear out remainder of list */
- node_list_t::iterator it = iter;
- it++;
- clear_node_list(&node_list, it, node_list.end());
-
- /* Record action */
- get_head()->explore_child(act);
- node_list.push_back(new Node(act, model->get_num_threads()));
- total_nodes++;
iter++;
+ return (*iter)->get_action();
}
- return (*iter)->get_action();
+
+ /* Diverging from previous execution; clear out remainder of list */
+ node_list_t::iterator it = iter;
+ it++;
+ clear_node_list(&node_list, it, node_list.end());
+
+ /* Record action */
+ get_head()->explore_child(act);
+ node_list.push_back(new Node(act, model->get_num_threads()));
+ total_nodes++;
+ iter++;
+ return NULL;
}
Node * NodeStack::get_head()
#include <list>
#include <vector>
+#include <set>
#include <cstddef>
#include "threads.h"
#include "mymemory.h"
class ModelAction;
+typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t;
+
class Node {
public:
Node(ModelAction *act = NULL, int nthreads = 1);
bool is_enabled(Thread *t);
ModelAction * get_action() { return action; }
+ void add_read_from(ModelAction *act);
+
void print();
MEMALLOC
int num_threads;
std::vector< bool, MyAlloc<bool> > explored_children;
std::vector< bool, MyAlloc<bool> > backtrack;
+ int numBacktracks;
+
+ /** The set of ModelActions that this the action at this Node may read
+ * from. Only meaningful if this Node represents a 'read' action. */
+ action_set_t may_read_from;
};
typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
/* Forward declaration */
class Thread;
-/** @brief The Scheduler class controls the Thread execution schedule. */
+/** @brief The Scheduler class performs the mechanics of Thread execution
+ * scheduling. */
class Scheduler {
public:
Scheduler();
createSharedLibrary();
//step 2 setup the stack context.
-
- int alreadySwapped = 0;
- getcontext( &savedSnapshotContext );
- if( !alreadySwapped ){
- alreadySwapped = 1;
- ucontext_t currentContext, swappedContext, newContext;
- getcontext( &newContext );
- newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
- newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
- newContext.uc_link = ¤tContext;
- makecontext( &newContext, entryPoint, 0 );
- swapcontext( &swappedContext, &newContext );
- }
+ ucontext_t newContext;
+ getcontext( &newContext );
+ newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
+ newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
+ makecontext( &newContext, entryPoint, 0 );
+ /* switch to a new entryPoint context, on a new stack */
+ swapcontext(&savedSnapshotContext, &newContext);
//add the code to take a snapshot here...
//to return to user process, do a second swapcontext...
class ModelAction;
+/** @brief A Thread is created for each user-space thread */
class Thread {
public:
Thread(thrd_t *t, void (*func)(void *), void *a);
projects / model-checker.git / commitdiff