Adds back the necessary bugfix from previous commit "01f8364" that were accidentally... ppopp17-artifact
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 24 Oct 2017 01:48:09 +0000 (18:48 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 24 Oct 2017 01:48:09 +0000 (18:48 -0700)
18 files changed:
.gitignore
common.h
execution.cc
execution.h
impatomic.cc
include/cdsannotate.h
include/impatomic.h
main.cc
model.cc
model.h
mymemory.cc
mymemory.h
nodestack.cc
nodestack.h
spec-analysis/cdsspec.h
test-cdsspec/run-all.sh
threads.cc
traceanalysis.h

index 8df986236c0ce4c60c181b23194f9db1b1d879f3..2d24b556c8016a6296495a344827eeaca2aea5a2 100644 (file)
@@ -13,3 +13,5 @@
 /doc/docs
 /benchmarks
 /README.html
+/cdsspec-compiler/classes
+/cdsspec-compiler/src/edu/uci/eecs/utilParser
index 62c16f45250e55a693864fd17759b9673d0220d6..7be72d72f8e0b56fc8f333ffe25489685b053f60 100644 (file)
--- a/common.h
+++ b/common.h
@@ -9,8 +9,9 @@
 #include "config.h"
 
 extern int model_out;
+extern int switch_alloc;
 
-#define model_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+#define model_print(fmt, ...) do { switch_alloc = 1; dprintf(model_out, fmt, ##__VA_ARGS__); switch_alloc = 0; } while (0)
 
 #ifdef CONFIG_DEBUG
 #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
index eaf245dd17216169f5fd2cb9818b37a76ba6ea4f..2a7e0dadd1e0918ac21b5f43dd4e3608935b8f18 100644 (file)
@@ -34,6 +34,7 @@ struct model_snapshot_members {
                too_many_reads(false),
                no_valid_reads(false),
                bad_synchronization(false),
+               bad_sc_read(false),
                asserted(false)
        { }
 
@@ -53,6 +54,7 @@ struct model_snapshot_members {
        bool no_valid_reads;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
+       bool bad_sc_read;
        bool asserted;
 
        SNAPSHOTALLOC
@@ -202,6 +204,13 @@ void ModelExecution::set_bad_synchronization()
        priv->bad_synchronization = true;
 }
 
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelExecution::set_bad_sc_read()
+{
+       priv->bad_sc_read = true;
+}
+
 bool ModelExecution::assert_bug(const char *msg)
 {
        priv->bugs.push_back(new bug_message(msg));
@@ -1306,6 +1315,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                                if (rf) {
                                        if (r_modification_order(act, rf))
                                                updated = true;
+                                       if (act->is_seqcst()) {
+                                               ModelAction *last_sc_write = get_last_seq_cst_write(act);
+                                               if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
+                                                       set_bad_sc_read();
+                                               }
+                                       }
                                } else if (promise) {
                                        if (r_modification_order(act, promise))
                                                updated = true;
@@ -1385,6 +1400,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const
                ptr += sprintf(ptr, "[no valid reads-from]");
        if (priv->bad_synchronization)
                ptr += sprintf(ptr, "[bad sw ordering]");
+       if (priv->bad_sc_read)
+               ptr += sprintf(ptr, "[bad sc read]");
        if (promises_expired())
                ptr += sprintf(ptr, "[promise expired]");
        if (promises.size() != 0)
@@ -1415,6 +1432,7 @@ bool ModelExecution::is_infeasible() const
                priv->no_valid_reads ||
                priv->too_many_reads ||
                priv->bad_synchronization ||
+               priv->bad_sc_read ||
                priv->hard_failed_promise ||
                promises_expired();
 }
@@ -1583,9 +1601,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
-                       // FIXME: The read from promise might read from an annotation
-                       if (act->get_type() == ATOMIC_ANNOTATION)
-                               continue;
 
                        /* Skip curr */
                        if (act == curr)
@@ -1619,12 +1634,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                                }
                        }
 
-                       /* C++, Section 29.3 statement 3 (second subpoint) */
-                       if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
-                               added = mo_graph->addEdge(act, rf) || added;
-                               break;
-                       }
-
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr
@@ -1756,9 +1765,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
                                        added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       if (act->get_reads_from() == NULL)
-                                               continue;
-                                       added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+                                       if (act->get_reads_from() == NULL) {
+                                               added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added;
+                                       } else
+                                               added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&
index fd117abf3970c8f6e3aa49e0a08ccc7120be520d..8c8031cff2b57719ad4dfece502b96cdbed97c0c 100644 (file)
@@ -117,7 +117,7 @@ public:
        action_list_t * get_action_trace() { return &action_trace; }
 
        CycleGraph * const get_mo_graph() { return mo_graph; }
-       
+
        int get_execution_number() const;
 
        SNAPSHOTALLOC
@@ -134,6 +134,7 @@ private:
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
        bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        void set_bad_synchronization();
+       void set_bad_sc_read();
        bool promises_expired() const;
        bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
        void wake_up_sleeping_actions(ModelAction *curr);
index 2d48989c147d051bd61d3a4d01fe0e2ba1bcf9ea..4b5d1c28941246fe1c0a1e2dc1567e4bac22a81e 100644 (file)
@@ -26,11 +26,15 @@ void atomic_flag_clear_explicit
 void atomic_flag_clear( volatile atomic_flag* __a__ )
 { atomic_flag_clear_explicit( __a__, memory_order_seq_cst ); }
 
-void __atomic_flag_wait__( volatile atomic_flag* __a__ )
-{ while ( atomic_flag_test_and_set( __a__ ) ); }
+void __atomic_flag_wait__( volatile atomic_flag* __a__ ) { 
+       while ( atomic_flag_test_and_set( __a__ ) )
+               ; 
+}
 
 void __atomic_flag_wait_explicit__( volatile atomic_flag* __a__,
-                                    memory_order __x__ )
-{ while ( atomic_flag_test_and_set_explicit( __a__, __x__ ) ); }
+                                    memory_order __x__ ) {
+       while ( atomic_flag_test_and_set_explicit( __a__, __x__ ))
+               ;
+}
 
 }
index b58486d676454f10ced09add01e206f54c82a419..bb6e3d6e469c4b04b24015573bbca836d387b44c 100644 (file)
@@ -2,13 +2,6 @@
 #define CDS_ANNOTATE_H
 #include <stdint.h>
 
-//#ifdef __cplusplus
-//extern "C" {
-//#endif
 void cdsannotate(uint64_t analysistype, void *annotation);
-//#ifdef __cplusplus
-//}
-//#endif
-
 
 #endif
index 1b9ce6be97f9efdb23debaaa87c820406a65ccf2..b4273eee4a5984ce47c3b0ae922700fcad1f9e11 100644 (file)
@@ -2330,23 +2330,28 @@ inline bool atomic_compare_exchange_strong
 inline void* atomic_fetch_add_explicit
 ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
 {
-       void* volatile* __p__ = &((__a__)->__f__);
-       void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
-       model_rmw_action((void *)__p__, __x__, (uint64_t) ((char*)(*__p__) + __m__));
-  return __r__; }
+       volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);
+       __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__);
+       __typeof__((__a__)->__f__) __copy__= __old__;
+       __copy__ = (void *) (((char *)__copy__) + __m__);
+       model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);
+       return __old__;
+}
 
-inline void* atomic_fetch_add
+ inline void* atomic_fetch_add
 ( volatile atomic_address* __a__, ptrdiff_t __m__ )
 { return atomic_fetch_add_explicit( __a__, __m__, memory_order_seq_cst ); }
 
 
 inline void* atomic_fetch_sub_explicit
 ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
-{
-       void* volatile* __p__ = &((__a__)->__f__);
-       void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
-       model_rmw_action((void *)__p__, __x__, (uint64_t)((char*)(*__p__) - __m__));
-  return __r__; }
+{      volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);
+       __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__);
+       __typeof__((__a__)->__f__) __copy__= __old__;
+       __copy__ = (void *) (((char *)__copy__) - __m__);
+       model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);
+       return __old__;
+}
 
 inline void* atomic_fetch_sub
 ( volatile atomic_address* __a__, ptrdiff_t __m__ )
diff --git a/main.cc b/main.cc
index 127ffd160ff8df930d30500b1944ec2a9b107b00..502f499eff9cb2de956256bb6f24b84080e600e0 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -141,9 +141,9 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                {"enabled", required_argument, NULL, 'e'},
                {"bound", required_argument, NULL, 'b'},
                {"verbose", optional_argument, NULL, 'v'},
-               {"uninitialized", optional_argument, NULL, 'u'},
-               {"analysis", optional_argument, NULL, 't'},
-               {"options", optional_argument, NULL, 'o'},
+               {"uninitialized", required_argument, NULL, 'u'},
+               {"analysis", required_argument, NULL, 't'},
+               {"options", required_argument, NULL, 'o'},
                {"maxexecutions", required_argument, NULL, 'x'},
                {0, 0, 0, 0} /* Terminator */
        };
@@ -231,6 +231,8 @@ static void install_trace_analyses(ModelExecution *execution)
                TraceAnalysis * ta=(*installedanalysis)[i];
                ta->setExecution(execution);
                model->add_trace_analysis(ta);
+               /** Call the installation event for each installed plugin */
+               ta->actionAtInstallation();
        }
 }
 
@@ -268,6 +270,18 @@ int main(int argc, char **argv)
        main_argc = argc;
        main_argv = argv;
 
+       /*
+        * If this printf statement is removed, CDSChecker will fail on an
+        * assert on some versions of glibc.  The first time printf is
+        * called, it allocated internal buffers.  We can't easily snapshot
+        * libc since we also use it.
+        */
+
+       printf("CDSChecker\n"
+                                "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+                                "Distributed under the GPLv2\n"
+                                "Written by Brian Norris and Brian Demsky\n\n");
+
        /* Configure output redirection for the model-checker */
        redirect_output();
 
index 8f0efcddd5e8f3ccfa027a7554f6a3d437c51f72..3bac9039b4822475bb0226adcf4fd85cc8008ea1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2,6 +2,7 @@
 #include <algorithm>
 #include <new>
 #include <stdarg.h>
+#include <string.h>
 
 #include "model.h"
 #include "action.h"
@@ -22,14 +23,18 @@ ModelChecker *model;
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
        params(params),
+       restart_flag(false),
+       exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
        execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),
-       trace_analyses()
+       trace_analyses(),
+       inspect_plugin(NULL)
 {
+       memset(&stats,0,sizeof(struct execution_stats));
 }
 
 /** @brief Destructor */
@@ -298,6 +303,9 @@ bool ModelChecker::next_execution()
 
                checkDataRaces();
                run_trace_analyses();
+       } else if (inspect_plugin && !execution->is_complete_execution() &&
+               (execution->too_many_steps())) {
+                inspect_plugin->analyze(execution->get_action_trace());
        }
 
        record_stats();
@@ -311,6 +319,14 @@ bool ModelChecker::next_execution()
        if (complete)
                earliest_diverge = NULL;
 
+       if (restart_flag) {
+               do_restart();
+               return true;
+       }
+
+       if (exit_flag)
+               return false;
+
        if ((diverge = execution->get_next_backtrack()) == NULL)
                return false;
 
@@ -330,10 +346,8 @@ bool ModelChecker::next_execution()
 
 /** @brief Run trace analyses on complete trace */
 void ModelChecker::run_trace_analyses() {
-       IN_TRACE_ANALYSIS = true;
        for (unsigned int i = 0; i < trace_analyses.size(); i++)
                trace_analyses[i]->analyze(execution->get_action_trace());
-       IN_TRACE_ANALYSIS = false;
 }
 
 /**
@@ -386,6 +400,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
+       if (inspect_plugin != NULL) {
+               inspect_plugin->inspectModelAction(act);
+       }
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
@@ -415,9 +432,35 @@ bool ModelChecker::should_terminate_execution()
        return false;
 }
 
+/** @brief Exit ModelChecker upon returning to the run loop of the
+ *     model checker. */
+void ModelChecker::exit_model_checker()
+{
+       exit_flag = true;
+}
+
+/** @brief Restart ModelChecker upon returning to the run loop of the
+ *     model checker. */
+void ModelChecker::restart()
+{
+       restart_flag = true;
+}
+
+void ModelChecker::do_restart()
+{
+       restart_flag = false;
+       diverge = NULL;
+       earliest_diverge = NULL;
+       reset_to_initial_state();
+       node_stack->full_reset();
+       memset(&stats,0,sizeof(struct execution_stats));
+       execution_number = 1;
+}
+
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
+       bool has_next;
        do {
                thrd_t user_thread;
                Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL);
@@ -465,7 +508,17 @@ void ModelChecker::run()
                        t = execution->take_step(curr);
                } while (!should_terminate_execution());
 
-       } while (next_execution());
+               has_next = next_execution();
+               if (inspect_plugin != NULL && !has_next) {
+                       inspect_plugin->actionAtModelCheckingFinish();
+                       // Check if the inpect plugin set the restart flag
+                       if (restart_flag) {
+                               model_print("******* Model-checking RESTART: *******\n");
+                               has_next = true;
+                               do_restart();
+                       }
+               }
+       } while (has_next);
 
        execution->fixup_release_sequences();
 
diff --git a/model.h b/model.h
index 74cb4e1f29aaf2c649fce027fc9dd10c714eb562..94483536cf4e7468346417c7d7ad87887ecaac9e 100644 (file)
--- a/model.h
+++ b/model.h
@@ -47,6 +47,15 @@ public:
 
        void run();
 
+       /** Restart the model checker, intended for pluggins. */
+       void restart();
+
+       /** Exit the model checker, intended for pluggins. */
+       void exit_model_checker();
+
+       /** Check the exit_flag. */
+       bool get_exit_flag() const { return exit_flag; }
+
        /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context() { return &system_context; }
 
@@ -66,12 +75,15 @@ public:
        void assert_user_bug(const char *msg);
 
        const model_params params;
-       void add_trace_analysis(TraceAnalysis *a) {
-               trace_analyses.push_back(a);
-       }
-
+       void add_trace_analysis(TraceAnalysis *a) {     trace_analyses.push_back(a); }
+       void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }
        MEMALLOC
 private:
+       /** Flag indicates whether to restart the model checker. */
+       bool restart_flag;
+       /** Flag indicates whether to exit the model checker. */
+       bool exit_flag;
+
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler * const scheduler;
        NodeStack * const node_stack;
@@ -97,6 +109,10 @@ private:
 
        ModelVector<TraceAnalysis *> trace_analyses;
 
+       /** @bref Implement restart. */
+       void do_restart();
+       /** @bref Plugin that can inspect new actions. */
+       TraceAnalysis *inspect_plugin;
        /** @brief The cumulative execution stats */
        struct execution_stats stats;
        void record_stats();
index 8bb5b46900e42b7071df9bcb18e35f9a3b38225d..e8ec08050f5d8e5389c01e136fe1c0a27f374f13 100644 (file)
 
 #define REQUESTS_BEFORE_ALLOC 1024
 
-bool IN_TRACE_ANALYSIS = false;
-
 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
 int nextRequest = 0;
 int howManyFreed = 0;
+int switch_alloc = 0;
 #if !USE_MPROTECT_SNAPSHOT
 static mspace sStaticSpace = NULL;
 #endif
@@ -126,7 +125,7 @@ void model_free(void *ptr)
 /** Bootstrap allocation. Problem is that the dynamic linker calls require
  *  calloc to work and calloc requires the dynamic linker to work. */
 
-#define BOOTSTRAPBYTES 4096
+#define BOOTSTRAPBYTES 131072
 char bootstrapmemory[BOOTSTRAPBYTES];
 size_t offset = 0;
 
@@ -136,7 +135,7 @@ void * HandleEarlyAllocationRequest(size_t sz)
        sz = (sz + 7) & ~7;
 
        if (sz > (BOOTSTRAPBYTES-offset)) {
-               model_print("OUT OF BOOTSTRAP MEMORY\n");
+               model_print("OUT OF BOOTSTRAP MEMORY.  Increase the size of BOOTSTRAPBYTES in mymemory.cc\n");
                exit(EXIT_FAILURE);
        }
 
@@ -181,8 +180,11 @@ static void * user_malloc(size_t size)
 void *malloc(size_t size)
 {
        if (user_snapshot_space) {
+               if (switch_alloc) {
+                       return model_malloc(size);
+               }
                /* Only perform user allocations from user context */
-               ASSERT(!model || thread_current() || IN_TRACE_ANALYSIS);
+               ASSERT(!model || thread_current());
                return user_malloc(size);
        } else
                return HandleEarlyAllocationRequest(size);
@@ -191,8 +193,12 @@ void *malloc(size_t size)
 /** @brief Snapshotting free implementation for user programs */
 void free(void * ptr)
 {
-       if (!DontFree(ptr))
+       if (!DontFree(ptr)) {
+               if (switch_alloc) {
+                       return model_free(ptr);
+               }
                mspace_free(user_snapshot_space, ptr);
+       }
 }
 
 /** @brief Snapshotting realloc implementation for user programs */
index 461f7d1e9c0c9293fc0f60f7541b1fa392a222d3..a62ab83b9ce5cbcd82999bc9463b2949ba7a0394 100644 (file)
                return p; \
        }
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-extern bool IN_TRACE_ANALYSIS;
-
 void *model_malloc(size_t size);
 void *model_calloc(size_t count, size_t size);
 void model_free(void *ptr);
 
-#ifdef __cplusplus
-} /* extern "C" */
-#endif
-
-#ifdef __cplusplus
-extern "C" {
-#endif
 void * snapshot_malloc(size_t size);
 void * snapshot_calloc(size_t count, size_t size);
 void * snapshot_realloc(void *ptr, size_t size);
 void snapshot_free(void *ptr);
-#ifdef __cplusplus
-} /* extern "C" */
-#endif
 
 void * Thread_malloc(size_t size);
 void Thread_free(void *ptr);
index e5f46875649ab9bac345728ee3ef8eabd061015d..bacd067dcb4b8277408e2efd5685fc27bac8e2da 100644 (file)
@@ -838,6 +838,16 @@ void NodeStack::pop_restofstack(int numAhead)
        node_list.back()->clear_backtracking();
 }
 
+/** Reset the node stack. */
+void NodeStack::full_reset() 
+{
+       for (unsigned int i = 0; i < node_list.size(); i++)
+               delete node_list[i];
+       node_list.clear();
+       reset_execution();
+       total_nodes = 1;
+}
+
 Node * NodeStack::get_head() const
 {
        if (node_list.empty() || head_idx < 0)
index f26100bad0e359459bf18263009028aa8a28f4e0..6ae96be8d508d9b598ae3bb3c396760fea6047da 100644 (file)
@@ -198,6 +198,7 @@ public:
        Node * get_next() const;
        void reset_execution();
        void pop_restofstack(int numAhead);
+       void full_reset();
        int get_total_nodes() { return total_nodes; }
 
        void print() const;
index db06189df25dd4366edfb51b7a456ace7847b888..37f2f5cc55ca3c8f4d2a839fb5d0a0247cb7c05c 100644 (file)
@@ -31,7 +31,7 @@ typedef struct TagInt {
        int val;
 
        TagInt(unsigned int tag, int val) : tag(tag), val(val) { }
-       
+
        TagInt(int val) : tag(0), val(val) { }
 }TagInt;
 
@@ -40,12 +40,9 @@ typedef SnapList<int> IntList;
 typedef SnapSet<int> IntSet;
 
 template<typename Key, typename Value>
-class Map: public unordered_map<Key, Value> {
+class Map: public unordered_map<Key, Value, std::hash<Key>,
+    std::equal_to<Value>, SnapshotAlloc<std::pair<const Key, Value>>> {
        public:
-       typedef unordered_map<Key, Value> map;
-
-       Map() : map() { }
-
        Value get(Key key) {
                return (*this)[key];
        }
@@ -54,25 +51,10 @@ class Map: public unordered_map<Key, Value> {
                (*this)[key] = value;
        }
 
-       SNAPSHOTALLOC
+  SNAPSHOTALLOC
 };
 
-class IntMap : public unordered_map<int, int> {
-       public:
-       typedef unordered_map<int, int> map;
-
-       IntMap() : map() { }
-
-       int get(int key) {
-               return (*this)[key];
-       }
-
-       void put(int key, int value) {
-               (*this)[key] = value;
-       }
-
-       SNAPSHOTALLOC
-};
+typedef Map<int, int> IntMap;
 
 typedef SnapVector<double> DoubleVector;
 typedef SnapList<double> DoubleList;
index 76c59e60f698797210e64421542dd52b9b3c9459..c3145d6bf0ecd43dc09899d88350eb5fc68c4886 100755 (executable)
@@ -1,19 +1,26 @@
-#!/bin/bash
-#
+#!/bin/bash -e
 
-BENCHS=(ms-queue linuxrwlocks mcs-lock chase-lev-deque-bugfix treiber-stack
-       ticket-lock seqlock read-copy-update concurrent-hashmap spsc-bugfix mpmc-queue)
+BENCHS=(
+    'ms-queue'\
+    'linuxrwlocks' \
+    'mcs-lock' \
+    'chase-lev-deque-bugfix' \
+    'ticket-lock' \
+    'seqlock' \
+    'read-copy-update' \
+    'spsc-bugfix' \
+    'mpmc-queue'
+    'concurrent-hashmap' \
+)
 
-echo ${BENCHS[*]}
-for i in ${BENCHS[*]}; do
-       echo "----------    Start to run $i    ----------"
-       tests=$(ls $i/testcase[1-9])
-       if [ -e "$i/main" ]; then
-               tests=($tests "$i/main")
-       fi
-       if [ -e "$i/testcase" ]; then
-               tests=($tests "$i/testcase")
-       fi
+for bench in ${BENCHS[@]}; do
+       echo "----------    Start to run ${bench}    ----------"
+  # Clear the test cases.
+  tests=()
+       tests=$(ls ${bench}/testcase[1-9] 2>/dev/null || true)
+
+       [ -e "${bench}/main" ] && tests+=("${bench}/main")
+       [ -e "${bench}/testcase" ] && tests+=("${bench}/testcase")
 
        for j in ${tests[*]}; do
                ./run.sh $j -m2 -y -u3 -tSPEC
index a0bc02970aa9ff71c6e8e1a04f6565d52b6db43a..a06af84636978f1bbd31f960c0c2368d79fc609a 100644 (file)
 /** Allocate a stack for a new thread. */
 static void * stack_allocate(size_t size)
 {
-       return snapshot_malloc(size);
+       return Thread_malloc(size);
 }
 
 /** Free a stack for a terminated thread. */
 static void stack_free(void *stack)
 {
-       snapshot_free(stack);
+       Thread_free(stack);
 }
 
 /**
index df3356ad50d422c08a3a2ba7d09234ccec394f5f..d363150ab3c72e2c3efcd46a2b8dd7d88dd970a8 100644 (file)
@@ -2,6 +2,7 @@
 #define TRACE_ANALYSIS_H
 #include "model.h"
 
+
 class TraceAnalysis {
  public:
        /** setExecution is called once after installation with a reference to
@@ -30,6 +31,20 @@ class TraceAnalysis {
 
        virtual void finish() = 0;
 
+       /** This method is used to inspect the normal/abnormal model
+        * action. */
+       virtual void inspectModelAction(ModelAction *act) {}
+
+       /** This method will be called by when a plugin is installed by the
+        * model checker. */
+       virtual void actionAtInstallation() {}
+
+       /** This method will be called when the model checker finishes the
+        * executions; With this method, the model checker can alter the
+        * state of the plugin and then the plugin can choose whether or not
+        * restart the model checker. */
+       virtual void actionAtModelCheckingFinish() {}
+
        SNAPSHOTALLOC
 };
 #endif