add a new class 'ModelHistory'

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 184bb40ef76cfe80b12ef4ebcd9e2751fa57abbf..5be511c86f0574b5a707a9ddabaa9e90156348eb 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,6 +1,10 @@
 #include <stdio.h>
+#include <string>
+
 #include "model.h"
+#include "execution.h"
 #include "action.h"
+#include "history.h"
 #include "cmodelint.h"
 #include "threads-model.h"
 
@@ -360,11 +364,32 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) {
  */
 
 void cds_func_entry(const char * funcName) {
+       if (!model) return;
+
         Thread * th = thread_current();
-        printf("thread %d Enter function %s\n", th->get_id(), funcName);
+       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();
-        printf("thread %d Exit from function %s\n", th->get_id(), funcName);
+       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/history.cc b/history.cc
new file mode 100644 (file)
index 0000000..ca52209
--- /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..fff5712
--- /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/model.cc b/model.cc
index 84a60a510456fbea7cd6f0e4e6df87499c40ee48..3235f5c488461dda1918fb2cd1bc5293441effa1 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"
 
 ModelChecker *model;
@@ -28,6 +29,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)

diff --git a/model.h b/model.h
index 2a505c3d0251064710a85f1b75aca17d912bd23e..4d8558e270613e968cccb01ea282f4af04d36a70 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. */
@@ -72,6 +74,7 @@ private:
        Scheduler * const scheduler;
        NodeStack * const node_stack;
        ModelExecution *execution;
+       ModelHistory *history;
 
        int execution_number;