Get gdax to not crash

diff --git a/Makefile b/Makefile
index b62e72a9de19225ab7bcc57a9da8cd8d6465a4b5..00b99cc45a12d0b89e0c4d447b3a2fb1ef4d4c84 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
-          sleeps.o
+          sleeps.o history.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic
@@ -36,6 +36,8 @@ README.html: README.md
 malloc.o: malloc.c
        $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
 
+futex.o: futex.cc
+       $(CXX) -fPIC -c futex.cc -std=c++11 $(CPPFLAGS)
 
 %.o : %.cc
        $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS)

diff --git a/action.cc b/action.cc
index 9a816de3837028c1dcec90d669237f8ba095fd49..3059e0d94be8a90c5db19ce0114cc44062f9c6aa 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -87,6 +87,40 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
 }
 
 
+/**
+ * @brief Construct a new ModelAction with source line number (requires llvm support)
+ *
+ * @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 size (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, const char * position, memory_order order, void *loc,
+                                                                                                uint64_t value, int size) :
+       location(loc),
+       position(position),
+       reads_from(NULL),
+       last_fence_release(NULL),
+       node(NULL),
+       cv(NULL),
+       value(value),
+       type(type),
+       order(order),
+       original_order(order),
+       seq_number(ACTION_INITIAL_CLOCK)
+{
+       /* References to NULL atomic variables can end up here */
+       ASSERT(loc);
+       this->size = size;
+       Thread *t = thread_current();
+       this->tid = t->get_id();
+}
+
+
 /**
  * @brief Construct a new ModelAction with source line number (requires llvm support)
  *

diff --git a/action.h b/action.h
index cebbec1beb6ba7d3f409673e92a214b792c8e623..c7703094d99ffe12213ec59a44b8c9ef0fdcc7a3 100644 (file)
--- a/action.h
+++ b/action.h
@@ -86,6 +86,7 @@ class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);
+       ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value, int size);
        ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ~ModelAction();
        void print() const;

diff --git a/classlist.h b/classlist.h
index 09aa09d134e19c1e4160896fde3a935424fc7ab6..641a148103b73f98a1d5448a9ff755867368e372 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -8,6 +8,7 @@ class CycleNode;
 class ModelAction;
 class ModelChecker;
 class ModelExecution;
+class ModelHistory;
 class Node;
 class NodeStack;
 class Scheduler;

diff --git a/cmodelint.cc b/cmodelint.cc
index b9eb214a5cffe4918939407a50526c28afedc925..9ea1b681c32d20c7adb9f62aff78f9aab21d480d 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,7 +1,10 @@
 #include <stdio.h>
+#include <string>
+
 #include "model.h"
 #include "execution.h"
 #include "action.h"
+#include "history.h"
 #include "cmodelint.h"
 #include "snapshot-interface.h"
 #include "threads-model.h"
@@ -86,7 +89,9 @@ void model_fence_action(memory_order ord) {
 
 /* ---  helper functions --- */
 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
-       ensureModelValue(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj), uint64_t);
+       ensureModelValue(
+               new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t
+               );
 }
 
 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
@@ -373,3 +378,34 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) {
         __old__ = __old__;  Silence clang (-Wunused-value)                    \
          })
  */
+
+void cds_func_entry(const char * funcName) {
+       if (!model) return;
+
+       Thread * th = thread_current();
+       uint32_t func_id;
+
+       ModelHistory *history = model->get_history();
+       if ( !history->getFuncMap()->contains(funcName) ) {
+               func_id = history->get_func_counter();
+               history->incr_func_counter();
+
+               history->getFuncMap()->put(funcName, func_id);
+       } else {
+               func_id = history->getFuncMap()->get(funcName);
+       }
+
+       history->enter_function(func_id, th->get_id());
+}
+
+void cds_func_exit(const char * funcName) {
+       if (!model) return;
+
+       Thread * th = thread_current();
+       uint32_t func_id;
+
+       ModelHistory *history = model->get_history();
+       func_id = history->getFuncMap()->get(funcName);
+
+       history->exit_function(func_id, th->get_id());
+}

diff --git a/execution.cc b/execution.cc
index 2c08711eee0d1a655272bd56f1adf0d900ef599d..2e7442515b4cf47556817f727ba3bd8a7e65b466 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
        thrd_last_fence_release(),
        node_stack(node_stack),
        priv(new struct model_snapshot_members ()),
-                        mo_graph(new CycleGraph()),
+       mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */

diff --git a/history.cc b/history.cc
new file mode 100644 (file)
index 0000000..e0560ba
--- /dev/null
+++ b/history.cc
@@ -0,0 +1,36 @@
+#include <inttypes.h>
+#include "history.h"
+#include "action.h"
+
+ModelHistory::ModelHistory() :
+       func_id(1),     /* function id starts with 1 */
+       func_map(),
+       func_history(),
+       work_list()
+{}
+
+void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
+{
+       if ( !work_list.contains(tid) ) {
+               // This thread has not been pushed to work_list
+               SnapList<uint32_t> * func_list = new SnapList<uint32_t>();
+               func_list->push_back(func_id);
+               work_list.put(tid, func_list);
+       } else {
+               SnapList<uint32_t> * func_list = work_list.get(tid);
+               func_list->push_back(func_id);
+       }
+}
+
+void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
+{
+       SnapList<uint32_t> * func_list = work_list.get(tid);
+       uint32_t last_func_id = func_list->back();
+
+       if (last_func_id == func_id) {
+               func_list->pop_back();
+       } else {
+               model_print("trying to exit with a wrong function id\n");
+               model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
+       }
+}

diff --git a/history.h b/history.h
new file mode 100644 (file)
index 0000000..441a999
--- /dev/null
+++ b/history.h
@@ -0,0 +1,39 @@
+#include "stl-model.h"
+#include "common.h"
+#include "hashtable.h"
+#include "modeltypes.h"
+
+/* forward declaration */
+class ModelAction;
+
+typedef ModelList<ModelAction *> action_mlist_t;
+
+class ModelHistory {
+public:
+       ModelHistory();
+
+       void enter_function(const uint32_t func_id, thread_id_t tid);
+       void exit_function(const uint32_t func_id, thread_id_t tid);
+
+       uint32_t get_func_counter() { return func_id; }
+       void incr_func_counter() { func_id++; }
+
+       HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
+       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> * getFuncHistory() { return &func_history; }
+
+       void print();
+
+private:
+       uint32_t func_id;
+
+       /* map function names to integer ids */
+       HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
+
+       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> func_history;
+
+       /* work_list stores a list of function ids for each thread
+        * SnapList<uint32_t> is intended to be used as a stack storing
+        * the functions that thread i has entered and yet to exit from
+        */
+       HashTable<thread_id_t, SnapList<uint32_t> *, uintptr_t, 4> work_list;
+};

diff --git a/include/cmodelint.h b/include/cmodelint.h
index 7bc6a253c9b5fedd61b7574558c647399f0207a3..78da6bd8003691255c9a67449f81d5a92cca513c 100644 (file)
--- a/include/cmodelint.h
+++ b/include/cmodelint.h
@@ -101,6 +101,9 @@ bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t d
 // cds atomic thread fence
 void cds_atomic_thread_fence(int atomic_index, const char * position);
 
+void cds_func_entry(const char * funcName);
+void cds_func_exit(const char * funcName);
+
 #if __cplusplus
 }
 #endif

diff --git a/libcdsTest/ms-queue/Makefile b/libcdsTest/ms-queue/Makefile
index 8df2ca5f423f1f41d6d336e7a7bd90bf9564c06a..a2b45572d4172ebc174dc77c2fefbd0eb454e09c 100644 (file)
--- a/libcdsTest/ms-queue/Makefile
+++ b/libcdsTest/ms-queue/Makefile
@@ -1,15 +1,21 @@
 all: intrusive_msqueue_hp.o
 
+CXX = clang++
+
 #%.o : %.cc 
 #      $(CXX) -c $@
 
-CFLAGS=-I. -I /scratch/benchmarks/libcds -std=c++11
+INCLUDE = -I. -I /scratch/benchmarks/libcds
+
+INCLUDE += -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -I. -I /scratch/benchmarks/libcds
+
+CPPFLAGS = $(INCLUDE) -g -O1 -std=c++11
 
 CDSDIR=/scratch/benchmarks/libcds/build-release/bin
 CDSLIB=-lcds_d -lpthread
 
 intrusive_msqueue_hp.o: intrusive_msqueue_hp.cc
-       $(CXX) -o msqueue intrusive_msqueue_hp.cc $(CFLAGS) -L $(CDSDIR) $(CDSLIB)
+       $(CXX) -o msqueue intrusive_msqueue_hp.cc $(CPPFLAGS) -L $(CDSDIR) $(CDSLIB)
 
 clean:
        rm -f *.o

diff --git a/libcdsTest/ms-queue/intrusive_msqueue_hp.cc b/libcdsTest/ms-queue/intrusive_msqueue_hp.cc
index 176ba5004ff6cd4b1e1e2a59d687fb5d0063dc49..88861fd73c5f13d7b45a9c78f18b88cf33929a94 100644 (file)
--- a/libcdsTest/ms-queue/intrusive_msqueue_hp.cc
+++ b/libcdsTest/ms-queue/intrusive_msqueue_hp.cc
@@ -19,6 +19,8 @@ typedef typename base_class::member_hook_item< ci::msqueue::node<gc_type>> membe
 
 typedef cds_test::intrusive_msqueue::mock_disposer mock_disposer;
 
+std::atomic_int x;
+
 template <typename Queue, typename Data>
 void test_enqueue( Queue& q, Data& arr )
 {
@@ -26,9 +28,15 @@ void test_enqueue( Queue& q, Data& arr )
     size_t nSize = arr.size();
 
     value_type * pv;
-    for ( size_t i = 0; i < nSize; ++i )
-       arr[i].nVal = static_cast<int>(i);
-
+//    for ( size_t i = 0; i < nSize; ++i )
+//     arr[i].nVal = static_cast<int>(i);
+
+    base_item_type test;
+    test.nVal = static_cast<int>(4);
+//    arr[0].nVal = static_cast<int>(5);
+    x.load();
+    q.enqueue( test );
+/*
     assert(q.empty());
     assert(q.size() == 0);
 
@@ -42,7 +50,8 @@ void test_enqueue( Queue& q, Data& arr )
     assert( pv == nullptr );
     assert( q.empty());
     assert(q.size() == 0);
-
+*/
+/*
     for ( size_t i = 0; i < nSize; ++i ) {
        if ( i & 1 )
            q.push( arr[i] );
@@ -51,6 +60,7 @@ void test_enqueue( Queue& q, Data& arr )
        assert( !q.empty());
        assert(q.size() == i+1);
     }
+*/
 }
 
 
@@ -61,34 +71,6 @@ void test_dequeue( Queue& q, Data& arr )
     size_t nSize = arr.size();
 
     value_type * pv;
-/*
-    for ( size_t i = 0; i < nSize; ++i )
-       arr[i].nVal = static_cast<int>(i);
-
-    assert(q.empty());
-    assert(q.size() == 0);
-
-    // pop from empty queue
-    pv = q.pop();
-    assert( pv == nullptr );
-    assert( q.empty());
-    assert(q.size() == 0);
-
-    pv = q.dequeue();
-    assert( pv == nullptr );
-    assert( q.empty());
-    assert(q.size() == 0);
-
-    // push/pop test
-    for ( size_t i = 0; i < nSize; ++i ) {
-       if ( i & 1 )
-           q.push( arr[i] );
-       else
-           q.enqueue( arr[i] );
-       assert( !q.empty());
-       assert(q.size() == i+1);
-    }
-*/
 
     for ( size_t i = 0; i < nSize; ++i ) {
        assert( !q.empty());
@@ -152,15 +134,14 @@ int main () {
                        std::vector<base_item_type> arr;
                        arr.resize(5);
                        printf("test start\n");
-                       {
-                               std::atomic<int> x;
-                               atomic_store_explicit(&x, 0xaaa, std::memory_order_seq_cst);
-                               test_queue q;
-                               test_enqueue(q, arr);
-                               atomic_store_explicit(&x, 0xccc, std::memory_order_seq_cst);
-                               test_dequeue(q, arr);
-                               atomic_store_explicit(&x, 0xbbb, std::memory_order_seq_cst);
-                       }
+
+                       atomic_store_explicit(&x, 0xaaa, std::memory_order_seq_cst);
+                       test_queue q;
+                       test_enqueue(q, arr);
+                       atomic_store_explicit(&x, 0xccc, std::memory_order_seq_cst);
+//                     test_dequeue(q, arr);
+                       atomic_store_explicit(&x, 0xbbb, std::memory_order_seq_cst);
+
                        printf("test end\n");
 
 //                     gc_type::scan();

diff --git a/libcdsTest/ms-queue/msqueue2 b/libcdsTest/ms-queue/msqueue2
index ded5d2a08fc7fb1d73d17b1e588bf6f8d9945568..c6121b20ab4a268f5fab52a8825412abfc2d43dc 100755 (executable)
Binary files a/libcdsTest/ms-queue/msqueue2 and b/libcdsTest/ms-queue/msqueue2 differ

diff --git a/libcdsTest/ms-queue/other b/libcdsTest/ms-queue/other
deleted file mode 100755 (executable)
index e6da92d..0000000
Binary files a/libcdsTest/ms-queue/other and /dev/null differ

diff --git a/libcdsTest/ms-queue/script.sh b/libcdsTest/ms-queue/script.sh
index 9aa72536ee96b66131de0b8d0b2fb8b9cd84e9fe..6080cb79ddb131a0cf6c705231db19df0114541b 100755 (executable)
--- a/libcdsTest/ms-queue/script.sh
+++ b/libcdsTest/ms-queue/script.sh
@@ -1,3 +1,5 @@
 #!/bin/sh
 
-clang++ -o msqueue2 -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so  intrusive_msqueue_hp.cc -I. -I /scratch/benchmarks/libcds -g -std=c++11 -L /scratch/random-fuzzer -lmodel -L /scratch/benchmarks/libcds/build-release/bin -lcds_d -lpthread
+clang++ -o msqueue2 -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so intrusive_msqueue_hp.cc -I. -I /scratch/benchmarks/libcds -g -O1 -std=c++11 -L /scratch/new-fuzzer -lmodel -L /scratch/benchmarks/libcds/libcds-llvm/bin -lcds_d -lpthread
+
+export LD_LIBRARY_PATH=/scratch/benchmarks/libcds/libcds-llvm/bin:/scratch/new-fuzzer/

diff --git a/libcdsTest/ms-queue/tmp b/libcdsTest/ms-queue/tmp
deleted file mode 100644 (file)
index 1dacb27..0000000
--- a/libcdsTest/ms-queue/tmp
+++ /dev/null
@@ -1,242 +0,0 @@
-key_delete is called
-has write to location: 0x60c1e0 values: 1 
-has write to location: 0x1a82928 values: 1a82a10 1a82a20 1a82a30 1a82a40 1a82a50 
-has write to location: 0x1a82980 values: 1 2 3 4 5 6 7 8 9 a b c d e f 10 11 
-has write to location: 0x1a829e0 values: 7f74888ecf28 0 1a82b10 0 1a82b20 0 1a82b30 0 1a82b40 0 7f74888ecf28 0 1a82b20 0 1a82b20 0 1a82b40 0 1a82b40 0 0 0 
-has write to location: 0x1a829f0 values: 1a82b10 0 1a82b10 0 1a82b30 0 1a82b30 0 1a82b50 0 1a82b50 0 
-has write to location: 0x1a82b10 values: 0 1a82b20 
-has write to location: 0x1a82b20 values: 0 1a82b30 
-has write to location: 0x1a82b30 values: 0 1a82b40 
-has write to location: 0x1a82b40 values: 0 1a82b50 
-has write to location: 0x1a82b50 values: 0 
-has write to location: 0x7f74888ecea8 values: 1a82b10 1a82b20 1a82b30 1a82b40 1a82b50 0 
-has write to location: 0x7f74888ecee8 values: 1a82b10 1a82b20 1a82b30 1a82b40 1a82b50 0 
-has write to location: 0x7f74888ecf28 values: 0 1a82b10 
-has write to location: 0x7f74888ecf68 values: 1 2 3 4 5 4 3 2 1 0 
-has write to location: 0x7f74888ecf78 values: aaa ccc bbb 
------------------------------------------
-location: 0x60c1e0: 
-0    0    uninitialized   relaxed        0x60c1e0   0                       ( 0)
-location: 0x7f74888ecee8: 
-0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
-location: 0x1a82980: 
-0    0    uninitialized   relaxed       0x1a82980   0                       ( 0)
-location: 0x7f74888ecee8: 
-0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
-location: 0x7f74888ecf28: 
-9    1    atomic write    release  0x7f74888ecf28   0                       ( 0,  9)
-location: 0x7f74888ecf28: 
-9    1    atomic write    release  0x7f74888ecf28   0                       ( 0,  9)
-location: 0x7f74888ecf68: 
-0    0    uninitialized   relaxed  0x7f74888ecf68   0                       ( 0)
-location: 0x7f74888ecee8: 
-0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
-location: 0x7f74888ecee8: 
-17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
-location: 0x1a82980: 
-12   1    atomic rmw      acq_rel       0x1a82980   0                   0   ( 0, 12)
-location: 0x7f74888ecee8: 
-17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
-location: 0x1a82b10: 
-3    1    atomic write    release       0x1a82b10   0                       ( 0,  3)
-location: 0x1a82b10: 
-3    1    atomic write    release       0x1a82b10   0                       ( 0,  3)
-location: 0x7f74888ecf68: 
-16   1    atomic rmw      relaxed  0x7f74888ecf68   0                   0   ( 0, 16)
-location: 0x7f74888ecee8: 
-17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
-location: 0x7f74888ecee8: 
-26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
-location: 0x1a82980: 
-21   1    atomic rmw      acq_rel       0x1a82980   0x1                 12  ( 0, 21)
-location: 0x7f74888ecee8: 
-26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
-location: 0x1a82b20: 
-4    1    atomic write    release       0x1a82b20   0                       ( 0,  4)
-location: 0x1a82b20: 
-4    1    atomic write    release       0x1a82b20   0                       ( 0,  4)
-location: 0x7f74888ecf68: 
-25   1    atomic rmw      relaxed  0x7f74888ecf68   0x1                 16  ( 0, 25)
-location: 0x7f74888ecee8: 
-26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
-location: 0x7f74888ecee8: 
-35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
-location: 0x1a82980: 
-30   1    atomic rmw      acq_rel       0x1a82980   0x2                 21  ( 0, 30)
-location: 0x7f74888ecee8: 
-35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
-location: 0x1a82b30: 
-5    1    atomic write    release       0x1a82b30   0                       ( 0,  5)
-location: 0x1a82b30: 
-5    1    atomic write    release       0x1a82b30   0                       ( 0,  5)
-location: 0x7f74888ecf68: 
-34   1    atomic rmw      relaxed  0x7f74888ecf68   0x2                 25  ( 0, 34)
-location: 0x7f74888ecee8: 
-35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
-location: 0x7f74888ecee8: 
-44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
-location: 0x1a82980: 
-39   1    atomic rmw      acq_rel       0x1a82980   0x3                 30  ( 0, 39)
-location: 0x7f74888ecee8: 
-44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
-location: 0x1a82b40: 
-6    1    atomic write    release       0x1a82b40   0                       ( 0,  6)
-location: 0x1a82b40: 
-6    1    atomic write    release       0x1a82b40   0                       ( 0,  6)
-location: 0x7f74888ecf68: 
-43   1    atomic rmw      relaxed  0x7f74888ecf68   0x3                 34  ( 0, 43)
-location: 0x7f74888ecee8: 
-44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
-location: 0x7f74888ecea8: 
-0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
-location: 0x1a82980: 
-48   1    atomic rmw      acq_rel       0x1a82980   0x4                 39  ( 0, 48)
-location: 0x7f74888ecea8: 
-0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
-location: 0x7f74888ecf28: 
-15   1    atomic rmw      release  0x7f74888ecf28   0                   9   ( 0, 15)
-location: 0x1a82980: 
-58   1    atomic rmw      acq_rel       0x1a82980   0x5                 48  ( 0, 58)
-location: 0x7f74888ecf28: 
-15   1    atomic rmw      release  0x7f74888ecf28   0                   9   ( 0, 15)
-location: 0x7f74888ecea8: 
-0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x7f74888ecea8: 
-0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
-location: 0x7f74888ecf68: 
-52   1    atomic rmw      relaxed  0x7f74888ecf68   0x4                 43  ( 0, 52)
-location: 0x7f74888ecea8: 
-66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
-location: 0x1a82980: 
-62   1    atomic rmw      acq_rel       0x1a82980   0x6                 58  ( 0, 62)
-location: 0x7f74888ecea8: 
-66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
-location: 0x1a82b10: 
-24   1    atomic rmw      release       0x1a82b10   0                   3   ( 0, 24)
-location: 0x1a82980: 
-72   1    atomic rmw      acq_rel       0x1a82980   0x7                 62  ( 0, 72)
-location: 0x1a82b10: 
-24   1    atomic rmw      release       0x1a82b10   0                   3   ( 0, 24)
-location: 0x7f74888ecea8: 
-66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x7f74888ecea8: 
-66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
-location: 0x7f74888ecf68: 
-67   1    atomic rmw      relaxed  0x7f74888ecf68   0x5                 52  ( 0, 67)
-location: 0x1a82928: 
-0    0    uninitialized   relaxed       0x1a82928   0x1a82a00               ( 0)
-location: 0x7f74888ecea8: 
-80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
-location: 0x1a82980: 
-76   1    atomic rmw      acq_rel       0x1a82980   0x8                 72  ( 0, 76)
-location: 0x7f74888ecea8: 
-80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
-location: 0x1a82b20: 
-33   1    atomic rmw      release       0x1a82b20   0                   4   ( 0, 33)
-location: 0x1a82980: 
-88   1    atomic rmw      acq_rel       0x1a82980   0x9                 76  ( 0, 88)
-location: 0x1a82b20: 
-33   1    atomic rmw      release       0x1a82b20   0                   4   ( 0, 33)
-location: 0x7f74888ecea8: 
-80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x7f74888ecea8: 
-80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
-location: 0x7f74888ecf68: 
-81   1    atomic rmw      relaxed  0x7f74888ecf68   0x4                 67  ( 0, 81)
-location: 0x1a82928: 
-83   1    atomic write    relaxed       0x1a82928   0x1a82a10               ( 0, 83)
-location: 0x7f74888ecea8: 
-96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
-location: 0x1a82980: 
-92   1    atomic rmw      acq_rel       0x1a82980   0xa                 88  ( 0, 92)
-location: 0x7f74888ecea8: 
-96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
-location: 0x1a82b30: 
-42   1    atomic rmw      release       0x1a82b30   0                   5   ( 0, 42)
-location: 0x1a82980: 
-104  1    atomic rmw      acq_rel       0x1a82980   0xb                 92  ( 0, 104)
-location: 0x1a82b30: 
-42   1    atomic rmw      release       0x1a82b30   0                   5   ( 0, 42)
-location: 0x7f74888ecea8: 
-96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x7f74888ecea8: 
-96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
-location: 0x7f74888ecf68: 
-97   1    atomic rmw      relaxed  0x7f74888ecf68   0x3                 81  ( 0, 97)
-location: 0x1a82928: 
-99   1    atomic write    relaxed       0x1a82928   0x1a82a20               ( 0, 99)
-location: 0x7f74888ecea8: 
-112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
-location: 0x1a82980: 
-108  1    atomic rmw      acq_rel       0x1a82980   0xc                 104 ( 0, 108)
-location: 0x7f74888ecea8: 
-112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
-location: 0x1a82b40: 
-51   1    atomic rmw      release       0x1a82b40   0                   6   ( 0, 51)
-location: 0x1a82980: 
-120  1    atomic rmw      acq_rel       0x1a82980   0xd                 108 ( 0, 120)
-location: 0x1a82b40: 
-51   1    atomic rmw      release       0x1a82b40   0                   6   ( 0, 51)
-location: 0x7f74888ecea8: 
-112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x7f74888ecea8: 
-112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
-location: 0x7f74888ecf68: 
-113  1    atomic rmw      relaxed  0x7f74888ecf68   0x2                 97  ( 0, 113)
-location: 0x1a82928: 
-115  1    atomic write    relaxed       0x1a82928   0x1a82a30               ( 0, 115)
-location: 0x7f74888ecea8: 
-128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
-location: 0x1a82980: 
-124  1    atomic rmw      acq_rel       0x1a82980   0xe                 120 ( 0, 124)
-location: 0x7f74888ecea8: 
-128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
-location: 0x1a82b50: 
-7    1    atomic write    release       0x1a82b50   0                       ( 0,  7)
-location: 0x1a82980: 
-137  1    atomic rmw      acq_rel       0x1a82980   0xf                 124 ( 0, 137)
-location: 0x1a82b50: 
-7    1    atomic write    release       0x1a82b50   0                       ( 0,  7)
-location: 0x7f74888ecea8: 
-128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
-location: 0x7f74888ecea8: 
-128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
-location: 0x7f74888ecee8: 
-53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
-location: 0x1a82928: 
-131  1    atomic write    relaxed       0x1a82928   0x1a82a40               ( 0, 131)
-Program output from execution 1:
----- BEGIN PROGRAM OUTPUT ----
-test start
-libcds - enqueue node m_pTail loc: 0x7f74888ecee8
-libcds - enqueue node m_pTail loc: 0x7f74888ecee8
-libcds - enqueue node m_pTail loc: 0x7f74888ecee8
-libcds - enqueue node m_pTail loc: 0x7f74888ecee8
-libcds - enqueue node m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
-libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
-test end
----- END PROGRAM OUTPUT   ----
-
-ecee8: ecf28, 1a82b10, 1a82b20, 1a82b30, 1a82b40, 1a82b50
-

diff --git a/model.cc b/model.cc
index 80d8845fed99714d9ba1dcd93cab9f40efcc5806..0a7913bfd5571163364f8de9b30055e03b9df0b5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -16,6 +16,7 @@
 #include "output.h"
 #include "traceanalysis.h"
 #include "execution.h"
+#include "history.h"
 #include "bugmessage.h"
 #include "params.h"
 
@@ -36,6 +37,7 @@ ModelChecker::ModelChecker() :
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
        execution(new ModelExecution(this, scheduler, node_stack)),
+       history(new ModelHistory()),
        execution_number(1),
        trace_analyses(),
        inspect_plugin(NULL)
@@ -161,7 +163,7 @@ void ModelChecker::print_bugs() const
                                                        bugs->size(),
                                                        bugs->size() > 1 ? "s" : "");
        for (unsigned int i = 0;i < bugs->size();i++)
-               (*bugs)[i]->print();
+               (*bugs)[i] -> print();
 }
 
 /**
@@ -172,15 +174,15 @@ void ModelChecker::print_bugs() const
  */
 void ModelChecker::record_stats()
 {
-       stats.num_total++;
+       stats.num_total ++;
        if (!execution->isfeasibleprefix())
-               stats.num_infeasible++;
+               stats.num_infeasible ++;
        else if (execution->have_bug_reports())
-               stats.num_buggy_executions++;
+               stats.num_buggy_executions ++;
        else if (execution->is_complete_execution())
-               stats.num_complete++;
+               stats.num_complete ++;
        else {
-               stats.num_redundant++;
+               stats.num_redundant ++;
 
                /**
                 * @todo We can violate this ASSERT() when fairness/sleep sets
@@ -261,15 +263,15 @@ bool ModelChecker::next_execution()
                return true;
        }
 // test code
-       execution_number++;
+       execution_number ++;
        reset_to_initial_state();
        return false;
 }
 
 /** @brief Run trace analyses on complete trace */
 void ModelChecker::run_trace_analyses() {
-       for (unsigned int i = 0;i < trace_analyses.size();i++)
-               trace_analyses[i]->analyze(execution->get_action_trace());
+       for (unsigned int i = 0;i < trace_analyses.size();i ++)
+               trace_analyses[i] -> analyze(execution->get_action_trace());
 }
 
 /**
@@ -369,7 +371,7 @@ void ModelChecker::run()
        char random_state[256];
        initstate(423121, random_state, sizeof(random_state));
 
-       for(int exec = 0;exec < params.maxexecutions;exec++) {
+       for(int exec = 0;exec < params.maxexecutions;exec ++) {
                Thread * t = init_thread;
 
                do {

diff --git a/model.h b/model.h
index dc325d71744398e28b75d2cfa0929c34d78e9cc8..8983d017f80fa1c5a17d53bd03edb49cedea102b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -46,6 +46,7 @@ public:
        ucontext_t * get_system_context() { return &system_context; }
 
        ModelExecution * get_execution() const { return execution; }
+       ModelHistory * get_history() const { return history; }
 
        int get_execution_number() const { return execution_number; }
 
@@ -63,6 +64,7 @@ public:
        model_params params;
        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. */
@@ -73,6 +75,7 @@ private:
        NodeStack * const node_stack;
        ModelExecution *execution;
        Thread * init_thread;
+       ModelHistory *history;
 
        int execution_number;