From: Brian Demsky Date: Mon, 8 Oct 2012 08:21:35 +0000 (-0700) Subject: merge massive speedup with release sequence support... X-Git-Tag: pldi2013~97 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=b8b39c87557325a384faa45d0cae56a6f71f52b1;hp=59eb730e1d19a0825008c40eb521bfc5c29df5f9 merge massive speedup with release sequence support... Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker Conflicts: schedule.cc schedule.h --- diff --git a/action.cc b/action.cc index 8dba82f..c1adc2e 100644 --- a/action.cc +++ b/action.cc @@ -12,7 +12,20 @@ #define ACTION_INITIAL_CLOCK 0 -ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) : +/** + * @brief Construct a new ModelAction + * + * @param type The type of action + * @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. + */ +ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, + uint64_t value, Thread *thread) : type(type), order(order), location(loc), @@ -22,7 +35,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint seq_number(ACTION_INITIAL_CLOCK), cv(NULL) { - Thread *t = thread_current(); + Thread *t = thread ? thread : thread_current(); this->tid = t->get_id(); } @@ -52,6 +65,11 @@ void ModelAction::set_seq_number(modelclock_t num) seq_number = num; } +bool ModelAction::is_relseq_fixup() const +{ + return type == MODEL_FIXUP_RELSEQ; +} + bool ModelAction::is_mutex_op() const { return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; @@ -307,6 +325,9 @@ void ModelAction::print() const { const char *type_str, *mo_str; switch (this->type) { + case MODEL_FIXUP_RELSEQ: + type_str = "relseq fixup"; + break; case THREAD_CREATE: type_str = "thread create"; break; diff --git a/action.h b/action.h index 96ea6fa..65b060f 100644 --- a/action.h +++ b/action.h @@ -14,6 +14,7 @@ #include "modeltypes.h" class ClockVector; +class Thread; using std::memory_order; using std::memory_order_relaxed; @@ -37,6 +38,8 @@ using std::memory_order_seq_cst; /** @brief Represents an action type, identifying one of several types of * ModelAction */ typedef enum action_type { + MODEL_FIXUP_RELSEQ, /**< Special ModelAction: finalize a release + * sequence */ THREAD_CREATE, /**< A thread creation action */ THREAD_START, /**< First action in each thread */ THREAD_YIELD, /**< A thread yield action */ @@ -64,7 +67,7 @@ class ClockVector; */ class ModelAction { public: - ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); + ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL); ~ModelAction(); void print() const; @@ -82,6 +85,7 @@ public: void copy_from_new(ModelAction *newaction); void set_seq_number(modelclock_t num); void set_try_lock(bool obtainedlock); + bool is_relseq_fixup() const; bool is_mutex_op() const; bool is_lock() const; bool is_trylock() const; diff --git a/common.cc b/common.cc index e05e094..b274989 100644 --- a/common.cc +++ b/common.cc @@ -4,12 +4,17 @@ #include "common.h" #include "model.h" +#include "stacktrace.h" #define MAX_TRACE_LEN 100 +#define CONFIG_STACKTRACE /** Print a backtrace of the current program state. */ void print_trace(void) { +#ifdef CONFIG_STACKTRACE + print_stacktrace(stdout); +#else void *array[MAX_TRACE_LEN]; char **strings; int size, i; @@ -23,6 +28,7 @@ void print_trace(void) printf("\t%s\n", strings[i]); free(strings); +#endif /* CONFIG_STACKTRACE */ } void model_print_summary(void) diff --git a/model.cc b/model.cc index 2c27567..4f2719f 100644 --- a/model.cc +++ b/model.cc @@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) : priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); /* First thread created will have id INITIAL_THREAD_ID */ priv->next_thread_id = INITIAL_THREAD_ID; + + /* Initialize a model-checker thread, for special ModelActions */ + model_thread = new Thread(get_next_id()); + thread_map->put(id_to_int(model_thread->get_id()), model_thread); } /** @brief Destructor */ @@ -166,6 +170,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* The next node will try to read from a different future value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); + } else if (nextnode->increment_relseq_break()) { + /* The next node will try to resolve a release sequence differently */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); } else { /* Make a different thread execute for next step */ scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid()))); @@ -249,7 +257,7 @@ bool ModelChecker::next_execution() num_feasible_executions++; } - DEBUG("Number of acquires waiting on pending release sequences: %lu\n", + DEBUG("Number of acquires waiting on pending release sequences: %zu\n", pending_rel_seqs->size()); if (isfinalfeasible() || DBG_ENABLED()) @@ -582,6 +590,76 @@ bool ModelChecker::process_thread_action(ModelAction *curr) return updated; } +/** + * @brief Process the current action for release sequence fixup activity + * + * Performs model-checker release sequence fixups for the current action, + * forcing a single pending release sequence to break (with a given, potential + * "loose" write) or to complete (i.e., synchronize). If a pending release + * sequence forms a complete release sequence, then we must perform the fixup + * synchronization, mo_graph additions, etc. + * + * @param curr The current action; must be a release sequence fixup action + * @param work_queue The work queue to which to add work items as they are + * generated + */ +void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue) +{ + const ModelAction *write = curr->get_node()->get_relseq_break(); + struct release_seq *sequence = pending_rel_seqs->back(); + pending_rel_seqs->pop_back(); + ASSERT(sequence); + ModelAction *acquire = sequence->acquire; + const ModelAction *rf = sequence->rf; + const ModelAction *release = sequence->release; + ASSERT(acquire); + ASSERT(release); + ASSERT(rf); + ASSERT(release->same_thread(rf)); + + if (write == NULL) { + /** + * @todo Forcing a synchronization requires that we set + * modification order constraints. For instance, we can't allow + * a fixup sequence in which two separate read-acquire + * operations read from the same sequence, where the first one + * synchronizes and the other doesn't. Essentially, we can't + * allow any writes to insert themselves between 'release' and + * 'rf' + */ + + /* Must synchronize */ + if (!acquire->synchronize_with(release)) { + set_bad_synchronization(); + return; + } + /* Re-check all pending release sequences */ + work_queue->push_back(CheckRelSeqWorkEntry(NULL)); + /* Re-check act for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(acquire)); + + /* propagate synchronization to later actions */ + action_list_t::reverse_iterator rit = action_trace->rbegin(); + for (; (*rit) != acquire; rit++) { + ModelAction *propagate = *rit; + if (acquire->happens_before(propagate)) { + propagate->synchronize_with(acquire); + /* Re-check 'propagate' for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(propagate)); + } + } + } else { + /* Break release sequence with new edges: + * release --mo--> write --mo--> rf */ + mo_graph->addEdge(release, write); + mo_graph->addEdge(write, rf); + } + + /* See if we have realized a data race */ + if (checkDataRaces()) + set_assert(); +} + /** * Initialize the current action by performing one or more of the following * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward @@ -633,6 +711,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) */ if (newcurr->is_write()) compute_promises(newcurr); + else if (newcurr->is_relseq_fixup()) + compute_relseq_breakwrites(newcurr); } return newcurr; } @@ -721,6 +801,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_mutex_op() && process_mutex(act)) update_all = true; + if (act->is_relseq_fixup()) + process_relseq_fixup(curr, &work_queue); + if (update_all) work_queue.push_back(CheckRelSeqWorkEntry(NULL)); else if (update) @@ -781,7 +864,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { if ((!parnode->backtrack_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || - !currnode->promise_empty()) + !currnode->promise_empty() || + !currnode->relseq_break_empty()) && (!priv->next_backtrack || *curr > *priv->next_backtrack)) { priv->next_backtrack = curr; @@ -1299,10 +1383,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, bool future_ordered = false; ModelAction *last = get_last_action(int_to_id(i)); - if (last && (rf->happens_before(last) || - get_thread(int_to_id(i))->is_complete())) + Thread *th = get_thread(int_to_id(i)); + if ((last && rf->happens_before(last)) || + !scheduler->is_enabled(th) || + th->is_complete()) future_ordered = true; + ASSERT(!th->is_model_thread() || future_ordered); + for (rit = list->rbegin(); rit != list->rend(); rit++) { const ModelAction *act = *rit; /* Reach synchronization -> this thread is complete */ @@ -1691,6 +1779,29 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) } } +/** + * Compute the set of writes that may break the current pending release + * sequence. This information is extracted from previou release sequence + * calculations. + * + * @param curr The current ModelAction. Must be a release sequence fixup + * action. + */ +void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) +{ + if (pending_rel_seqs->empty()) + return; + + struct release_seq *pending = pending_rel_seqs->back(); + for (unsigned int i = 0; i < pending->writes.size(); i++) { + const ModelAction *write = pending->writes[i]; + curr->get_node()->add_relseq_break(write); + } + + /* NULL means don't break the sequence; just synchronize */ + curr->get_node()->add_relseq_break(NULL); +} + /** * 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" @@ -1894,7 +2005,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread *curr = thread_current(); + Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL; if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); @@ -1917,6 +2028,26 @@ bool ModelChecker::take_step() { DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, next ? id_to_int(next->get_id()) : -1); + /* + * Launch end-of-execution release sequence fixups only when there are: + * + * (1) no more user threads to run (or when execution replay chooses + * the 'model_thread') + * (2) pending release sequences + * (3) pending assertions (i.e., data races) + * (4) no pending promises + */ + if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && + isfinalfeasible() && !unrealizedraces.empty()) { + printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", + pending_rel_seqs->size()); + ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, + std::memory_order_seq_cst, NULL, VALUE_NONE, + model_thread); + set_current_action(fixup); + return true; + } + /* next == NULL -> don't take any more steps */ if (!next) return false; diff --git a/model.h b/model.h index d2baaf4..7bc3585 100644 --- a/model.h +++ b/model.h @@ -141,6 +141,7 @@ private: bool process_write(ModelAction *curr); bool process_mutex(ModelAction *curr); bool process_thread_action(ModelAction *curr); + void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue); bool check_action_enabled(ModelAction *curr); bool take_step(); @@ -153,6 +154,7 @@ private: void reset_to_initial_state(); bool resolve_promises(ModelAction *curr); void compute_promises(ModelAction *curr); + void compute_relseq_breakwrites(ModelAction *curr); void check_curr_backtracking(ModelAction * curr); void add_action_to_lists(ModelAction *act); @@ -202,6 +204,10 @@ private: * together for efficiency and maintainability. */ struct model_snapshot_members *priv; + /** A special model-checker Thread; used for associating with + * model-checker-related ModelAcitons */ + Thread *model_thread; + /** * @brief The modification order graph * diff --git a/nodestack.cc b/nodestack.cc index 76d167d..3db80e8 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -32,7 +32,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) may_read_from(), read_from_index(0), future_values(), - future_index(-1) + future_index(-1), + relseq_break_writes(), + relseq_break_index(0) { if (act) { act->set_node(this); @@ -352,6 +354,58 @@ bool Node::increment_future_value() { return false; } +/** + * Add a write ModelAction to the set of writes that may break the release + * sequence. This is used during replay exploration of pending release + * sequences. This Node must correspond to a release sequence fixup action. + * + * @param write The write that may break the release sequence. NULL means we + * allow the release sequence to synchronize. + */ +void Node::add_relseq_break(const ModelAction *write) +{ + relseq_break_writes.push_back(write); +} + +/** + * Get the write that may break the current pending release sequence, + * according to the replay / divergence pattern. + * + * @return A write that may break the release sequence. If NULL, that means + * the release sequence should not be broken. + */ +const ModelAction * Node::get_relseq_break() +{ + if (relseq_break_index < (int)relseq_break_writes.size()) + return relseq_break_writes[relseq_break_index]; + else + return NULL; +} + +/** + * Increments the index into the relseq_break_writes set to explore the next + * item. + * @return Returns false if we have explored all values. + */ +bool Node::increment_relseq_break() +{ + DBG(); + promises.clear(); + if (relseq_break_index < ((int)relseq_break_writes.size())) { + relseq_break_index++; + return (relseq_break_index < ((int)relseq_break_writes.size())); + } + return false; +} + +/** + * @return True if all writes that may break the release sequence have been + * explored + */ +bool Node::relseq_break_empty() { + return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); +} + void Node::explore(thread_id_t tid) { int i = id_to_int(tid); diff --git a/nodestack.h b/nodestack.h index 147b004..803d2b8 100644 --- a/nodestack.h +++ b/nodestack.h @@ -92,6 +92,11 @@ public: bool promise_empty(); enabled_type_t *get_enabled_array() {return enabled_array;} + void add_relseq_break(const ModelAction *write); + const ModelAction * get_relseq_break(); + bool increment_relseq_break(); + bool relseq_break_empty(); + void print(); void print_may_read_from(); @@ -117,6 +122,9 @@ private: std::vector< struct future_value, ModelAlloc > future_values; std::vector< promise_t, ModelAlloc > promises; int future_index; + + std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; + int relseq_break_index; }; typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t; diff --git a/schedule.cc b/schedule.cc index c5e58fe..ea1d582 100644 --- a/schedule.cc +++ b/schedule.cc @@ -9,7 +9,7 @@ /** Constructor */ Scheduler::Scheduler() : - is_enabled(NULL), + enabled(NULL), enabled_len(0), curr_thread_index(0), current(NULL) @@ -21,25 +21,36 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { if (threadid>=enabled_len) { enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1)); memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t)); - if (is_enabled != NULL) { - memcpy(new_enabled, is_enabled, enabled_len*sizeof(enabled_type_t)); - snapshot_free(is_enabled); + if (enabled != NULL) { + memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t)); + snapshot_free(enabled); } - is_enabled=new_enabled; + enabled=new_enabled; enabled_len=threadid+1; } - is_enabled[threadid]=enabled_status; + enabled[threadid]=enabled_status; +} + +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool Scheduler::is_enabled(Thread *t) const +{ + int id = id_to_int(t->get_id()); + return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED); } enabled_type_t Scheduler::get_enabled(Thread *t) { - return is_enabled[id_to_int(t->get_id())]; + return enabled[id_to_int(t->get_id())]; } void Scheduler::update_sleep_set(Node *n) { enabled_type_t *enabled_array=n->get_enabled_array(); for(int i=0;iget_id())); + ASSERT(!t->is_model_thread()); set_enabled(t, THREAD_ENABLED); } @@ -102,6 +114,7 @@ void Scheduler::sleep(Thread *t) */ void Scheduler::wake(Thread *t) { + ASSERT(!t->is_model_thread()); set_enabled(t, THREAD_DISABLED); t->set_state(THREAD_READY); } @@ -120,7 +133,7 @@ Thread * Scheduler::next_thread(Thread *t) int old_curr_thread = curr_thread_index; while(true) { curr_thread_index = (curr_thread_index+1) % enabled_len; - if (is_enabled[curr_thread_index]==THREAD_ENABLED) { + if (enabled[curr_thread_index]==THREAD_ENABLED) { t = model->get_thread(int_to_id(curr_thread_index)); break; } @@ -129,6 +142,9 @@ Thread * Scheduler::next_thread(Thread *t) return NULL; } } + } else if (t->is_model_thread()) { + /* model-checker threads never run */ + t = NULL; } else { curr_thread_index = id_to_int(t->get_id()); } @@ -143,6 +159,7 @@ Thread * Scheduler::next_thread(Thread *t) */ Thread * Scheduler::get_current_thread() const { + ASSERT(!current || !current->is_model_thread()); return current; } diff --git a/schedule.h b/schedule.h index 3a54e8c..7267059 100644 --- a/schedule.h +++ b/schedule.h @@ -30,15 +30,17 @@ public: Thread * next_thread(Thread *t); Thread * get_current_thread() const; void print() const; - enabled_type_t * get_enabled() { return is_enabled; }; + enabled_type_t * get_enabled() { return enabled; }; void remove_sleep(Thread *t); void add_sleep(Thread *t); enabled_type_t get_enabled(Thread *t); void update_sleep_set(Node *n); + bool is_enabled(Thread *t) const; + SNAPSHOTALLOC private: /** The list of available Threads that are not currently running */ - enabled_type_t * is_enabled; + enabled_type_t *enabled; int enabled_len; int curr_thread_index; void set_enabled(Thread *t, enabled_type_t enabled_status); diff --git a/stacktrace.h b/stacktrace.h new file mode 100644 index 0000000..01d31d2 --- /dev/null +++ b/stacktrace.h @@ -0,0 +1,86 @@ +// stacktrace.h (c) 2008, Timo Bingmann from http://idlebox.net/ +// published under the WTFPL v2.0 + +#ifndef __STACKTRACE_H__ +#define __STACKTRACE_H__ + +#include +#include +#include +#include + +/** Print a demangled stack backtrace of the caller function to FILE* out. */ +static inline void print_stacktrace(FILE *out = stderr, unsigned int max_frames = 63) +{ + fprintf(out, "stack trace:\n"); + + // storage array for stack trace address data + void* addrlist[max_frames+1]; + + // retrieve current stack addresses + int addrlen = backtrace(addrlist, sizeof(addrlist) / sizeof(void*)); + + if (addrlen == 0) { + fprintf(out, " \n"); + return; + } + + // resolve addresses into strings containing "filename(function+address)", + // this array must be free()-ed + char** symbollist = backtrace_symbols(addrlist, addrlen); + + // allocate string which will be filled with the demangled function name + size_t funcnamesize = 256; + char* funcname = (char*)malloc(funcnamesize); + + // iterate over the returned symbol lines. skip the first, it is the + // address of this function. + for (int i = 1; i < addrlen; i++) { + char *begin_name = 0, *begin_offset = 0, *end_offset = 0; + + // find parentheses and +address offset surrounding the mangled name: + // ./module(function+0x15c) [0x8048a6d] + for (char *p = symbollist[i]; *p; ++p) { + if (*p == '(') + begin_name = p; + else if (*p == '+') + begin_offset = p; + else if (*p == ')' && begin_offset) { + end_offset = p; + break; + } + } + + if (begin_name && begin_offset && end_offset && begin_name < begin_offset) { + *begin_name++ = '\0'; + *begin_offset++ = '\0'; + *end_offset = '\0'; + + // mangled name is now in [begin_name, begin_offset) and caller + // offset in [begin_offset, end_offset). now apply + // __cxa_demangle(): + + int status; + char* ret = abi::__cxa_demangle(begin_name, + funcname, &funcnamesize, &status); + if (status == 0) { + funcname = ret; // use possibly realloc()-ed string + fprintf(out, " %s : %s+%s\n", + symbollist[i], funcname, begin_offset); + } else { + // demangling failed. Output function name as a C function with + // no arguments. + fprintf(out, " %s : %s()+%s\n", + symbollist[i], begin_name, begin_offset); + } + } else { + // couldn't parse the line? print the whole line. + fprintf(out, " %s\n", symbollist[i]); + } + } + + free(funcname); + free(symbollist); +} + +#endif // __STACKTRACE_H__ diff --git a/test/double-relseq.c b/test/double-relseq.c new file mode 100644 index 0000000..5b220eb --- /dev/null +++ b/test/double-relseq.c @@ -0,0 +1,57 @@ +/* + * This test performs some relaxed, release, acquire opeations on a single + * atomic variable. It can give some rough idea of release sequence support but + * probably should be improved to give better information. + * + * This test tries to establish two release sequences, where we should always + * either establish both or establish neither. (Note that this is only true for + * a few executions of interest, where both load-acquire's read from the same + * write.) + */ + +#include + +#include "libthreads.h" +#include "librace.h" +#include "stdatomic.h" + +atomic_int x; +int var = 0; + +static void a(void *obj) +{ + store_32(&var, 1); + atomic_store_explicit(&x, 1, memory_order_release); + atomic_store_explicit(&x, 42, memory_order_relaxed); +} + +static void b(void *obj) +{ + int r = atomic_load_explicit(&x, memory_order_acquire); + printf("r = %u\n", r); + printf("load %d\n", load_32(&var)); +} + +static void c(void *obj) +{ + atomic_store_explicit(&x, 2, memory_order_relaxed); +} + +void user_main() +{ + thrd_t t1, t2, t3, t4; + + atomic_init(&x, 0); + + printf("Thread %d: creating 4 threads\n", thrd_current()); + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + thrd_create(&t3, (thrd_start_t)&b, NULL); + thrd_create(&t4, (thrd_start_t)&c, NULL); + + thrd_join(t1); + thrd_join(t2); + thrd_join(t3); + thrd_join(t4); + printf("Thread %d is finished\n", thrd_current()); +} diff --git a/test/pending-release.c b/test/pending-release.c index 37433b1..f3ae9f4 100644 --- a/test/pending-release.c +++ b/test/pending-release.c @@ -12,9 +12,11 @@ #include "stdatomic.h" atomic_int x; +int var = 0; static void a(void *obj) { + store_32(&var, 1); atomic_store_explicit(&x, *((int *)obj), memory_order_release); atomic_store_explicit(&x, *((int *)obj) + 1, memory_order_relaxed); } @@ -23,6 +25,7 @@ static void b2(void *obj) { int r = atomic_load_explicit(&x, memory_order_acquire); printf("r = %u\n", r); + store_32(&var, 3); } static void b1(void *obj) @@ -31,6 +34,7 @@ static void b1(void *obj) int i = 7; int r = atomic_load_explicit(&x, memory_order_acquire); printf("r = %u\n", r); + store_32(&var, 2); thrd_create(&t3, (thrd_start_t)&a, &i); thrd_create(&t4, (thrd_start_t)&b2, NULL); thrd_join(t3); diff --git a/test/releaseseq.c b/test/releaseseq.c index d3127f3..462a59f 100644 --- a/test/releaseseq.c +++ b/test/releaseseq.c @@ -11,9 +11,11 @@ #include "stdatomic.h" atomic_int x; +int var = 0; static void a(void *obj) { + store_32(&var, 1); atomic_store_explicit(&x, 1, memory_order_release); atomic_store_explicit(&x, 42, memory_order_relaxed); } @@ -22,6 +24,7 @@ static void b(void *obj) { int r = atomic_load_explicit(&x, memory_order_acquire); printf("r = %u\n", r); + printf("load %d\n", load_32(&var)); } static void c(void *obj) diff --git a/threads.cc b/threads.cc index ca4b28b..7f51515 100644 --- a/threads.cc +++ b/threads.cc @@ -2,6 +2,8 @@ * @brief Thread functions. */ +#include + #include "libthreads.h" #include "common.h" #include "threads.h" @@ -112,6 +114,31 @@ void Thread::complete() } } +/** + * @brief Construct a new model-checker Thread + * + * A model-checker Thread is used for accounting purposes only. It will never + * have its own stack, and it should never be inserted into the Scheduler. + * + * @param tid The thread ID to assign + */ +Thread::Thread(thread_id_t tid) : + parent(NULL), + creation(NULL), + pending(NULL), + start_routine(NULL), + arg(NULL), + stack(NULL), + user_thread(NULL), + id(tid), + state(THREAD_READY), /* Thread is always ready? */ + wait_list(), + last_action_val(0), + model_thread(true) +{ + memset(&context, 0, sizeof(context)); +} + /** * Construct a new thread. * @param t The thread identifier of the newly created thread. @@ -126,7 +153,8 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) : user_thread(t), state(THREAD_CREATED), wait_list(), - last_action_val(VALUE_NONE) + last_action_val(VALUE_NONE), + model_thread(false) { int ret; diff --git a/threads.h b/threads.h index a379494..7f005c0 100644 --- a/threads.h +++ b/threads.h @@ -35,6 +35,7 @@ class ModelAction; /** @brief A Thread is created for each user-space thread */ class Thread { public: + Thread(thread_id_t tid); Thread(thrd_t *t, void (*func)(void *), void *a); ~Thread(); void complete(); @@ -101,6 +102,8 @@ public: return ret; } + bool is_model_thread() { return model_thread; } + friend void thread_startup(); SNAPSHOTALLOC @@ -131,6 +134,9 @@ private: * @see Thread::get_return_value() */ uint64_t last_action_val; + + /** @brief Is this Thread a special model-checker thread? */ + const bool model_thread; }; Thread * thread_current();