Merge branch 'master' of /home/git/model-checker
authorBrian Demsky <bdemsky@uci.edu>
Thu, 15 Nov 2012 04:55:23 +0000 (20:55 -0800)
committerBrian Demsky <bdemsky@uci.edu>
Thu, 15 Nov 2012 04:55:23 +0000 (20:55 -0800)
19 files changed:
README [new file with mode: 0644]
common.cc
common.h
config.h
datarace.cc
datarace.h
include/librace.h
include/model-assert.h [new file with mode: 0644]
librace.cc
main.cc
model.cc
model.h
nodestack.cc
promise.cc
schedule.cc
schedule.h
snapshot-interface.cc
snapshotimp.h
test/deadlock.cc [new file with mode: 0644]

diff --git a/README b/README
new file mode 100644 (file)
index 0000000..12a02ff
--- /dev/null
+++ b/README
@@ -0,0 +1,59 @@
+****************************************
+CDSChecker Readme
+****************************************
+
+This is an evaluation-only version of CDSChecker. Please do not distribute.
+
+CDSChecker compiles as a dynamically-linked shared library by simply running
+'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
+(clang/clang++) and GCC.
+
+Test programs should use the standard C11/C++11 library headers
+(<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
+name their main routine as user_main(int, char**) rather than main(int, char**).
+We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
+
+Test programs may also use our included happens-before race detector by
+including <librace.h> and utilizing the appropriate functions
+(store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to
+from non-atomic shared memory.
+
+Test programs should be compiled against our shared library (libmodel.so) using
+the headers in the include/ directory. Then the shared library must be made
+available to the dynamic linker, using the LD_LIBRARY_PATH environment
+variable, for instance.
+
+Sample run instructions:
+
+$ make
+$ export LD_LIBRARY_PATH=.
+$ ./test/userprog.o                   # Runs simple test program
+$ ./test/userprog.o -h                # Prints help information
+Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]
+
+Options:
+-h                    Display this help message and exit
+-m                    Maximum times a thread can read from the same write
+                      while other writes exist. Default: 0
+-M                    Maximum number of future values that can be sent to
+                      the same read. Default: 0
+-s                    Maximum actions that the model checker will wait for
+                      a write from the future past the expected number of
+                      actions. Default: 100
+-S                    Future value expiration sloppiness. Default: 10
+-f                    Specify a fairness window in which actions that are
+                      enabled sufficiently many times should receive
+                      priority for execution. Default: 0
+-e                    Enabled count. Default: 1
+-b                    Upper length bound. Default: 0
+--                    Program arguments follow.
+
+
+Note that we also provide a series of benchmarks (distributed separately),
+which can be placed under the benchmarks/ directory. After building CDSChecker,
+you can build and run the benchmarks as follows:
+
+  cd benchmarks
+  make
+  ./run.sh barrier/barrier -f 10 -m 2  # runs barrier test with fairness/memory liveness
+  ./bench.sh <dir>                     # run all benchmarks twice, with timing results; all logged to <dir>
index b274989..f4aa7ec 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -2,6 +2,8 @@
 #include <stdio.h>
 #include <stdlib.h>
 
+#include <model-assert.h>
+
 #include "common.h"
 #include "model.h"
 #include "stacktrace.h"
@@ -40,3 +42,13 @@ void assert_hook(void)
 {
        printf("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__);
 }
+
+void model_assert(bool expr, const char *file, int line)
+{
+       if (!expr) {
+               printf("  [BUG] Program has hit assertion in file %s at line %d\n",
+                               file, line);
+               model->set_assert();
+               model->switch_to_master(NULL);
+       }
+}
index 50410ea..81b2672 100644 (file)
--- a/common.h
+++ b/common.h
@@ -20,6 +20,7 @@
 
 void assert_hook(void);
 
+#ifdef CONFIG_ASSERT
 #define ASSERT(expr) \
 do { \
        if (!(expr)) { \
@@ -30,6 +31,10 @@ do { \
                exit(EXIT_FAILURE); \
        } \
 } while (0)
+#else
+#define ASSERT(expr) \
+       do { } while (0)
+#endif /* CONFIG_ASSERT */
 
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
index 971ea27..891dfd7 100644 (file)
--- a/config.h
+++ b/config.h
@@ -9,6 +9,10 @@
 /*             #ifndef CONFIG_DEBUG
                #define CONFIG_DEBUG
                #endif
+
+               #ifndef CONFIG_ASSERT
+               #define CONFIG_ASSERT
+               #endif
 */
 
 /** Turn on support for dumping cyclegraphs as dot files at each
 /* Size of stack to allocate for a thread. */
 #define STACK_SIZE (1024 * 1024)
 
+/** How many shadow tables of memory to preallocate for data race detector. */
+#define SHADOWBASETABLES 4
+
+/** Enable debugging assertions (via ASSERT()) */
+#define CONFIG_ASSERT
 
 #endif
index 270e523..ac364d7 100644 (file)
@@ -5,29 +5,45 @@
 #include <cstring>
 #include "mymemory.h"
 #include "clockvector.h"
+#include "config.h"
 
 struct ShadowTable *root;
 std::vector<struct DataRace *> unrealizedraces;
+void *memory_base;
+void *memory_top;
+
 
 /** This function initialized the data race detector. */
 void initRaceDetector() {
        root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
+       memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable)*SHADOWBASETABLES, 1);
+       memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable)*SHADOWBASETABLES;
+}
+
+void * table_calloc(size_t size) {
+       if ((((char *)memory_base)+size)>memory_top) {
+               return snapshot_calloc(size, 1);
+       } else {
+               void *tmp=memory_base;
+               memory_base=((char *)memory_base)+size;
+               return tmp;
+       }
 }
 
 /** This function looks up the entry in the shadow table corresponding to a
  * given address.*/
-static uint64_t * lookupAddressEntry(void * address) {
+static uint64_t * lookupAddressEntry(const void * address) {
        struct ShadowTable *currtable=root;
 #if BIT48
        currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
        if (currtable==NULL) {
-               currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1));
+               currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
        }
 #endif
 
        struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
        if (basetable==NULL) {
-               basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1));
+               basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
        }
        return &basetable->array[((uintptr_t)address)&MASK16BIT];
 }
@@ -75,7 +91,7 @@ static void expandRecord(uint64_t * shadow) {
 }
 
 /** This function is called when we detect a data race.*/
-static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
        struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
        race->oldthread=oldthread;
        race->oldclock=oldclock;
@@ -210,7 +226,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 }
 
 /** This function does race detection on a read for an expanded record. */
-void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
        struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
        /* Check for datarace against last write. */
@@ -268,7 +284,7 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl
 }
 
 /** This function does race detection on a read. */
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
        uint64_t * shadow=lookupAddressEntry(location);
        uint64_t shadowval=*shadow;
 
index 627b8cc..2fb1a7f 100644 (file)
@@ -36,14 +36,14 @@ struct DataRace {
        bool isnewwrite;
 
        /* Address of data race. */
-       void *address;
+       const void *address;
 };
 
 #define MASK16BIT 0xffff
 
 void initRaceDetector();
 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock);
 bool checkDataRaces();
 void printRace(struct DataRace *race);
 
index 591b292..cabf066 100644 (file)
@@ -16,10 +16,10 @@ extern "C" {
        void store_32(void *addr, uint32_t val);
        void store_64(void *addr, uint64_t val);
 
-       uint8_t load_8(void *addr);
-       uint16_t load_16(void *addr);
-       uint32_t load_32(void *addr);
-       uint64_t load_64(void *addr);
+       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);
 
 #ifdef __cplusplus
 }
diff --git a/include/model-assert.h b/include/model-assert.h
new file mode 100644 (file)
index 0000000..a091e15
--- /dev/null
@@ -0,0 +1,15 @@
+#ifndef __MODEL_ASSERT_H__
+#define __MODEL_ASSERT_H__
+
+#if __cplusplus
+extern "C" {
+#endif
+
+void model_assert(bool expr, const char *file, int line);
+#define MODEL_ASSERT(expr) model_assert((expr), __FILE__, __LINE__)
+
+#if __cplusplus
+}
+#endif
+
+#endif /* __MODEL_ASSERT_H__ */
index 3c56d96..95b97aa 100644 (file)
@@ -54,7 +54,7 @@ void store_64(void *addr, uint64_t val)
        (*(uint64_t *)addr) = val;
 }
 
-uint8_t load_8(void *addr)
+uint8_t load_8(const void *addr)
 {
        DEBUG("addr = %p\n", addr);
        thread_id_t tid=thread_current()->get_id();
@@ -63,40 +63,40 @@ uint8_t load_8(void *addr)
        return *((uint8_t *)addr);
 }
 
-uint16_t load_16(void *addr)
+uint16_t load_16(const void *addr)
 {
        DEBUG("addr = %p\n", addr);
        thread_id_t tid=thread_current()->get_id();
        ClockVector * cv=model->get_cv(tid);
        raceCheckRead(tid, addr, cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
        return *((uint16_t *)addr);
 }
 
-uint32_t load_32(void *addr)
+uint32_t load_32(const void *addr)
 {
        DEBUG("addr = %p\n", addr);
        thread_id_t tid=thread_current()->get_id();
        ClockVector * cv=model->get_cv(tid);
        raceCheckRead(tid, addr, cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv);
        return *((uint32_t *)addr);
 }
 
-uint64_t load_64(void *addr)
+uint64_t load_64(const void *addr)
 {
        DEBUG("addr = %p\n", addr);
        thread_id_t tid=thread_current()->get_id();
        ClockVector * cv=model->get_cv(tid);
        raceCheckRead(tid, addr, cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+4), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+5), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+6), cv);
-       raceCheckRead(tid, (void *)(((uintptr_t)addr)+7), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+4), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+5), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+6), cv);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr)+7), cv);
        return *((uint64_t *)addr);
 }
diff --git a/main.cc b/main.cc
index 8a17a18..fb4acbe 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -20,6 +20,8 @@ static void param_defaults(struct model_params * params) {
        params->fairwindow = 0;
        params->enabledcount = 1;
        params->bound = 0;
+       params->maxfuturevalues = 0;
+       params->expireslop = 10;
 }
 
 static void print_usage(struct model_params *params) {
@@ -33,21 +35,24 @@ static void print_usage(struct model_params *params) {
 "-h                    Display this help message and exit\n"
 "-m                    Maximum times a thread can read from the same write\n"
 "                      while other writes exist. Default: %d\n"
+"-M                    Maximum number of future values that can be sent to\n"
+"                      the same read. Default: %d\n"
 "-s                    Maximum actions that the model checker will wait for\n"
 "                      a write from the future past the expected number of\n"
 "                      actions. Default: %d\n"
+"-S                    Future value expiration sloppiness. Default: %u\n"
 "-f                    Specify a fairness window in which actions that are\n"
 "                      enabled sufficiently many times should receive\n"
 "                      priority for execution. Default: %d\n"
 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
 "--                    Program arguments follow.\n\n",
-params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound);
+params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
        exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {
-       const char *shortopts = "hm:s:f:e:b:";
+       const char *shortopts = "hm:M:s:S:f:e:b:";
        int opt;
        bool error = false;
        while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
@@ -58,6 +63,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
                case 's':
                        params->maxfuturedelay = atoi(optarg);
                        break;
+               case 'S':
+                       params->expireslop = atoi(optarg);
+                       break;
                case 'f':
                        params->fairwindow = atoi(optarg);
                        break;
@@ -70,13 +78,18 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
                case 'm':
                        params->maxreads = atoi(optarg);
                        break;
+               case 'M':
+                       params->maxfuturevalues = atoi(optarg);
+                       break;
                default: /* '?' */
                        error = true;
                        break;
                }
        }
-       (*argc) -= optind;
-       (*argv) += optind;
+       (*argv)[optind - 1] = (*argv)[0];
+       (*argc) -= (optind - 1);
+       (*argv) += (optind - 1);
+       optind = 1;
 
        if (error)
                print_usage(params);
index 78907f1..922a0d6 100644 (file)
--- a/model.cc
+++ b/model.cc
 
 ModelChecker *model;
 
+/**
+ * Structure for holding small ModelChecker members that should be snapshotted
+ */
+struct model_snapshot_members {
+       ModelAction *current_action;
+       unsigned int next_thread_id;
+       modelclock_t used_sequence_numbers;
+       Thread *nextThread;
+       ModelAction *next_backtrack;
+};
+
 /** @brief Constructor */
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
@@ -101,7 +112,7 @@ thread_id_t ModelChecker::get_next_id()
 }
 
 /** @return the number of user threads created during this execution */
-unsigned int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads() const
 {
        return priv->next_thread_id;
 }
@@ -244,6 +255,27 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
        }
 }
 
+/**
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
+ *
+ * @return True if program is in a deadlock; false otherwise
+ */
+bool ModelChecker::is_deadlocked() const
+{
+       bool blocking_threads = false;
+       for (unsigned int i = 0; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               if (is_enabled(tid))
+                       return false;
+               Thread *t = get_thread(tid);
+               if (!t->is_model_thread() && t->get_pending())
+                       blocking_threads = true;
+       }
+       return blocking_threads;
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -257,6 +289,8 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
+       if (is_deadlocked())
+               printf("ERROR: DEADLOCK\n");
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
@@ -272,7 +306,7 @@ bool ModelChecker::next_execution()
                        pending_rel_seqs->size());
 
 
-       if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+       if (isfinalfeasible() || DBG_ENABLED()) {
                checkDataRaces();
                print_summary();
        }
@@ -841,6 +875,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
        return true;
 }
 
+/**
+ * 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 ModelChecker::set_current_action(ModelAction *act) {
+       priv->current_action = act;
+}
+
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
@@ -1513,7 +1557,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                ModelAction *last = get_last_action(int_to_id(i));
                Thread *th = get_thread(int_to_id(i));
                if ((last && rf->happens_before(last)) ||
-                               !scheduler->is_enabled(th) ||
+                               !is_enabled(th) ||
                                th->is_complete())
                        future_ordered = true;
 
@@ -2000,17 +2044,14 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
                        /* Don't consider more than one seq_cst write if we are a seq_cst read. */
                        if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
-                               DEBUG("Adding action to may_read_from:\n");
-                               if (DBG_ENABLED()) {
-                                       act->print();
-                                       curr->print();
-                               }
-
-                               if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
-                                       if (sleep_can_read_from(curr, act))
-                                               curr->get_node()->add_read_from(act);
-                               } else
+                               if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
+                                       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 per-thread that "happens before" curr */
@@ -2158,6 +2199,26 @@ Thread * ModelChecker::get_thread(ModelAction *act) const
        return get_thread(act->get_tid());
 }
 
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param t The Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(Thread *t) const
+{
+       return scheduler->is_enabled(t);
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param tid The ID of the Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(thread_id_t tid) const
+{
+       return scheduler->is_enabled(tid);
+}
+
 /**
  * Switch from a user-context to the "master thread" context (a.k.a. system
  * context). This switch is made with the intention of exploring a particular
diff --git a/model.h b/model.h
index 59a0759..6e7f224 100644 (file)
--- a/model.h
+++ b/model.h
@@ -23,6 +23,7 @@ class CycleGraph;
 class Promise;
 class Scheduler;
 class Thread;
+struct model_snapshot_members;
 
 /** @brief Shorthand for a list of release sequence heads */
 typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
@@ -37,22 +38,20 @@ struct model_params {
        unsigned int fairwindow;
        unsigned int enabledcount;
        unsigned int bound;
+
+       /** @brief Maximum number of future values that can be sent to the same
+        *  read */
+       int maxfuturevalues;
+
+       /** @brief Only generate a new future value/expiration pair if the
+        *  expiration time exceeds the existing one by more than the slop
+        *  value */
+       unsigned int expireslop;
 };
 
 struct PendingFutureValue {
        ModelAction *writer;
-       ModelAction * act;
-};
-
-/**
- * Structure for holding small ModelChecker members that should be snapshotted
- */
-struct model_snapshot_members {
-       ModelAction *current_action;
-       unsigned int next_thread_id;
-       modelclock_t used_sequence_numbers;
-       Thread *nextThread;
-       ModelAction *next_backtrack;
+       ModelAction *act;
 };
 
 /** @brief Records information regarding a single pending release sequence */
@@ -88,8 +87,11 @@ public:
        Thread * get_thread(thread_id_t tid) const;
        Thread * get_thread(ModelAction *act) const;
 
+       bool is_enabled(Thread *t) const;
+       bool is_enabled(thread_id_t tid) const;
+
        thread_id_t get_next_id();
-       unsigned int get_num_threads();
+       unsigned int get_num_threads() const;
        Thread * get_current_thread();
 
        int switch_to_master(ModelAction *act);
@@ -106,13 +108,13 @@ public:
        void finish_execution();
        bool isfeasibleprefix();
        void set_assert() {asserted=true;}
+       bool is_deadlocked() const;
 
        /** @brief Alert the model-checker that an incorrectly-ordered
         * synchronization was made */
        void set_bad_synchronization() { bad_synchronization = true; }
 
        const model_params params;
-       Scheduler * get_scheduler() { return scheduler;}
        Node * get_curr_node();
 
        MEMALLOC
@@ -132,13 +134,7 @@ private:
        void wake_up_sleeping_actions(ModelAction * curr);
        modelclock_t get_next_seq_num();
 
-       /**
-        * 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) { priv->current_action = act; }
+       void set_current_action(ModelAction *act);
        Thread * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
index 743cb86..b4f75e0 100644 (file)
@@ -192,26 +192,39 @@ bool Node::misc_empty() {
 
 
 /**
- * Adds a value from a weakly ordered future write to backtrack to.
+ * Adds a value from a weakly ordered future write to backtrack to. This
+ * operation may "fail" if the future value has already been run (within some
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
  * @param value is the value to backtrack to.
+ * @return True if the future value was successully added; false otherwise
  */
 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
-       int suitableindex=-1;
+       int idx = -1; /* Highest index where value is found */
        for (unsigned int i = 0; i < future_values.size(); i++) {
                if (future_values[i].value == value) {
-                       if (future_values[i].expiration>=expiration)
+                       if (expiration <= future_values[i].expiration)
                                return false;
-                       if (future_index < ((int) i)) {
-                               suitableindex=i;
-                       }
+                       idx = i;
                }
        }
-
-       if (suitableindex!=-1) {
-               future_values[suitableindex].expiration=expiration;
+       if (idx > future_index) {
+               /* Future value hasn't been explored; update expiration */
+               future_values[idx].expiration = expiration;
                return true;
+       } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+               /* Future value has been explored and is within the "sloppy" window */
+               return false;
        }
-       struct future_value newfv={value, expiration};
+
+       /* Limit the size of the future-values set */
+       if (model->params.maxfuturevalues > 0 &&
+                       (int)future_values.size() >= model->params.maxfuturevalues)
+               return false;
+
+       struct future_value newfv = {value, expiration};
        future_values.push_back(newfv);
        return true;
 }
index 68290ee..90591eb 100644 (file)
@@ -11,11 +11,10 @@ bool Promise::increment_threads(thread_id_t tid) {
                return false;
        
        synced_thread[id]=true;
-       enabled_type_t * enabled=model->get_scheduler()->get_enabled();
        unsigned int sync_size=synced_thread.size();
        int promise_tid=id_to_int(read->get_tid());
        for(unsigned int i=1;i<model->get_num_threads();i++) {
-               if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) {
+               if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && model->is_enabled(int_to_id(i))) {
                        return false;
                }
        }
@@ -23,10 +22,9 @@ bool Promise::increment_threads(thread_id_t tid) {
 }
 
 bool Promise::check_promise() {
-       enabled_type_t * enabled=model->get_scheduler()->get_enabled();
        unsigned int sync_size=synced_thread.size();
        for(unsigned int i=1;i<model->get_num_threads();i++) {
-               if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)) {
+               if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) {
                        return false;
                }
        }
index 93379c2..26217d0 100644 (file)
@@ -35,13 +35,29 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
 
 /**
  * @brief Check if a Thread is currently enabled
+ *
+ * Check if a Thread is currently enabled. "Enabled" includes both
+ * THREAD_ENABLED and THREAD_SLEEP_SET.
  * @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);
+       return is_enabled(t->get_id());
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ *
+ * Check if a Thread is currently enabled. "Enabled" includes both
+ * THREAD_ENABLED and THREAD_SLEEP_SET.
+ * @param tid The ID of the Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool Scheduler::is_enabled(thread_id_t tid) const
+{
+       int i = id_to_int(tid);
+       return (i >= enabled_len) ? false : (enabled[i] != THREAD_DISABLED);
 }
 
 enabled_type_t Scheduler::get_enabled(Thread *t) {
index 7267059..da91fdd 100644 (file)
@@ -36,6 +36,7 @@ public:
        enabled_type_t get_enabled(Thread *t);
        void update_sleep_set(Node *n);
        bool is_enabled(Thread *t) const;
+       bool is_enabled(thread_id_t tid) const;
 
        SNAPSHOTALLOC
 private:
index 47fafa5..51fe2f0 100644 (file)
@@ -3,7 +3,6 @@
 #include <iostream>
 #include <fstream>
 #include <unistd.h>
-#include <sys/types.h>
 #include <sstream>
 #include <cstring>
 #include <string>
 #include <inttypes.h>
 #include "common.h"
 
-
+/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
+ * /.../model-checker/test/userprog.o) */
 #define MYBINARYNAME "model"
 #define MYLIBRARYNAME "libmodel.so"
-#define MAPFILE_FORMAT "/proc/%d/maps"
+#define MAPFILE "/proc/self/maps"
 
 SnapshotStack * snapshotObject;
 
@@ -68,28 +68,37 @@ static void SnapshotGlobalSegments(){
        pclose(map);
 }
 #else
+
+static void get_binary_name(char *buf, size_t len)
+{
+       if (readlink("/proc/self/exe", buf, len) == -1) {
+               perror("readlink");
+               exit(EXIT_FAILURE);
+       }
+}
+
 /** The SnapshotGlobalSegments function computes the memory regions
  *     that may contain globals and then configures the snapshotting
  *     library to snapshot them.
  */
 static void SnapshotGlobalSegments(){
-       int pid = getpid();
-       char buf[9000], filename[100];
+       char buf[9000];
+       char binary_name[800];
        FILE *map;
 
-       sprintf(filename, MAPFILE_FORMAT, pid);
-       map = fopen(filename, "r");
+       map = fopen(MAPFILE, "r");
        if (!map) {
                perror("fopen");
                exit(EXIT_FAILURE);
        }
+       get_binary_name(binary_name, sizeof(binary_name));
        while (fgets(buf, sizeof(buf), map)) {
                char regionname[200] = "";
                char r, w, x, p;
                void *begin, *end;
 
                sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname);
-               if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) {
+               if (w == 'w' && (strstr(regionname, binary_name) || strstr(regionname, MYLIBRARYNAME))) {
                        size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
                        if (len != 0)
                                addMemoryRegionToSnapShot(begin, len);
index 2e4929d..b03d285 100644 (file)
@@ -9,7 +9,6 @@
 #include <inttypes.h>
 #include <fcntl.h>
 #include <sys/mman.h>
-#include <sys/types.h>
 #include <csignal>
 #define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20)) // 100mb for the shared memory
 #define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)  // 20 mb out of the above 100 mb for my stack
diff --git a/test/deadlock.cc b/test/deadlock.cc
new file mode 100644 (file)
index 0000000..3b26bec
--- /dev/null
@@ -0,0 +1,46 @@
+#include <stdio.h>
+#include <threads.h>
+#include <mutex>
+
+#include "librace.h"
+
+std::mutex *x;
+std::mutex *y;
+uint32_t shared = 0;
+
+static void a(void *obj)
+{
+       x->lock();
+       y->lock();
+       printf("shared = %u\n", load_32(&shared));
+       y->unlock();
+       x->unlock();
+}
+
+static void b(void *obj)
+{
+       y->lock();
+       x->lock();
+       store_32(&shared, 16);
+       printf("write shared = 16\n");
+       x->unlock();
+       y->unlock();
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;
+
+       x = new std::mutex();
+       y = new std::mutex();
+
+       printf("Thread %d: creating 2 threads\n", thrd_current());
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&b, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       printf("Thread %d is finished\n", thrd_current());
+
+       return 0;
+}