From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 26 Sep 2016 18:00:59 +0000 (-0700)
Subject: Add the CDSSpec checker back end
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=refs%2Fheads%2Fcdsspec-checker;p=model-checker.git
Add the CDSSpec checker back end
---
diff --git a/Makefile b/Makefile
index eb84076..56d0dab 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
include common.mk
-SCFENCE_DIR := scfence
+SPEC_DIR := spec-analysis
OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
@@ -8,7 +8,9 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
context.o scanalysis.o execution.o plugins.o libannotate.o
-CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR)
+include $(SPEC_DIR)/Makefile
+
+CPPFLAGS += -Iinclude -I. -I$(SPEC_DIR)
LDFLAGS := -ldl -lrt -rdynamic
SHARED := -shared
@@ -34,28 +36,27 @@ docs: *.c *.cc *.h README.html
README.html: README.md
$(MARKDOWN) $< > $@
+$(LIB_SO): $(OBJECTS)
+ $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS)
malloc.o: malloc.c
- $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
-
-%.o : %.cc
- $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS)
-
-include $(SCFENCE_DIR)/Makefile
+ $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPLAGS) -Wno-unused-variable
--include $(wildcard $(SCFENCE_DIR)/.*.d)
-
-$(LIB_SO): $(OBJECTS)
- $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS)
+%.o: %.cc
+ $(CXX) -MMD -MF $(dir $@).$(notdir $@).d -fPIC -c $< -o $@ $(CPPFLAGS)
%.pdf: %.dot
dot -Tpdf $< -o $@
--include $(OBJECTS:%=.%.d)
+# Replace all the basename with
+ALL_DEPS := $(shell echo $(OBJECTS) | sed -E 's/([^ ]*\/)?([^\/ ]*)/\1\.\2.d/g')
+-include $(ALL_DEPS)
+#-include $(OBJECTS:%=.%.d)
+
PHONY += clean
clean:
- rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o
+ rm -f *.o *.so $(ALL_DEPS) *.pdf *.dot $(OBJECTS)
$(MAKE) -C $(TESTS_DIR) clean
PHONY += mrclean
diff --git a/action.cc b/action.cc
index d4c6253..2e9dece 100644
--- a/action.cc
+++ b/action.cc
@@ -9,7 +9,6 @@
#include "common.h"
#include "threads-model.h"
#include "nodestack.h"
-#include "wildcard.h"
#define ACTION_INITIAL_CLOCK 0
@@ -35,7 +34,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
uint64_t value, Thread *thread) :
type(type),
order(order),
- original_order(order),
location(loc),
value(value),
reads_from(NULL),
@@ -555,7 +553,7 @@ const char * ModelAction::get_type_str() const
case ATOMIC_WAIT: return "wait";
case ATOMIC_NOTIFY_ONE: return "notify one";
case ATOMIC_NOTIFY_ALL: return "notify all";
- case ATOMIC_ANNOTATION: return "annotation";
+ case ATOMIC_ANNOTATION: return "atomic annotation";
default: return "unknown type";
};
}
diff --git a/action.h b/action.h
index c8ad85b..ad3b828 100644
--- a/action.h
+++ b/action.h
@@ -96,8 +96,6 @@ public:
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
memory_order get_mo() const { return order; }
- memory_order get_original_mo() const { return original_order; }
- void set_mo(memory_order order) { this->order = order; }
void * get_location() const { return location; }
modelclock_t get_seq_number() const { return seq_number; }
uint64_t get_value() const { return value; }
@@ -196,9 +194,6 @@ private:
/** @brief The memory order for this operation. */
memory_order order;
- /** @brief The original memory order parameter for this operation. */
- memory_order original_order;
-
/** @brief A pointer to the memory location for this action. */
void *location;
diff --git a/common.mk b/common.mk
index bc068df..46f7e7c 100644
--- a/common.mk
+++ b/common.mk
@@ -8,7 +8,9 @@ UNAME := $(shell uname)
LIB_NAME := model
LIB_SO := lib$(LIB_NAME).so
-CPPFLAGS += -Wall -g -O3
+CPPFLAGS += -Wall -O3 -g
+
+CFLAGS := $(CPPFLAGS)
# Mac OSX options
ifeq ($(UNAME), Darwin)
diff --git a/execution.cc b/execution.cc
index 2a7e0da..eaf245d 100644
--- a/execution.cc
+++ b/execution.cc
@@ -34,7 +34,6 @@ struct model_snapshot_members {
too_many_reads(false),
no_valid_reads(false),
bad_synchronization(false),
- bad_sc_read(false),
asserted(false)
{ }
@@ -54,7 +53,6 @@ struct model_snapshot_members {
bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
- bool bad_sc_read;
bool asserted;
SNAPSHOTALLOC
@@ -204,13 +202,6 @@ 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));
@@ -1315,12 +1306,6 @@ 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;
@@ -1400,8 +1385,6 @@ 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)
@@ -1432,7 +1415,6 @@ 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();
}
@@ -1601,6 +1583,9 @@ 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)
@@ -1634,6 +1619,12 @@ 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
@@ -1765,10 +1756,9 @@ 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) {
- added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added;
- } else
- added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+ if (act->get_reads_from() == NULL)
+ continue;
+ added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
}
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
diff --git a/execution.h b/execution.h
index 9322f55..fd117ab 100644
--- a/execution.h
+++ b/execution.h
@@ -117,11 +117,11 @@ public:
action_list_t * get_action_trace() { return &action_trace; }
CycleGraph * const get_mo_graph() { return mo_graph; }
+
+ int get_execution_number() const;
SNAPSHOTALLOC
private:
- int get_execution_number() const;
-
ModelChecker *model;
const model_params * const params;
@@ -134,7 +134,6 @@ 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);
diff --git a/impatomic.cc b/impatomic.cc
index 4b5d1c2..2d48989 100644
--- a/impatomic.cc
+++ b/impatomic.cc
@@ -26,15 +26,11 @@ 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__ ) ); }
}
diff --git a/include/cdsannotate.h b/include/cdsannotate.h
index bb6e3d6..b58486d 100644
--- a/include/cdsannotate.h
+++ b/include/cdsannotate.h
@@ -2,6 +2,13 @@
#define CDS_ANNOTATE_H
#include <stdint.h>
+//#ifdef __cplusplus
+//extern "C" {
+//#endif
void cdsannotate(uint64_t analysistype, void *annotation);
+//#ifdef __cplusplus
+//}
+//#endif
+
#endif
diff --git a/include/impatomic.h b/include/impatomic.h
index b4273ee..1b9ce6b 100644
--- a/include/impatomic.h
+++ b/include/impatomic.h
@@ -2330,28 +2330,23 @@ inline bool atomic_compare_exchange_strong
inline void* atomic_fetch_add_explicit
( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
{
- 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__;
-}
+ 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__; }
- 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__ )
-{ 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__;
-}
+{
+ 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__; }
inline void* atomic_fetch_sub
( volatile atomic_address* __a__, ptrdiff_t __m__ )
diff --git a/include/model_memory.h b/include/model_memory.h
new file mode 100644
index 0000000..bb5a001
--- /dev/null
+++ b/include/model_memory.h
@@ -0,0 +1,25 @@
+#ifndef _MODEL_MEMORY_H
+#define _MODEL_MEMORY_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+void* snapshot_malloc(size_t size);
+void* snapshot_calloc(size_t count, size_t size);
+void snapshot_free(void *ptr);
+
+#define MODEL_MALLOC(x) snapshot_malloc((x))
+#define MODEL_CALLOC(x, y) snapshot_calloc((x), (y))
+#define MODEL_FREE(x) snapshot_free((x))
+
+#define CMODEL_MALLOC(x) snapshot_malloc((x))
+#define CMODEL_CALLOC(x, y) snapshot_calloc((x), (y))
+#define CMODEL_FREE(x) snapshot_free((x))
+
+#ifdef __cplusplus
+} /* extern "C" */
+#endif
+
+
+#endif
diff --git a/include/stdatomic.h b/include/stdatomic.h
index d4d2198..a5038ff 100644
--- a/include/stdatomic.h
+++ b/include/stdatomic.h
@@ -56,6 +56,38 @@ using std::atomic_ullong;
using std::atomic_wchar_t;
+/****** More atomic types *****/
+using std::atomic_int_least8_t;
+using std::atomic_uint_least8_t;
+using std::atomic_int_least16_t;
+using std::atomic_uint_least16_t;
+using std::atomic_int_least32_t;
+using std::atomic_uint_least32_t;
+using std::atomic_int_least64_t;
+using std::atomic_uint_least64_t;
+
+using std::atomic_int_fast8_t;
+using std::atomic_uint_fast8_t;
+using std::atomic_int_fast16_t;
+using std::atomic_uint_fast16_t;
+using std::atomic_int_fast32_t;
+using std::atomic_uint_fast32_t;
+using std::atomic_int_fast64_t;
+using std::atomic_uint_fast64_t;
+
+using std::atomic_intptr_t;
+using std::atomic_uintptr_t;
+
+using std::atomic_ssize_t;
+using std::atomic_size_t;
+
+using std::atomic_ptrdiff_t;
+
+using std::atomic_intmax_t;
+using std::atomic_uintmax_t;
+
+
+
using std::atomic;
using std::memory_order;
using std::memory_order_relaxed;
diff --git a/main.cc b/main.cc
index 0d1fa1c..127ffd1 100644
--- 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", required_argument, NULL, 'u'},
- {"analysis", required_argument, NULL, 't'},
- {"options", required_argument, NULL, 'o'},
+ {"uninitialized", optional_argument, NULL, 'u'},
+ {"analysis", optional_argument, NULL, 't'},
+ {"options", optional_argument, NULL, 'o'},
{"maxexecutions", required_argument, NULL, 'x'},
{0, 0, 0, 0} /* Terminator */
};
@@ -231,8 +231,6 @@ 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();
}
}
diff --git a/model.cc b/model.cc
index 3bac903..8f0efcd 100644
--- a/model.cc
+++ b/model.cc
@@ -2,7 +2,6 @@
#include <algorithm>
#include <new>
#include <stdarg.h>
-#include <string.h>
#include "model.h"
#include "action.h"
@@ -23,18 +22,14 @@ 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(),
- inspect_plugin(NULL)
+ trace_analyses()
{
- memset(&stats,0,sizeof(struct execution_stats));
}
/** @brief Destructor */
@@ -303,9 +298,6 @@ 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();
@@ -319,14 +311,6 @@ 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;
@@ -346,8 +330,10 @@ 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;
}
/**
@@ -400,9 +386,6 @@ 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");
@@ -432,35 +415,9 @@ 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);
@@ -508,17 +465,7 @@ void ModelChecker::run()
t = execution->take_step(curr);
} while (!should_terminate_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);
+ } while (next_execution());
execution->fixup_release_sequences();
diff --git a/model.h b/model.h
index 9448353..74cb4e1 100644
--- a/model.h
+++ b/model.h
@@ -47,15 +47,6 @@ 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; }
@@ -75,15 +66,12 @@ public:
void assert_user_bug(const char *msg);
const model_params params;
- void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); }
- void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; }
+ void add_trace_analysis(TraceAnalysis *a) {
+ trace_analyses.push_back(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;
@@ -109,10 +97,6 @@ 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();
diff --git a/mymemory.cc b/mymemory.cc
index 4182e09..8bb5b46 100644
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -13,6 +13,8 @@
#define REQUESTS_BEFORE_ALLOC 1024
+bool IN_TRACE_ANALYSIS = false;
+
size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
int nextRequest = 0;
int howManyFreed = 0;
@@ -124,7 +126,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 131072
+#define BOOTSTRAPBYTES 4096
char bootstrapmemory[BOOTSTRAPBYTES];
size_t offset = 0;
@@ -134,7 +136,7 @@ void * HandleEarlyAllocationRequest(size_t sz)
sz = (sz + 7) & ~7;
if (sz > (BOOTSTRAPBYTES-offset)) {
- model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n");
+ model_print("OUT OF BOOTSTRAP MEMORY\n");
exit(EXIT_FAILURE);
}
@@ -180,7 +182,7 @@ void *malloc(size_t size)
{
if (user_snapshot_space) {
/* Only perform user allocations from user context */
- ASSERT(!model || thread_current());
+ ASSERT(!model || thread_current() || IN_TRACE_ANALYSIS);
return user_malloc(size);
} else
return HandleEarlyAllocationRequest(size);
diff --git a/mymemory.h b/mymemory.h
index a62ab83..461f7d1 100644
--- a/mymemory.h
+++ b/mymemory.h
@@ -47,14 +47,30 @@
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);
diff --git a/nodestack.cc b/nodestack.cc
index bacd067..e5f4687 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -838,16 +838,6 @@ 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)
diff --git a/nodestack.h b/nodestack.h
index 6ae96be..f26100b 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -198,7 +198,6 @@ 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;
diff --git a/params.h b/params.h
index d5fd1cb..c5b617b 100644
--- a/params.h
+++ b/params.h
@@ -14,7 +14,7 @@ struct model_params {
unsigned int enabledcount;
unsigned int bound;
unsigned int uninitvalue;
- int maxexecutions;
+ unsigned int maxexecutions;
/** @brief Maximum number of future values that can be sent to the same
* read */
diff --git a/plugins.cc b/plugins.cc
index 38493de..f3852bb 100644
--- a/plugins.cc
+++ b/plugins.cc
@@ -1,6 +1,6 @@
#include "plugins.h"
#include "scanalysis.h"
-#include "scfence.h"
+#include "specanalysis.h"
ModelVector<TraceAnalysis *> * registered_analysis;
ModelVector<TraceAnalysis *> * installed_analysis;
@@ -9,7 +9,7 @@ void register_plugins() {
registered_analysis=new ModelVector<TraceAnalysis *>();
installed_analysis=new ModelVector<TraceAnalysis *>();
registered_analysis->push_back(new SCAnalysis());
- registered_analysis->push_back(new SCFence());
+ registered_analysis->push_back(new SPECAnalysis());
}
ModelVector<TraceAnalysis *> * getRegisteredTraceAnalysis() {
diff --git a/scfence/scfence.cc b/scfence/scfence.cc
index 130dc3b..63408cb 100644
--- a/scfence/scfence.cc
+++ b/scfence/scfence.cc
@@ -35,7 +35,7 @@ void SCFence::setExecution(ModelExecution * execution) {
}
const char * SCFence::name() {
- const char * name = "AUTOMO";
+ const char * name = "SCFENCE";
return name;
}
diff --git a/spec-analysis/.gitignore b/spec-analysis/.gitignore
new file mode 100644
index 0000000..e3b3c9f
--- /dev/null
+++ b/spec-analysis/.gitignore
@@ -0,0 +1,12 @@
+# generic types
+*.o
+*.swp
+*.swo
+*.so
+*~
+*.dot
+.*.d
+*.pdf
+
+# files in this directory
+/tags
diff --git a/spec-analysis/Makefile b/spec-analysis/Makefile
new file mode 100644
index 0000000..02c24e9
--- /dev/null
+++ b/spec-analysis/Makefile
@@ -0,0 +1,7 @@
+# This make file is to be added by the Makefile at the main directory
+
+LOCAL_OBJS := specanalysis.o executiongraph.o specannotation.o methodcall.o
+
+SPEC_OBJS := $(LOCAL_OBJS:%=$(SPEC_DIR)/%)
+
+OBJECTS += $(SPEC_OBJS)
diff --git a/spec-analysis/cdsspec.h b/spec-analysis/cdsspec.h
new file mode 100644
index 0000000..db06189
--- /dev/null
+++ b/spec-analysis/cdsspec.h
@@ -0,0 +1,376 @@
+#ifndef _CDSSPEC_H
+#define _CDSSPEC_H
+
+#include <vector>
+#include <list>
+#include <string>
+#include <iterator>
+#include <algorithm>
+#include <set>
+#include <unordered_map>
+
+#include <functional>
+
+#include <stdarg.h>
+
+#include "mymemory.h"
+//#include "common.h"
+#include "methodcall.h"
+
+using namespace std;
+
+/** Macro for output (stole from common.h) */
+extern int model_out;
+#define PRINT(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+
+/**
+ A special kind of integer that has been embedded with a universal tag (ID)
+*/
+typedef struct TagInt {
+ unsigned int tag;
+ int val;
+
+ TagInt(unsigned int tag, int val) : tag(tag), val(val) { }
+
+ TagInt(int val) : tag(0), val(val) { }
+}TagInt;
+
+typedef SnapVector<int> IntVector;
+typedef SnapList<int> IntList;
+typedef SnapSet<int> IntSet;
+
+template<typename Key, typename Value>
+class Map: public unordered_map<Key, Value> {
+ public:
+ typedef unordered_map<Key, Value> map;
+
+ Map() : map() { }
+
+ Value get(Key key) {
+ return (*this)[key];
+ }
+
+ void put(Key key, Value value) {
+ (*this)[key] = value;
+ }
+
+ 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 SnapVector<double> DoubleVector;
+typedef SnapList<double> DoubleList;
+typedef SnapSet<double> DoubleSet;
+
+/********** Debugging functions **********/
+template<class Container>
+inline void printContainer(Container *container) {
+ if (!container || container->size() == 0)
+ PRINT("EMPTY");
+ for (auto it = container->begin(); it != container->end(); it++) {
+ int item = *it;
+ PRINT("%d ", item);
+ }
+}
+
+inline void printMap(IntMap *container) {
+ if (!container || container->size() == 0)
+ PRINT("EMPTY");
+ for (auto it = container->begin(); it != container->end(); it++) {
+ pair<int, int> item = *it;
+ PRINT("(%d, %d) ", item.first, item.second);
+ }
+}
+
+/********** More general specification-related types and operations **********/
+
+#define NewMethodSet new SnapSet<Method>
+
+#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
+#define CAT_HELPER(a, b) a ## b
+#define X(name) CAT(__##name, __LINE__) /* unique variable */
+
+/**
+ This is a generic ForEach primitive for all the containers that support
+ using iterator to iterate.
+*/
+#define ForEach(item, container) \
+ auto X(_container) = (container); \
+ auto X(iter) = X(_container)->begin(); \
+ for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
+ X(_container)->end()) ? *X(iter) : 0)
+
+/**
+ This is a common macro that is used as a constant for the name of specific
+ variables. We basically have two usage scenario:
+ 1. In Subset operation, we allow users to specify a condition to extract a
+ subset. In that condition expression, we provide NAME, RET(type), ARG(type,
+ field) and STATE(field) to access each item's (method call) information.
+ 2. In general specification (in pre- & post- conditions and side effects),
+ we would automatically generate an assignment that assign the current
+ MethodCall* pointer to a variable namedd _M. With this, when we access the
+ state of the current method, we use STATE(field) (this is a reference
+ for read/write).
+*/
+#define ITEM _M
+#define _M ME
+
+#define S_RET __value->S_RET
+
+/**
+ This operation is specifically for Method set. For example, when we want to
+ construct an integer set from the state field "x" (which is an
+ integer) of the previous set of method calls (PREV), and the new set goes to
+ "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users
+ can use the "readSet" as an integer set (set<int>)
+*/
+#define MakeSet(type, oldset, newset, field) \
+ auto newset = new SnapSet<type>; \
+ ForEach (_M, oldset) \
+ newset->insert(field); \
+
+/**
+ We provide a more general subset operation that takes a plain boolean
+ expression on each item (access by the name "ITEM") of the set, and put it
+ into a new set if the boolean expression (Guard) on that item holds. This is
+ used as the second arguments of the Subset operation. An example to extract
+ a subset of positive elements on an IntSet "s" would be "Subset(s,
+ GeneralGuard(int, ITEM > 0))"
+*/
+#define GeneralGuard(type, expression) std::function<bool(type)> \
+ ([&](type ITEM) -> bool { return (expression);}) \
+
+/**
+ This is a more specific guard designed for the Method (MethodCall*). It
+ basically wrap around the GeneralGuard with the type Method. An example to
+ extract the subset of method calls in the PREV set whose state "x" is
+ equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
+*/
+#define Guard(expression) GeneralGuard(Method, expression)
+
+#define MostRecent(guard) mostRecent(_M, guard)
+
+/**
+ A general subset operation that takes a condition and returns all the item
+ for which the boolean guard holds.
+*/
+inline SnapSet<Method>* mostRecent(Method method, std::function<bool(MethodCall*)> condition) {
+ SnapSet<Method> *res = new SnapSet<Method>;
+ // A list of potential nodes that are most recent
+ MethodList *toCheckList = new MethodList;
+ MethodSet prev = method->prev;
+ if (prev->empty()) // method is START node
+ return res;
+ else {
+ ForEach (_M, prev)
+ toCheckList->push_back(_M);
+ }
+ // Searching loop
+ while (!toCheckList->empty()) {
+ Method _M = toCheckList->front();
+ toCheckList->pop_front();
+
+ if (condition(_M)) {
+ bool recencyFlag = true;
+ ForEach (m, res) {
+ if (MethodCall::belong(_M->allNext, m)) {
+ recencyFlag = false;
+ break;
+ }
+ }
+ if (recencyFlag)
+ res->insert(_M);
+ }
+ else { // Not what we want, keep going up the graph
+ prev = _M->prev;
+ if (!prev->empty()) {
+ ForEach (_M, prev)
+ toCheckList->push_back(_M);
+ }
+ }
+ }
+ return res;
+}
+
+
+/**
+ A general subset operation that takes a condition and returns all the item
+ for which the boolean guard holds.
+*/
+template <class T>
+inline SnapSet<T>* Subset(SnapSet<T> *original, std::function<bool(T)> condition) {
+ SnapSet<T> *res = new SnapSet<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->insert(_M);
+ }
+ return res;
+}
+
+/**
+ A general set operation that takes a condition and returns if there exists
+ any item for which the boolean guard holds.
+*/
+template <class T>
+inline bool HasItem(SnapSet<T> *original, std::function<bool(T)> condition) {
+ ForEach (_M, original) {
+ if (condition(_M))
+ return true;
+ }
+ return false;
+}
+
+
+
+/**
+ A general sublist operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old list.
+*/
+template <class T>
+inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
+ list<T> *res = new list<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}
+
+/**
+ A general subvector operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old vector.
+*/
+template <class T>
+inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
+ vector<T> *res = new vector<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}
+
+/** General for set, list & vector */
+#define Size(container) ((container)->size())
+
+#define _BelongHelper(type) \
+ template<class T> \
+ inline bool Belong(type<T> *container, T item) { \
+ return std::find(container->begin(), \
+ container->end(), item) != container->end(); \
+ }
+
+_BelongHelper(SnapSet)
+_BelongHelper(SnapVector)
+_BelongHelper(SnapList)
+
+/** General set operations */
+template<class T>
+inline SnapSet<T>* Intersect(SnapSet<T> *set1, SnapSet<T> *set2) {
+ SnapSet<T> *res = new SnapSet<T>;
+ ForEach (item, set1) {
+ if (Belong(set2, item))
+ res->insert(item);
+ }
+ return res;
+}
+
+template<class T>
+inline SnapSet<T>* Union(SnapSet<T> *s1, SnapSet<T> *s2) {
+ SnapSet<T> *res = new SnapSet<T>(*s1);
+ ForEach (item, s2)
+ res->insert(item);
+ return res;
+}
+
+template<class T>
+inline SnapSet<T>* Subtract(SnapSet<T> *set1, SnapSet<T> *set2) {
+ SnapSet<T> *res = new SnapSet<T>;
+ ForEach (item, set1) {
+ if (!Belong(set2, item))
+ res->insert(item);
+ }
+ return res;
+}
+
+template<class T>
+inline void Insert(SnapSet<T> *s, T item) { s->insert(item); }
+
+template<class T>
+inline void Insert(SnapSet<T> *s, SnapSet<T> *others) {
+ ForEach (item, others)
+ s->insert(item);
+}
+
+/*
+inline MethodSet MakeSet(int count, ...) {
+ va_list ap;
+ MethodSet res;
+
+ va_start (ap, count);
+ res = NewMethodSet;
+ for (int i = 0; i < count; i++) {
+ Method item = va_arg (ap, Method);
+ res->insert(item);
+ }
+ va_end (ap);
+ return res;
+}
+*/
+
+/********** Method call related operations **********/
+#define Id(method) method->id
+#define ID Id(_M)
+
+#define Name(method) method->name
+#define NAME Name(_M)
+
+#define StructName(type) __struct_ ## type ## __
+#define Value(method, type, field) ((StructName(type)*) method->value)->field
+#define Ret(method, type) Value(method, type, RET)
+#define CRet(method, type) Value(method, type, C_RET)
+#define Arg(method, type, arg) Value(method, type, arg)
+
+#define VALUE(type, field) Value(_M, type, field)
+#define RET(type) VALUE(type, RET)
+#define C_RET(type) VALUE(type, C_RET)
+#define ARG(type, arg) VALUE(type, arg)
+
+#define State(method, field) ((StateStruct*) method->state)->field
+#define STATE(field) State(_M, field)
+
+#define Prev(method) method->prev
+#define PREV _M->prev
+
+#define Next(method) method->next
+#define NEXT _M->next
+
+#define Concurrent(method) method->concurrent
+#define CONCURRENT _M->concurrent
+
+#define AllPrev(method) method->allPrev
+#define ALLPREV _M->allPrev
+
+#define AllNext(method) method->allNext
+#define ALLNEXT _M->allNext
+
+/***************************************************************************/
+/***************************************************************************/
+
+#endif
diff --git a/spec-analysis/executiongraph.cc b/spec-analysis/executiongraph.cc
new file mode 100644
index 0000000..fddd345
--- /dev/null
+++ b/spec-analysis/executiongraph.cc
@@ -0,0 +1,1611 @@
+#include <algorithm>
+#include "executiongraph.h"
+#include "action.h"
+#include "cyclegraph.h"
+#include "threads-model.h"
+#include "clockvector.h"
+#include "execution.h"
+#include <sys/time.h>
+#include <assert.h>
+#include <iterator>
+#include "modeltypes.h"
+#include "model-assert.h"
+#include "time.h"
+
+/******************** PotentialOP ********************/
+PotentialOP::PotentialOP(ModelAction *op, CSTR label) :
+ operation(op),
+ label(label)
+{
+
+}
+
+
+/******************** ExecutionGraph ********************/
+/********* ExecutionGraph (public functions) **********/
+/**
+ Initialze the necessary fields
+*/
+ExecutionGraph::ExecutionGraph(ModelExecution *e, bool allowCyclic) : execution(e), allowCyclic(allowCyclic) {
+ methodList = new MethodList;
+ randomHistory = NULL;
+
+ broken = false;
+ noOrderingPoint = false;
+ cyclic = false;
+ threadLists = new SnapVector<action_list_t*>;
+}
+
+void ExecutionGraph::buildGraph(action_list_t *actions) {
+ buildThreadLists(actions);
+
+ // First process the initialization annotation
+ bool hasInitAnno = false;
+ action_list_t::iterator iter = actions->begin();
+ for (; iter != actions->end(); iter++) {
+ ModelAction *act = *iter;
+ SpecAnnotation *anno = getAnnotation(act);
+ if (!anno)
+ continue;
+ // Deal with the Initialization annotation
+ if (anno->type == INIT) {
+ hasInitAnno = true;
+ AnnoInit *annoInit = (AnnoInit*) anno->annotation;
+ processInitAnnotation(annoInit);
+ break;
+ }
+ }
+ if (!hasInitAnno) {
+ model_print("There is no initialization annotation\n");
+ broken = true;
+ return;
+ }
+
+ // Process the nodes for method calls of each thread
+ buildNodesFromThreads();
+ // Establish the edges
+ buildEdges();
+}
+
+bool ExecutionGraph::isBroken() {
+ return broken;
+}
+
+bool ExecutionGraph::isNoOrderingPoint() {
+ return noOrderingPoint;
+}
+
+bool ExecutionGraph::hasCycle() {
+ if (cyclic)
+ return true;
+ if (randomHistory)
+ return false;
+ randomHistory = generateOneRandomHistory();
+ return cyclic;
+}
+
+void ExecutionGraph::resetBroken() {
+ broken = false;
+}
+
+bool ExecutionGraph::checkAdmissibility() {
+ MethodList::iterator iter1, iter2;
+ bool admissible = true;
+ for (iter1 = methodList->begin(); iter1 != methodList->end(); iter1++) {
+ Method m1 = *iter1;
+ iter1++;
+ iter2 = iter1;
+ iter1--;
+ for (; iter2 != methodList->end(); iter2++) {
+ Method m2 = *iter2;
+ if (isReachable(m1, m2) || isReachable(m2, m1))
+ continue;
+
+ /* Now we need to check whether we have a commutativity rule that
+ * says the two method calls should be ordered */
+ bool commute = true;
+ for (int i = 0; i < commuteRuleNum; i++) {
+ CommutativityRule rule = *(commuteRules + i);
+ /* Check whether condition is satisfied */
+ if (!rule.isRightRule(m1, m2)) // Not this rule
+ continue;
+ else
+ commute = rule.checkCondition(m1, m2);
+ if (!commute) // The rule requires them to be ordered
+ break;
+ }
+ // We have a rule that require m1 and m2 to be ordered
+ if (!commute) {
+ admissible = false;
+ model_print("These two nodes should not commute:\n");
+ model_print("\t");
+ ModelAction *begin1 = m1->begin;
+ ModelAction *begin2 = m2->begin;
+ int tid1 = id_to_int(begin1->get_tid());
+ int tid2 = id_to_int(begin2->get_tid());
+ model_print("%s_%d (T%d)", m1->name,
+ begin1->get_seq_number(), tid1);
+ model_print(" <-> ");
+ model_print("%s_%d (T%d)", m2->name,
+ begin2->get_seq_number(), tid2);
+ model_print("\n");
+ }
+ }
+ }
+
+ return admissible;
+}
+
+/** Checking cyclic graph specification */
+bool ExecutionGraph::checkCyclicGraphSpec(bool verbose) {
+ if (verbose) {
+ model_print("---- Start to check cyclic graph ----\n");
+ }
+
+ bool pass = false;
+ for (MethodList::iterator it = methodList->begin(); it != methodList->end();
+ it++) {
+ Method m = *it;
+ if (isFakeMethod(m))
+ continue;
+
+ StateFunctions *funcs = NULL;
+ if (verbose) {
+ m->print(false, false);
+ model_print("\n");
+
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ UpdateState_t printValue = (UpdateState_t) funcs->print->function;
+ if (printValue) {
+ model_print("\t********** Value Info **********\n");
+ (*printValue)(m);
+ }
+ }
+
+ // Cyclic graph only supports @PreCondition
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ CheckState_t preCondition = (CheckState_t)
+ funcs->preCondition->function;
+
+ // @PreCondition of Mehtod m
+ if (preCondition) {
+ pass = (*preCondition)(m, m);
+
+ if (!pass) {
+ model_print("PreCondition is not satisfied. Problematic method"
+ " is as follow: \n");
+ m->print(true, true);
+ if (verbose) {
+ model_print("---- Check cyclic graph END ----\n\n");
+ }
+ return false;
+ }
+ }
+ }
+
+ if (!pass) {
+ // Print out the graph
+ model_print("Problmatic execution graph: \n");
+ print(true);
+ } else if (verbose) {
+ // Print out the graph in verbose
+ model_print("Execution graph: \n");
+ print(true);
+ }
+
+ if (verbose) {
+ model_print("---- Check cyclic graph END ----\n\n");
+ }
+ return true;
+}
+
+
+
+
+/** To check "num" random histories */
+bool ExecutionGraph::checkRandomHistories(int num, bool stopOnFail, bool verbose) {
+ ASSERT (!cyclic);
+ bool pass = true;
+ int i;
+ for (i = 0; i < num; i++) {
+ MethodList *history = generateOneRandomHistory();
+ pass &= checkStateSpec(history, verbose, i + 1);
+ if (!pass) {
+ // Print out the graph
+ model_print("Problmatic execution graph: \n");
+ print();
+ if (stopOnFail) { // Just stop on this
+ // Recycle
+ delete history;
+ if (verbose)
+ model_print("We totally checked %d histories.\n", i + 1);
+ return false;
+ }
+ } else if (verbose) {
+ // Print out the graph in verbose
+ model_print("Execution graph: \n");
+ print();
+ }
+ // Recycle
+ delete history;
+ }
+
+ if (verbose)
+ model_print("We totally checked %d histories.\n", i);
+ return pass;
+}
+
+
+/**
+ To generate and check all possible histories.
+
+ If stopOnFailure is true, we stop generating any history and end the
+ checking process. Verbose flag controls how the checking process is exposed.
+*/
+bool ExecutionGraph::checkAllHistories(bool stopOnFailure, bool verbose) {
+ ASSERT (!cyclic);
+ MethodList *curList = new MethodList;
+ int numLiveNodes = methodList->size();
+ int historyIndex = 1;
+ if (verbose) {
+ // Print out the graph in verbose
+ print();
+ }
+
+ // FIXME: make stopOnFailure always true
+ stopOnFailure = true;
+ bool pass = checkAllHistoriesHelper(curList, numLiveNodes, historyIndex,
+ stopOnFailure, verbose);
+ if (pass) {
+ for (MethodList::iterator it = methodList->begin(); it !=
+ methodList->end(); it++) {
+ Method m = *it;
+ if (isFakeMethod(m))
+ continue;
+ if (!m->justified) {
+ model_print("\t");
+ m->print(false, false);
+ model_print(": unjustified\n");
+ pass = false;
+ break;
+ }
+ }
+ }
+
+ if (!pass && !verbose) {
+ // Print out the graph
+ print();
+ }
+ if (verbose)
+ model_print("We totally checked %d histories.\n", historyIndex - 1);
+ return pass;
+}
+
+
+/********** Several public printing functions (ExecutionGraph) **********/
+
+void ExecutionGraph::printOneHistory(MethodList *history, CSTR header) {
+ model_print("------------- %s (exec #%d) -------------\n", header,
+ execution->get_execution_number());
+ int idx = 1;
+ for (MethodList::iterator it = history->begin(); it != history->end(); it++) {
+ Method m = *it;
+ model_print("%d. ", idx++);
+ m->print(false);
+ }
+ model_print("------------- %s (exec #%d) (end) -------------\n",
+ header, execution->get_execution_number());
+}
+
+void ExecutionGraph::printAllHistories(MethodListVector *histories) {
+ model_print("------------- All histories (exec #%d) -------------\n",
+ execution->get_execution_number());
+ for (unsigned i = 0; i < histories->size(); i++) {
+ model_print("*********************** # %d ***********************\n", i + 1);
+ MethodList *history = (*histories)[i];
+ int idx = 1;
+ for (MethodList::iterator it = history->begin(); it != history->end();
+ it++) {
+ Method m = *it;
+ model_print("%d. ", idx++);
+ m->print(false);
+ }
+ if (i != histories->size() - 1)
+ model_print("\n");
+ }
+ model_print("------------- All histories (exec #%d) (end) "
+ "-------------\n\n", execution->get_execution_number());
+}
+
+/**
+ By default we print only all the edges that are directly from this mehtod
+ call node. If passed allEdges == true, we will print all the edges that are
+ reachable (SC/hb after) the current node.
+*/
+void ExecutionGraph::print(bool allEdges) {
+ model_print("\n");
+ const char *extraStr = allEdges ? "All Edges" : "";
+ model_print("------------------ Execution Graph -- %s (exec #%d)"
+ " ------------------\n", extraStr, execution->get_execution_number());
+ for (MethodList::iterator iter = methodList->begin(); iter !=
+ methodList->end(); iter++) {
+ Method m = *iter;
+ /* Print the info the this method */
+ m->print(false);
+ /* Print the info the edges directly from this node */
+ SnapSet<Method> *theSet = allEdges ? m->allNext : m->next;
+ for (SnapSet<Method>::iterator nextIter = theSet->begin(); nextIter !=
+ theSet->end(); nextIter++) {
+ Method next = *nextIter;
+ model_print("\t--> ");
+ next->print(false);
+ }
+ }
+ model_print("------------------ End Graph (exec #%d)"
+ " ------------------\n", execution->get_execution_number());
+ model_print("\n");
+}
+
+/**
+ By default we print only all the edges that are directly to this mehtod
+ call node. If passed allEdges == true, we will print all the edges that are
+ reachable (SC/hb before) from the current node.
+
+ Only for debugging!!
+*/
+void ExecutionGraph::PrintReverse(bool allEdges) {
+ model_print("\n");
+ const char *extraStr = allEdges ? "All Edges" : "";
+ model_print("------------------ Reverse Execution Graph -- %s (exec #%d)"
+ " ------------------\n", extraStr, execution->get_execution_number());
+ for (MethodList::iterator iter = methodList->begin(); iter !=
+ methodList->end(); iter++) {
+ Method m = *iter;
+ /* Print the info the this method */
+ m->print(false);
+ /* Print the info the edges directly from this node */
+ SnapSet<Method> *theSet = allEdges ? m->allPrev : m->prev;
+ for (SnapSet<Method>::iterator prevIter = theSet->begin(); prevIter !=
+ theSet->end(); prevIter++) {
+ Method prev = *prevIter;
+ model_print("\t--> ");
+ prev->print(false);
+ }
+ }
+ model_print("------------------ End Reverse Graph (exec #%d)"
+ " ------------------\n", execution->get_execution_number());
+ model_print("\n");
+}
+
+
+/********** Internal member functions (ExecutionGraph) **********/
+
+void ExecutionGraph::buildThreadLists(action_list_t *actions) {
+ int maxthreads = 0;
+ for (action_list_t::iterator it = actions->begin(); it != actions->end(); it++) {
+ ModelAction *act = *it;
+ int threadid = id_to_int(act->get_tid());
+ if (threadid == 0)
+ continue;
+ if (threadid > maxthreads) {
+ threadLists->resize(threadid + 1);
+ maxthreads = threadid;
+ }
+ action_list_t *list = (*threadLists)[threadid];
+ if (!list) {
+ list = new action_list_t;
+ (*threadLists)[threadid] = list;
+ }
+ list->push_back(act);
+ }
+}
+
+/**
+ Outside of this function, we have already processed the INIT type of
+ annotation, and we focus on extracting all the method call nodes in the
+ current thread list. This routine basically iterates the list, finds the
+ INTERFACE_BEGIN annotation, call the function extractMethod(), and advance
+ the iterator. That is to say, we would only see INIT or INTERFACE_BEGIN
+ annotations; if not, the specification annotations are wrong (we mark the
+ graph is broken)
+*/
+void ExecutionGraph::buildNodesFromThread(action_list_t *actions) {
+ action_list_t::iterator iter = actions->begin();
+
+ // FIXME: Just for the purpose of debugging
+ //printActions(actions, "BuildNodesFromThread");
+
+ // annoBegin == NULL means we are looking for the beginning annotation
+ while (iter != actions->end()) {
+ ModelAction *act = *iter;
+ SpecAnnotation *anno = getAnnotation(act);
+ if (!anno) { // Means this is not an annotation action
+ iter++;
+ continue;
+ }
+ if (anno->type == INTERFACE_BEGIN) { // Interface beginning anno
+ Method m = extractMethod(actions, iter);
+ if (m) {
+ // Get a complete method call node and store it
+ methodList->push_back(m);
+ } else {
+ broken = true;
+ model_print("Error with constructing a complete node.\n");
+ return;
+ }
+ } else if (anno->type != INIT) {
+ broken = true;
+ model_print("Missing beginning annotation.\n");
+ return;
+ } else { // This is an INIT annotation
+ iter++;
+ }
+ }
+}
+
+void ExecutionGraph::buildNodesFromThreads() {
+ /* We start from the 1st real thread */
+ for (unsigned i = 1; i < threadLists->size(); i++) {
+ buildNodesFromThread((*threadLists)[i]);
+ if (broken) // Early exit when detecting errors
+ return;
+ }
+}
+
+/**
+ Find the previous non-annotation model action (ordering point from the
+ current iterator
+*/
+ModelAction* ExecutionGraph::findPrevAction(action_list_t *actions, action_list_t::iterator
+ iter) {
+ while (iter != actions->begin()) {
+ iter--;
+ ModelAction *res = *iter;
+ if (res->get_type() != ATOMIC_ANNOTATION)
+ return res;
+ }
+ return NULL;
+}
+
+/**
+ When called, the current iter points to a beginning annotation; when done,
+ the iter points to either the end of the list or the next INTERFACE_BEGIN
+ annotation.
+*/
+Method ExecutionGraph::extractMethod(action_list_t *actions, action_list_t::iterator &iter) {
+ ModelAction *act = *iter;
+ SpecAnnotation *anno = getAnnotation(act);
+ ASSERT(anno && anno->type == INTERFACE_BEGIN);
+
+ // Partially initialize the commit point node with the already known fields
+ AnnoInterfaceInfo *info = (AnnoInterfaceInfo*) anno->annotation;
+ Method m = new MethodCall(info->name, info->value, act);
+
+ // Some declaration for potential ordering points and its check
+ CSTR label;
+ PotentialOP *potentialOP= NULL;
+ // A list of potential ordering points
+ PotentialOPList *popList = new PotentialOPList;
+ // Ordering point operation
+ ModelAction *op = NULL;
+ // Whether the potential ordering points were defined
+ bool hasAppeared = false;
+
+ bool methodComplete = false;
+ int nestedLevel = 0;
+ for (iter++; iter != actions->end(); iter++) {
+ act = *iter;
+ SpecAnnotation *anno = getAnnotation(act);
+ if (!anno)
+ continue;
+ // Now we are dealing with one annotation
+ switch (anno->type) {
+ case POTENTIAL_OP:
+ //model_print("POTENTIAL_OP\n");
+ label = (CSTR) anno->annotation;
+ op = findPrevAction(actions, iter);
+ if (!op) {
+ model_print("Potential ordering point annotation should"
+ "follow an atomic operation.\n");
+ model_print("%s_%d\n", label,
+ act->get_seq_number());
+ broken = true;
+ return NULL;
+ }
+ potentialOP = new PotentialOP(op, label);
+ popList->push_back(potentialOP);
+ break;
+ case OP_CHECK:
+ //model_print("OP_CHECK\n");
+ label = (CSTR) anno->annotation;
+ // Check if corresponding potential ordering point has appeared.
+ hasAppeared = false;
+ // However, in the current version of spec, we take the most
+ // recent one in the list as the commit point (so we use
+ // reverse iterator)
+ for (PotentialOPList::reverse_iterator popIter = popList->rbegin();
+ popIter != popList->rend(); popIter++) {
+ potentialOP = *popIter;
+ if (label == potentialOP->label) {
+ m->addOrderingPoint(potentialOP->operation);
+ hasAppeared = true;
+ break; // Done when find the "first" PCP
+ }
+ }
+ if (!hasAppeared) {
+ model_print("Ordering point check annotation should"
+ "have previous potential ordering point.\n");
+ model_print("%s_%d\n", label,
+ act->get_seq_number());
+ broken = true;
+ return NULL;
+ }
+ break;
+ case OP_DEFINE:
+ //model_print("CP_DEFINE_CHECK\n");
+ op = findPrevAction(actions, iter);
+ if (!op) {
+ model_print("Ordering point define should "
+ "follow an atomic operation.\n");
+ act->print();
+ broken = true;
+ return NULL;
+ }
+ m->addOrderingPoint(op);
+ break;
+ case OP_CLEAR:
+ //model_print("OP_CLEAR\n");
+ // Reset everything
+ // Clear the list of potential ordering points
+ popList->clear();
+ // Clear the previous list of commit points
+ m->orderingPoints->clear();
+ break;
+ case OP_CLEAR_DEFINE:
+ //model_print("OP_CLEAR_DEFINE\n");
+ // Reset everything
+ popList->clear();
+ m->orderingPoints->clear();
+ // Define the ordering point
+ op = findPrevAction(actions, iter);
+ if (!op) {
+ model_print("Ordering point clear define should "
+ "follow an atomic operation.\n");
+ act->print();
+ broken = true;
+ return NULL;
+ }
+ m->addOrderingPoint(op);
+ break;
+ case INTERFACE_BEGIN:
+ nestedLevel++;
+ break;
+ case INTERFACE_END:
+ if (nestedLevel == 0) {
+ methodComplete = true;
+ }
+ else
+ nestedLevel--;
+ break;
+ default:
+ model_print("Unknown type!! We should never get here.\n");
+ ASSERT(false);
+ return NULL;
+ }
+ if (methodComplete) // Get out of the loop when we have a complete node
+ break;
+ }
+
+ ASSERT (iter == actions->end() || (getAnnotation(*iter) &&
+ getAnnotation(*iter)->type == INTERFACE_END));
+ if (iter != actions->end())
+ iter++;
+
+ delete popList;
+ // XXX: We just allow methods to have no specified ordering points. In that
+ // case, the method is concurrent with every other method call
+ if (m->orderingPoints->size() == 0) {
+ noOrderingPoint = true;
+ return m;
+ } else {
+ // Get a complete method call
+ return m;
+ }
+}
+
+/**
+ A utility function to extract the actual annotation
+ pointer and return the actual annotation if this is an annotation action;
+ otherwise return NULL.
+*/
+SpecAnnotation* ExecutionGraph::getAnnotation(ModelAction *act) {
+ if (act->get_type() != ATOMIC_ANNOTATION)
+ return NULL;
+ if (act->get_value() != SPEC_ANALYSIS)
+ return NULL;
+ SpecAnnotation *anno = (SpecAnnotation*) act->get_location();
+ ASSERT (anno);
+ return anno;
+}
+
+void ExecutionGraph::processInitAnnotation(AnnoInit *annoInit) {
+ // Assign state initial (and copy) function
+ NamedFunction *func = annoInit->initial;
+ ASSERT (func && func->type == INITIAL);
+ initial= annoInit->initial;
+
+ func = annoInit->final;
+ ASSERT (func && func->type == FINAL);
+ final= annoInit->final;
+
+ func = annoInit->copy;
+ ASSERT (func && func->type == COPY);
+ copy= annoInit->copy;
+
+ func = annoInit->clear;
+ ASSERT (func && func->type == CLEAR);
+ clear= annoInit->clear;
+
+ func = annoInit->printState;
+ ASSERT (func && func->type == PRINT_STATE);
+ printState = annoInit->printState;
+
+ // Assign the function map (from interface name to state functions)
+ funcMap = annoInit->funcMap;
+
+ // Initialize the commutativity rules array and size
+ commuteRules = annoInit->commuteRules;
+ commuteRuleNum = annoInit->commuteRuleNum;
+}
+
+/**
+ After building up the graph (both the nodes and egdes are correctly built),
+ we also call this function to initialize the most recent justified node of
+ each method node.
+
+ A justified method node of a method m is a method that is in the allPrev set
+ of m, and all other nodes in the allPrev set of m are either before or after
+ it. The most recent justified node is the most recent one in the hb/SC
+ order.
+*/
+void ExecutionGraph::initializeJustifiedNode() {
+ MethodList::iterator it = methodList->begin();
+ // Start from the second methods in the list --- skipping the START node
+ for (it++; it != methodList->end(); it++) {
+ Method m = *it;
+ // Walk all the way up, when we have multiple immediately previous
+ // choices, pick one and check if that node is a justified node --- its
+ // concurrent set should be disjoint with the whole set m->allPrev. If
+ // not, keep going up; otherwise, that node is the most recent justified
+ // node
+
+ MethodSet prev = NULL;
+ Method justified = m;
+ do {
+ prev = justified->prev;
+ // At the very least we should have the START nodes
+ ASSERT (!prev->empty());
+
+ // setIt points to the very beginning of allPrev set
+ SnapSet<Method>::iterator setIt = prev->begin();
+ justified = *setIt;
+ // Check whether justified is really the justified node
+ if (MethodCall::disjoint(justified->concurrent, m->allPrev))
+ break;
+ } while (true);
+
+ ASSERT (justified != m);
+ // Don't forget to set the method's field
+ m->justifiedMethod = justified;
+
+ // Ensure we reset the justified field to be false in the beginning
+ m->justified = false;
+ }
+}
+
+
+/**
+ This is a very important interal function to build the graph. When called,
+ we assume that we have a list of method nodes built (extracted from the raw
+ execution), and this routine is responsible for building the connection
+ edges between them to yield an execution graph for checking
+*/
+void ExecutionGraph::buildEdges() {
+
+ MethodList::iterator iter1, iter2;
+ // First build the allPrev and allNext set (don't care if they are right
+ // previous or right next first)
+ for (iter1 = methodList->begin(); iter1 != methodList->end(); iter1++) {
+ Method m1 = *iter1;
+ iter1++;
+ iter2 = iter1;
+ iter1--;
+ for (; iter2 != methodList->end(); iter2++) {
+ Method m2 = *iter2;
+ int val = conflict(m1, m2);
+ if (val == 1) {
+ m1->allNext->insert(m2);
+ m2->allPrev->insert(m1);
+ } else if (val == -1) {
+ m2->allNext->insert(m1);
+ m1->allPrev->insert(m2);
+ } else if (val == SELF_CYCLE) {
+ if (allowCyclic) {
+ // m1 -> m2
+ m1->allNext->insert(m2);
+ m2->allPrev->insert(m1);
+ // m2 -> m1
+ m2->allNext->insert(m1);
+ m1->allPrev->insert(m2);
+ }
+ }
+ }
+ }
+
+ // Initialize two special nodes (START & FINISH)
+ Method startMethod = new MethodCall(GRAPH_START);
+ Method finishMethod = new MethodCall(GRAPH_FINISH);
+ // Initialize startMethod and finishMethd
+ startMethod->allNext->insert(finishMethod);
+ finishMethod->allPrev->insert(startMethod);
+ for (MethodList::iterator iter = methodList->begin(); iter !=
+ methodList->end(); iter++) {
+ Method m = *iter;
+ startMethod->allNext->insert(m);
+ m->allPrev->insert(startMethod);
+ m->allNext->insert(finishMethod);
+ finishMethod->allPrev->insert(m);
+ }
+ // Push these two special nodes to the beginning & end of methodList
+ methodList->push_front(startMethod);
+ methodList->push_back(finishMethod);
+
+ // Now build the prev, next and concurrent sets
+ for (MethodList::iterator iter = methodList->begin(); iter != methodList->end();
+ iter++) {
+ Method m = *iter;
+ // prev -- nodes in allPrev that are before none in allPrev
+ // next -- nodes in allNext that are after none in allNext (but we
+ // actually build this set together with building prev
+ SnapSet<Method>::iterator setIt;
+ for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) {
+ Method prevMethod = *setIt;
+ if (MethodCall::disjoint(m->allPrev, prevMethod->allNext)) {
+ m->prev->insert(prevMethod);
+ prevMethod->next->insert(m);
+ }
+ }
+
+ // concurrent -- all other nodes besides MYSELF, allPrev and allNext
+ for (MethodList::iterator concurIter = methodList->begin(); concurIter !=
+ methodList->end(); concurIter++) {
+ Method concur = *concurIter;
+ if (concur != m && !MethodCall::belong(m->allPrev, concur)
+ && !MethodCall::belong(m->allNext, concur))
+ m->concurrent->insert(concur);
+ }
+ }
+
+ if (!cyclic)
+ AssertEdges();
+ // Initialize the justified method of each method
+ if (!cyclic)
+ initializeJustifiedNode();
+}
+
+/**
+ This method call is used to check whether the edge sets of the nodes are
+ built correctly --- consistently. We should only use this routine after the
+ builiding of edges when debugging
+*/
+void ExecutionGraph::AssertEdges() {
+ // Assume there is no self-cycle in execution (ordering points are fine)
+ ASSERT (!cyclic);
+
+ MethodList::iterator it;
+ for (it = methodList->begin(); it != methodList->end(); it++) {
+ Method m = *it;
+ SnapSet<Method>::iterator setIt, setIt1;
+ int val = 0;
+
+ // Soundness of sets
+ // 1. allPrev is sound
+ for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) {
+ Method prevMethod = *setIt;
+ val = conflict(prevMethod, m);
+ ASSERT (val == 1);
+ }
+ // 2. allNext is sound
+ for (setIt = m->allNext->begin(); setIt != m->allNext->end(); setIt++) {
+ Method nextMethod = *setIt;
+ val = conflict(m, nextMethod);
+ ASSERT (val == 1);
+ }
+ // 3. concurrent is sound
+ for (setIt = m->concurrent->begin(); setIt != m->concurrent->end(); setIt++) {
+ Method concur = *setIt;
+ val = conflict(m, concur);
+ ASSERT (val == 0);
+ }
+ // 4. allPrev & allNext are complete
+ ASSERT (1 + m->allPrev->size() + m->allNext->size() + m->concurrent->size()
+ == methodList->size());
+ // 5. prev is sound
+ for (setIt = m->prev->begin(); setIt != m->prev->end(); setIt++) {
+ Method prev = *setIt;
+ ASSERT (MethodCall::belong(m->allPrev, prev));
+ for (setIt1 = m->allPrev->begin(); setIt1 != m->allPrev->end();
+ setIt1++) {
+ Method middle = *setIt1;
+ if (middle == prev)
+ continue;
+ val = conflict(prev, middle);
+ // prev is before none
+ ASSERT (val != 1);
+ }
+ }
+ // 6. prev is complete
+ for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) {
+ Method prev = *setIt;
+ if (MethodCall::belong(m->prev, prev))
+ continue;
+ // Ensure none of other previous nodes should be in the prev set
+ bool hasMiddle = false;
+ for (setIt1 = m->allPrev->begin(); setIt1 != m->allPrev->end();
+ setIt1++) {
+ Method middle = *setIt1;
+ if (middle == prev)
+ continue;
+ val = conflict(prev, middle);
+ if (val == 1)
+ hasMiddle = true;
+ }
+ ASSERT (hasMiddle);
+ }
+
+ // 7. next is sound
+ for (setIt = m->next->begin(); setIt != m->next->end(); setIt++) {
+ Method next = *setIt;
+ ASSERT (MethodCall::belong(m->allNext, next));
+ for (setIt1 = m->allNext->begin(); setIt1 != m->allNext->end();
+ setIt1++) {
+ Method middle = *setIt1;
+ if (middle == next)
+ continue;
+ val = conflict(middle, next);
+ // next is after none
+ ASSERT (val != 1);
+ }
+ }
+ // 8. next is complete
+ for (setIt = m->allNext->begin(); setIt != m->allNext->end(); setIt++) {
+ Method next = *setIt;
+ if (MethodCall::belong(m->next, next))
+ continue;
+ // Ensure none of other next nodes should be in the next set
+ bool hasMiddle = false;
+ for (setIt1 = m->allNext->begin(); setIt1 != m->allNext->end();
+ setIt1++) {
+ Method middle = *setIt1;
+ if (middle == next)
+ continue;
+ val = conflict(middle, next);
+ if (val == 1)
+ hasMiddle = true;
+ }
+ ASSERT (hasMiddle);
+ }
+ }
+}
+
+/**
+ The conflicting relation between two model actions by hb/SC. If act1 and
+ act2 commutes, it returns 0; Otherwise, if act1->act2, it returns 1; and if
+ act2->act1, it returns -1
+*/
+int ExecutionGraph::conflict(ModelAction *act1, ModelAction *act2) {
+ if (act1->happens_before(act2))
+ return 1;
+ else if (act2->happens_before(act1))
+ return -1;
+
+ if (act1->is_seqcst() && act2->is_seqcst()) {
+ if (act1->get_seq_number() < act2->get_seq_number())
+ return 1;
+ else
+ return -1;
+ } else
+ return 0;
+}
+
+/**
+ If there is no conflict between the ordering points of m1 and m2, then it
+ returns 0; Otherwise, if m1->m2, it returns 1; and if m2->m1, it returns -1.
+ If some ordering points have inconsistent conflicting relation, we print out
+ an error message (Self-cycle) and set the broken flag and return
+*/
+int ExecutionGraph::conflict(Method m1, Method m2) {
+ ASSERT (m1 != m2);
+
+ if (isStartMethod(m1))
+ return 1;
+ if (isFinishMethod(m2))
+ return 1;
+
+ action_list_t *OPs1= m1->orderingPoints;
+ action_list_t *OPs2= m2->orderingPoints;
+ // Method calls without ordering points are concurrent with any others
+ if (OPs1->empty() || OPs2->empty())
+ return 0;
+ int val = 0;
+ action_list_t::iterator iter1, iter2;
+ for (iter1 = OPs1->begin(); iter1 != OPs1->end(); iter1++) {
+ ModelAction *act1 = *iter1;
+ for (iter2 = OPs2->begin(); iter2 != OPs2->end(); iter2++) {
+ ModelAction *act2 = *iter2;
+ int res = conflict(act1, act2);
+ if (res == 0) // Commuting actions
+ continue;
+ if (val == 0)
+ val = res;
+ else if (val != res) { // Self cycle
+ cyclic = true;
+ if (!allowCyclic) {
+ model_print("There is a self cycle between the following two "
+ "methods\n");
+ m1->print();
+ m2->print();
+ broken = true;
+ }
+ return SELF_CYCLE;
+ }
+ }
+ }
+ return val;
+}
+
+/**
+ Whether m2 is before m2 in the execution graph
+*/
+bool ExecutionGraph::isReachable(Method m1, Method m2) {
+ return MethodCall::belong(m1->allNext, m2);
+}
+
+MethodVector* ExecutionGraph::getRootNodes() {
+ MethodVector *vec = new MethodVector;
+ for (MethodList::iterator it = methodList->begin(); it != methodList->end();
+ it++) {
+ Method m = *it;
+ if (!m->exist)
+ continue;
+ MethodSet prevMethods = m->allPrev;
+ if (prevMethods->size() == 0) { // Fast check (naturally a root node)
+ vec->push_back(m);
+ continue;
+ }
+
+ // Also a root when all previous nodes no longer exist
+ bool isRoot = true;
+ for (SnapSet<Method>::iterator setIt = prevMethods->begin(); setIt !=
+ prevMethods->end(); setIt++) {
+ Method prev = *setIt;
+ if (prev->exist) { // It does have an incoming edge
+ isRoot = false;
+ break;
+ }
+ }
+ // It does not have an incoming edge now
+ if (isRoot)
+ vec->push_back(m);
+ }
+ return vec;
+}
+
+/**
+ Collects the set of method call nodes that do NOT have any following nodes
+ (the tail of the graph)
+*/
+MethodVector* ExecutionGraph::getEndNodes() {
+ MethodVector *vec = new MethodVector;
+ for (MethodList::iterator it = methodList->begin(); it != methodList->end();
+ it++) {
+ Method m = *it;
+ if (m->next->size() == 0)
+ vec->push_back(m);
+ }
+ return vec;
+}
+
+/**
+ This is a helper function for generating all the topological sortings of the
+ execution graph. The idea of this function is recursively do the following
+ process: logically mark whether a method call node is alive or not
+ (initially all are alive), find a list of nodes that are root nodes (that
+ have no incoming edges), continuously pick one node in that list, add it to the curList
+ (which stores one topological sorting), and then recursively call itself to
+ resolve the rest.
+
+ Arguments:
+ curList -> It represents a temporal result of a specific topological
+ sorting; keep in mind that before calling this function, pass an empty
+ list.
+ numLiveNodes -> The number of nodes that are logically alive (that have not
+ been selected and added in a specific topological sorting yet). We keep
+ such a number as an optimization since when numLinveNodes equals to 0,
+ we can backtrack. Initially it is the size of the method call list.
+ historyIndex -> The current history index. We should start with 1.
+ stopOnFailure -> Stop the checking once we see a failed history
+ verbose -> Whether the verbose mode is on
+*/
+bool ExecutionGraph::checkAllHistoriesHelper(MethodList *curList, int
+ &numLiveNodes, int &historyIndex, bool stopOnFailure, bool verbose) {
+ if (cyclic)
+ return false;
+
+ bool satisfied = true;
+ if (numLiveNodes == 0) { // Found one sorting, and we can backtrack
+ // Don't forget to increase the history number
+ satisfied = checkStateSpec(curList, verbose, historyIndex++);
+ // Don't forget to recycle
+ delete curList;
+ return satisfied;
+ }
+
+ MethodVector *roots = getRootNodes();
+ // Cycle exists (no root nodes but still have live nodes
+ if (roots->size() == 0) {
+ model_print("There is a cycle in this graph so we cannot generate"
+ " sequential histories\n");
+ cyclic = true;
+ return false;
+ }
+
+ for (unsigned i = 0; i < roots->size(); i++) {
+ Method m = (*roots)[i];
+ m->exist = false;
+ numLiveNodes--;
+ // Copy the whole current list and use that copy for the next recursive
+ // call (because we will need the same copy for other iterations at the
+ // same level of recursive calls)
+ MethodList *newList = new MethodList(*curList);
+ newList->push_back(m);
+
+ bool oneSatisfied = checkAllHistoriesHelper(newList, numLiveNodes,
+ historyIndex, stopOnFailure, verbose);
+ // Stop the checking once failure or cycle detected
+ if (!oneSatisfied && (cyclic || stopOnFailure)) {
+ delete curList;
+ delete roots;
+ return false;
+ }
+ satisfied &= oneSatisfied;
+ // Recover
+ m->exist = true;
+ numLiveNodes++;
+ }
+ delete curList;
+ delete roots;
+ return satisfied;
+}
+
+/** To check one generated history */
+bool ExecutionGraph::checkHistory(MethodList *history, int historyIndex, bool
+ verbose) {
+ bool pass = checkStateSpec(history, verbose, historyIndex);
+ if (!pass) {
+ // Print out the graph
+ model_print("Problmatic execution graph: \n");
+ print();
+ } else if (verbose) {
+ // Print out the graph in verbose
+ model_print("Execution graph: \n");
+ print();
+ }
+ return pass;
+}
+
+/** Generate one random topological sorting */
+MethodList* ExecutionGraph::generateOneRandomHistory() {
+ MethodList *res = new MethodList;
+ int liveNodeNum = methodList->size();
+ generateOneRandomHistoryHelper(res, liveNodeNum);
+ if (cyclic) {
+ delete res;
+ return NULL;
+ }
+ // Reset the liveness of each method
+ for (MethodList::iterator it = methodList->begin(); it != methodList->end();
+ it++) {
+ Method m = *it;
+ m->exist = true;
+ }
+ return res;
+}
+
+/**
+ The helper function to generate one random topological sorting
+*/
+void ExecutionGraph::generateOneRandomHistoryHelper(MethodList
+ *curList, int &numLiveNodes) {
+ if (cyclic)
+ return;
+
+ if (numLiveNodes == 0) { // Found one sorting, and we can return
+ // Don't forget to recycle
+ return;
+ }
+
+ MethodVector *roots = getRootNodes();
+ // Cycle exists (no root nodes but still have live nodes
+ if (roots->size() == 0) {
+ model_print("There is a cycle in this graph so we cannot generate"
+ " sequential histories\n");
+ cyclic = true;
+ return;
+ }
+
+ srand (time(NULL));
+ int pick = rand() % roots->size();
+ Method m = (*roots)[pick];
+
+ m->exist = false;
+ numLiveNodes--;
+ curList->push_back(m);
+
+ delete roots;
+ generateOneRandomHistoryHelper(curList, numLiveNodes);
+}
+
+Method ExecutionGraph::getStartMethod() {
+ return methodList->front();
+}
+
+Method ExecutionGraph::getFinishMethod() {
+ return methodList->back();
+}
+
+/**
+ Print out the ordering points and dynamic calling info (return value &
+ arguments) of all the methods in the methodList
+*/
+void ExecutionGraph::printAllMethodInfo(bool verbose) {
+ model_print("------------------ Method Info (exec #%d)"
+ " ------------------\n", execution->get_execution_number());
+ for (MethodList::iterator iter = methodList->begin(); iter !=
+ methodList->end(); iter++) {
+ Method m = *iter;
+ printMethodInfo(m, verbose);
+ }
+ model_print("------------------ End Info (exec #%d)"
+ " ------------------\n\n", execution->get_execution_number());
+}
+
+/**
+ Print out the ordering points and dynamic calling info (return value &
+ arguments).
+*/
+void ExecutionGraph::printMethodInfo(Method m, bool verbose) {
+ StateFunctions *funcs = NULL;
+ m->print(verbose, true);
+
+ if (isFakeMethod(m))
+ return;
+
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ UpdateState_t printValue = (UpdateState_t) funcs->print->function;
+
+ model_print("\t********** Value Info **********\n");
+ if (printValue) {
+ (*printValue)(m);
+ } else {
+ model_print("\tNothing printed..\n");
+ }
+}
+
+
+/** Clear the states of the method call */
+void ExecutionGraph::clearStates() {
+ UpdateState_t clearFunc = (UpdateState_t) clear->function;
+ for (MethodList::iterator it = methodList->begin(); it != methodList->end();
+ it++) {
+ Method m = *it;
+ if (m->state) {
+ (*clearFunc)(m);
+ }
+ }
+}
+
+
+/**
+ Checking the state specification (in sequential order)
+*/
+bool ExecutionGraph::checkStateSpec(MethodList *history, bool verbose, int
+ historyIndex) {
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Start to check history #%d ----\n", historyIndex);
+ else
+ model_print("---- Start to check history ----\n");
+ }
+
+ // @Transition can also return a boolean. For example when a steal() and
+ // take() in the deque both gets the last element, then we can see a bug in
+ // the evaluating the list of @Transitions for a following operation.
+ bool satisfied = true;
+
+ // @Initial state (with a fake starting node)
+ Method startMethod = getStartMethod();
+ UpdateState_t initialFunc = (UpdateState_t) initial->function;
+ UpdateState_t printStateFunc = (UpdateState_t) printState->function;
+ UpdateState_t clearFunc = (UpdateState_t) clear->function;
+
+ // We execute the equivalent sequential data structure with the state of the
+ // startMethod node
+ (*initialFunc)(startMethod);
+ if (verbose) {
+ startMethod->print(false, true);
+ model_print("\t@Initial on START\n");
+ if (printStateFunc) { // If user has defined the print-out function
+ model_print("\t********** State Info **********\n");
+ (*printStateFunc)(startMethod);
+ }
+ }
+
+ StateFunctions *funcs = NULL;
+ /** Execute each method call in the history */
+ for (MethodList::iterator it = history->begin(); it != history->end();
+ it++) {
+ Method m = *it;
+ if (isFakeMethod(m))
+ continue;
+
+ StateTransition_t transition = NULL;
+
+ if (verbose) {
+ m->print(false, true);
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ UpdateState_t printValue = (UpdateState_t) funcs->print->function;
+ if (printValue) {
+ model_print("\t********** Value Info **********\n");
+ (*printValue)(m);
+ }
+ }
+
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+
+ CheckState_t preCondition = (CheckState_t)
+ funcs->preCondition->function;
+ // @PreCondition of Mehtod m
+ if (preCondition) {
+ satisfied = (*preCondition)(startMethod, m);
+
+ if (!satisfied) {
+ model_print("PreCondition is not satisfied. Problematic method"
+ " is as follow: \n");
+ m->print(true, true);
+ printOneHistory(history, "Failed History");
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Check history #%d END ----\n\n",
+ historyIndex);
+ else
+ model_print("---- Check history END ----\n\n");
+ }
+ break;
+ }
+ }
+
+ // After checking the PreCondition, we run the transition on the
+ // startMethod node to update its state
+ transition = (StateTransition_t) funcs->transition->function;
+ // @Transition on the state of startMethod
+ satisfied = (*transition)(startMethod, m);
+ if (!satisfied) { // Error in evaluating @Transition
+ model_print("Transition returns false. Problematic method"
+ " is as follow: \n");
+ m->print(true, true);
+ printOneHistory(history, "Failed History");
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Check history #%d END ----\n\n",
+ historyIndex);
+ else
+ model_print("---- Check history END ----\n\n");
+ }
+ break;
+ }
+
+ if (verbose) {
+ model_print("\t@Transition on itself\n");
+ if (printStateFunc) {
+ model_print("\t********** State Info **********\n");
+ (*printStateFunc)(startMethod);
+ }
+ }
+
+ // @PostCondition of Mehtod m
+ CheckState_t postCondition = (CheckState_t)
+ funcs->postCondition->function;
+ if (postCondition) {
+ satisfied = (*postCondition)(startMethod, m);
+
+ if (!satisfied) {
+ model_print("PostCondition is not satisfied. Problematic method"
+ " is as follow: \n");
+ m->print(true, true);
+ printOneHistory(history, "Failed History");
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Check history #%d END ----\n\n",
+ historyIndex);
+ else
+ model_print("---- Check history END ----\n\n");
+ }
+ break;
+ }
+ }
+ }
+
+ // Clear out the states created when checking
+ (*clearFunc)(startMethod);
+
+ if (satisfied && verbose) {
+ printOneHistory(history, "Passed History");
+ // Print the history in verbose mode
+ if (historyIndex > 0)
+ model_print("---- Check history #%d END ----\n\n", historyIndex);
+ else
+ model_print("---- Check history END ----\n\n");
+ }
+
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Start to check justifying subhistory #%d ----\n", historyIndex);
+ else
+ model_print("---- Start to check justifying subhistory ----\n");
+
+ }
+ for (MethodList::iterator it = history->begin(); it != history->end();
+ it++) {
+ Method m = *it;
+ if (isFakeMethod(m))
+ continue;
+ // Check justifying subhistory
+ if (!m->justified) {
+ funcs = funcMap->get(m->name);
+ CheckState_t justifyingPrecondition = (CheckState_t)
+ funcs->justifyingPrecondition->function;
+ CheckState_t justifyingPostcondition = (CheckState_t)
+ funcs->justifyingPostcondition->function;
+ if (!justifyingPrecondition && !justifyingPostcondition ) {
+ // No need to check justifying conditions
+ m->justified = true;
+ if (verbose) {
+ model_print("\tMethod call ");
+ m->print(false, false);
+ model_print(": automatically justified.\n");
+ }
+ } else {
+ bool justified = checkJustifyingSubhistory(history, m, verbose, historyIndex);
+ if (justified) {
+ // Set the "justified" flag --- no need to check again for cur
+ m->justified = true;
+ if (verbose) {
+ model_print("\tMethod call ");
+ m->print(false, false);
+ model_print(": is justified\n");
+ }
+ } else {
+ if (verbose) {
+ model_print("\tMethod call ");
+ m->print(false, false);
+ model_print(": has NOT been justified yet\n");
+ }
+ }
+ }
+ } else {
+ if (verbose) {
+ model_print("\tMethod call ");
+ m->print(false, false);
+ model_print(": is justified\n");
+ }
+ }
+ }
+ if (verbose) {
+ if (historyIndex > 0)
+ model_print("---- Start to check justifying subhistory #%d END ----\n\n", historyIndex);
+ else
+ model_print("---- Start to check justifying subhistory # END ----\n\n");
+
+ }
+
+ return satisfied;
+}
+
+bool ExecutionGraph::checkJustifyingSubhistory(MethodList *history, Method
+ cur, bool verbose, int historyIndex) {
+ if (verbose) {
+ model_print("\tMethod call ");
+ cur->print(false, false);
+ model_print(": is being justified\n");
+ }
+
+ // @Transition can also return a boolean. For example when a steal() and
+ // take() in the deque both gets the last element, then we can see a bug in
+ // the evaluating the list of @Transitions for a following operation.
+ bool satisfied = true;
+
+ // @Initial state (with a fake starting node)
+ Method startMethod = getStartMethod();
+ UpdateState_t initialFunc = (UpdateState_t) initial->function;
+ UpdateState_t printStateFunc = (UpdateState_t) printState->function;
+ UpdateState_t printVauleFunc = NULL;
+ UpdateState_t clearFunc = (UpdateState_t) clear->function;
+
+ // We execute the equivalent sequential data structure with the state of the
+ // current method call
+ (*initialFunc)(cur);
+ if (verbose) {
+ startMethod->print(false, true);
+ model_print("\t@Initial on ");
+ cur->print(false, true);
+ if (printStateFunc) { // If user has defined the print-out function
+ model_print("\t********** State Info **********\n");
+ (*printStateFunc)(cur);
+ }
+ }
+
+ StateFunctions *funcs = NULL;
+ StateTransition_t transition = NULL;
+ /** Execute each method call in the justifying subhistory till cur */
+ for (MethodList::iterator it = history->begin(); it != history->end(); it++) {
+ Method m = *it;
+ if (m == cur)
+ break;
+ if (isFakeMethod(m))
+ continue;
+
+ // Ignore method calls that are not in my justifying subhistory
+ if (!MethodCall::belong(cur->allPrev, m))
+ continue;
+
+
+ if (verbose) {
+ m->print(false, true);
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ UpdateState_t printValue = (UpdateState_t) funcs->print->function;
+ if (printValue) {
+ model_print("\t********** Value Info **********\n");
+ (*printValue)(m);
+ }
+ }
+
+ funcs = funcMap->get(m->name);
+ ASSERT (funcs);
+ transition = (StateTransition_t)
+ funcs->transition->function;
+
+ // In checking justifying behaviors, we don't check precondition &
+ // postcondition for other method calls
+
+ // @Transition on the state of the "cur" method call
+ satisfied = (*transition)(cur, m);
+ if (!satisfied) { // Error in evaluating @Transition
+ if (verbose) {
+ model_print("\tFailed @Transition before\n");
+ }
+ // Clear out the states created when checking
+ (*clearFunc)(startMethod);
+ return false;
+ } else {
+ if (verbose) {
+ model_print("\t@Transition on itself\n");
+ if (printStateFunc) {
+ model_print("\t********** State Info **********\n");
+ (*printStateFunc)(startMethod);
+ }
+ }
+ }
+ }
+
+ // For justifying subhistory, we only check the @JustifyingPrecondition &
+ // @JustifyingPostcondition for the last method call (the one we are
+ // checking)
+
+ // First check the @JustifyingPrecondition
+ funcs = funcMap->get(cur->name);
+ if (satisfied) {
+ // Check the justifying preondition on cur
+ CheckState_t justifyingPrecondition = (CheckState_t)
+ funcs->justifyingPrecondition->function;
+ if (justifyingPrecondition) {
+ // @JustifyingPrecondition of Mehtod cur
+ satisfied = (*justifyingPrecondition)(cur, cur);
+ }
+ if (!satisfied) {
+ if (verbose) {
+ model_print("\tFailed @JustifyingPrecondition\n");
+ }
+ // Clear out the states created when checking
+ (*clearFunc)(startMethod);
+ return false;
+ }
+ }
+
+ // Then execute the @Transition
+ transition = (CheckState_t) funcs->transition->function;
+ // @Transition on the state of the "cur" method call
+ satisfied = (*transition)(cur, cur);
+ if (!satisfied) { // Error in evaluating @Transition
+ if (verbose) {
+ model_print("\tFailed @Transition on itself\n");
+ }
+ // Clear out the states created when checking
+ (*clearFunc)(startMethod);
+ return false;
+ }
+ if (verbose) {
+ model_print("\t@Transition on itself\n");
+ if (printStateFunc) {
+ model_print("\t********** State Info **********\n");
+ (*printStateFunc)(startMethod);
+ }
+ }
+
+ // Finally check the @JustifyingPostcondition
+ if (satisfied) {
+ // Check the justifying preondition on cur
+ funcs = funcMap->get(cur->name);
+ CheckState_t justifyingPostcondition = (CheckState_t)
+ funcs->justifyingPostcondition->function;
+ if (justifyingPostcondition) {
+ // @JustifyingPostcondition of Mehtod cur
+ satisfied = (*justifyingPostcondition)(cur, cur);
+ }
+ }
+
+ // Clear out the states created when checking
+ (*clearFunc)(startMethod);
+ return satisfied;
+}
+
+
+/**
+ To take a list of actions and print it out in a nicer way
+*/
+void ExecutionGraph::printActions(action_list_t *actions, const char *header) {
+ model_print("%s\n", header);
+ model_print("---------- Thread List (Begin) ---------\n");
+ for (action_list_t::iterator it = actions->begin(); it != actions->end();
+ it++) {
+ ModelAction *act = *it;
+ SpecAnnotation *anno = getAnnotation(act);
+ if (anno) {
+ model_print("%s -> ", specAnnoType2Str(anno->type));
+ }
+ act->print();
+ }
+ model_print("---------- Thread List (End) ---------\n");
+}
+
+void ExecutionGraph::printOneSubhistory(MethodList *history, Method cur, CSTR header) {
+ model_print("------------- %s (exec #%d) -------------\n", header,
+ execution->get_execution_number());
+ int idx = 1;
+ for (MethodList::iterator it = history->begin(); it != history->end(); it++) {
+ Method m = *it;
+ if (!MethodCall::belong(cur->allPrev, m))
+ continue;
+ model_print("%d. ", idx++);
+ m->print(false);
+ }
+ model_print("------------- %s (exec #%d) (end) -------------\n",
+ header, execution->get_execution_number());
+}
+
diff --git a/spec-analysis/executiongraph.h b/spec-analysis/executiongraph.h
new file mode 100644
index 0000000..870fd60
--- /dev/null
+++ b/spec-analysis/executiongraph.h
@@ -0,0 +1,338 @@
+#ifndef _EXECUTIONGRAPH_H
+#define _EXECUTIONGRAPH_H
+
+#include <stack>
+
+#include "hashtable.h"
+#include "specannotation.h"
+#include "mymemory.h"
+#include "modeltypes.h"
+#include "action.h"
+#include "common.h"
+#include "execution.h"
+
+#include "methodcall.h"
+#include "specannotation.h"
+
+
+const int SELF_CYCLE = 0xfffe;
+
+/**
+ Record the a potential commit point information, including the potential
+ commit point label number and the corresponding operation
+*/
+typedef struct PotentialOP {
+ ModelAction *operation;
+ CSTR label;
+
+ PotentialOP(ModelAction *op, CSTR name);
+
+ SNAPSHOTALLOC
+} PotentialOP;
+
+class Graph;
+
+
+typedef SnapList<PotentialOP*> PotentialOPList;
+
+/**
+ This represents the execution graph at the method call level. Each node is a
+ MethodCall type that has the runtime info (return value & arguments) and the
+ state info the method call. The edges in this graph are the hb/SC edges
+ dereived from the ordering points of the method call. Those edges
+ information are stoed in the PREV and NEXT set of MethodCall struct.
+*/
+class ExecutionGraph {
+ public:
+ ExecutionGraph(ModelExecution *e, bool allowCyclic);
+
+ /********** Public class interface for the core checking engine **********/
+ /**
+ Build the graph for an execution. It should returns true when the graph
+ is correctly built
+ */
+ void buildGraph(action_list_t *actions);
+
+ /** Check whether this is a broken execution */
+ bool isBroken();
+
+ /** Check whether this is an execution that has method calls without
+ * ordering points */
+ bool isNoOrderingPoint();
+
+ /**
+ Check whether this is a cyclic execution graph, meaning that the graph
+ has an cycle derived from the ordering points' hb/SC relation
+ */
+ bool hasCycle();
+
+ /** Reset the internal graph "broken" state to okay again */
+ void resetBroken();
+
+ /** Check whether the execution is admmisible */
+ bool checkAdmissibility();
+
+ /** Checking cyclic graph specification */
+ bool checkCyclicGraphSpec(bool verbose);
+
+ /** Check whether a number of random history is correct */
+ bool checkRandomHistories(int num = 1, bool stopOnFail = true, bool verbose = false);
+
+ /** Check whether all histories are correct */
+ bool checkAllHistories(bool stopOnFailure = true, bool verbose = false);
+
+ /********** A few public printing functions for DEBUGGING **********/
+
+ /**
+ Print out the ordering points and dynamic calling info (return value &
+ arguments) of all the methods in the methodList
+ */
+ void printAllMethodInfo(bool verbose);
+
+ /** Print a random sorting */
+ void printOneHistory(MethodList *list, CSTR header = "A random history");
+
+ /** Print all the possible sortings */
+ void printAllHistories(MethodListVector *sortings);
+
+ /** Print out the graph for the purpose of debugging */
+ void print(bool allEdges = false);
+
+ /**
+ Print out the graph in reverse order (with previous edges) for the
+ purpose of debugging
+ */
+ void PrintReverse(bool allEdges);
+
+ SNAPSHOTALLOC
+
+ private:
+ /** The corresponding execution */
+ ModelExecution *execution;
+
+ /** All the threads each in a separate list of actions */
+ SnapVector<action_list_t*> *threadLists;
+
+ /** A plain list of all method calls (Method) in this execution */
+ MethodList *methodList;
+
+ /**
+ A list that represents some random history. The reason we have this here
+ is that before checking anything, we have to check graph acyclicity, and
+ that requires us to check whether we can generate a topological sorting.
+ Therefore, when we check it, we store that random result here.
+ */
+ MethodList *randomHistory;
+
+ /** Whether this is a broken graph */
+ bool broken;
+
+ /** Whether this graph has method calls that have no ordering points */
+ bool noOrderingPoint;
+
+ /** Whether there is a cycle in the graph */
+ bool cyclic;
+
+ /** Whether users expect us to check cyclic graph */
+ bool allowCyclic;
+
+
+ /** The state initialization function */
+ NamedFunction *initial;
+
+ /** FIXME: The final check function; we might delete this */
+ NamedFunction *final;
+
+ /** The state copy function */
+ NamedFunction *copy;
+
+ /** The state clear function */
+ NamedFunction *clear;
+
+ /** The state print-out function */
+ NamedFunction *printState;
+
+ /** The map from interface label name to the set of spec functions */
+ StateFuncMap *funcMap;
+
+ /** The commutativity rule array and its size */
+ CommutativityRule *commuteRules;
+ int commuteRuleNum;
+
+ /********** Internal member functions **********/
+
+ /**
+ Simply build a vector of lists of thread actions. Such info will be very
+ useful for later constructing the execution graph
+ */
+ void buildThreadLists(action_list_t *actions);
+
+ /** Build the nodes from a thread list */
+ void buildNodesFromThread(action_list_t *actions);
+
+ /** Build the nodes from all the thread lists */
+ void buildNodesFromThreads();
+
+
+ /**
+ Find the previous non-annotation model action (ordering point from the
+ current iterator
+ */
+ ModelAction* findPrevAction(action_list_t *actions, action_list_t::iterator
+ iter);
+
+ /**
+ Extract a MethodCall node starting from the current iterator, and the
+ iter iterator will be advanced to the next INTERFACE_BEGIN annotation.
+ When called, the iter must point to an INTERFACE_BEGIN annotation
+ */
+ Method extractMethod(action_list_t *actions, action_list_t::iterator &iter);
+
+ /**
+ Process the initialization annotation block to initialize the
+ commutativity rule info and the checking function info
+ */
+ void processInitAnnotation(AnnoInit *annoInit);
+
+ /**
+ A utility function to extract the actual annotation
+ pointer and return the actual annotation if this is an annotation action;
+ otherwise return NULL.
+ */
+ SpecAnnotation* getAnnotation(ModelAction *act);
+
+ /**
+ After building up the graph (both the nodes and egdes are correctly
+ built), we also call this function to initialize the most recent
+ justified node of each method node.
+
+ A justified method node of a method m is a method that is in the allPrev
+ set of m, and all other nodes in the allPrev set of m are either before
+ or after it. The most recent justified node is the most recent one in
+ the hb/SC order.
+ */
+ void initializeJustifiedNode();
+
+ /**
+ After extracting the MethodCall info for each method call, we use this
+ function to build the edges (a few different sets of edges that
+ represent the edge of the execution graph (PREV, NEXT & CONCURRENT...)
+ */
+ void buildEdges();
+
+ /**
+ This method call is used to check whether the edge sets of the nodes are
+ built correctly --- consistently. We should only use this routine after the
+ builiding of edges when debugging
+ */
+ void AssertEdges();
+
+ /**
+ The conflicting relation between two model actions by hb/SC. If act1 and
+ act2 commutes, it returns 0; Otherwise, if act1->act2, it returns 1; and
+ if act2->act1, it returns -1
+ */
+ int conflict(ModelAction *act1, ModelAction *act2);
+
+ /**
+ If there is no conflict between the ordering points of m1 and m2, then
+ it returns 0; Otherwise, if m1->m2, it returns 1; and if m2->m1, it
+ returns -1. If some ordering points have inconsistent conflicting
+ relation, we print out an error message (Self-cycle) and set the broken
+ flag and return
+ */
+ int conflict(Method m1, Method m2);
+
+ /**
+ Check whether m1 is before m2 in hb/SC; Reachability <=> m1 -hb/SC-> m2.
+ We need to call this method when checking admissibility properties
+ */
+ bool isReachable(Method m1, Method m2);
+
+ /**
+ Find the list of nodes that do not have any incoming edges (root nodes).
+ Be careful that when generating histories, this function will also
+ consider whether a method node logicall exists.
+ */
+ MethodVector* getRootNodes();
+
+ /**
+ Find the list of nodes that do not have any outgoing edges (end nodes)
+ */
+ MethodVector* getEndNodes();
+
+ /**
+ A helper function for generating and check all sequential histories. Before calling this function, initialize an empty
+ MethodList , and pass it as curList. Also pass the size of the method
+ list as the numLiveNodes.
+
+ If you only want to stop the checking process when finding one failed
+ history, pass true to stopOnFailure.
+ */
+ bool checkAllHistoriesHelper(MethodList *curList, int &numLiveNodes, int
+ &historyNum, bool stopOnFailure, bool verbose);
+
+
+ /** Check whether a specific history is correct */
+ bool checkHistory(MethodList *history, int historyIndex, bool verbose = false);
+
+ /** Generate one random topological sorting */
+ MethodList* generateOneRandomHistory();
+
+ /**
+ The helper function to generate one random topological sorting
+ */
+ void generateOneRandomHistoryHelper(MethodList
+ *curList, int &numLiveNodes);
+
+ /** Return the fake nodes -- START & END */
+ Method getStartMethod();
+ Method getFinishMethod();
+
+ /** Whether method call node m is a fake node */
+ inline bool isFakeMethod(Method m) {
+ return isStartMethod(m) || isFinishMethod(m);
+ }
+
+ /** Whether method call node m is a starting node */
+ inline bool isStartMethod(Method m) {
+ return m->name == GRAPH_START;
+ }
+
+ /** Whether method call node m is a finish node */
+ inline bool isFinishMethod(Method m) {
+ return m->name == GRAPH_FINISH;
+ }
+
+ /**
+ Print out the ordering points and dynamic calling info (return value &
+ arguments).
+ */
+ void printMethodInfo(Method m, bool verbose);
+
+ /** Clear the states of the method call */
+ void clearStates();
+
+ /**
+ Check the state specifications (PreCondition & PostCondition & state
+ transition and evaluation) based on the graph (called after
+ admissibility check). The verbose option controls whether we print a
+ detailed list of checking functions that we have called
+ */
+ bool checkStateSpec(MethodList *history, bool verbose, int historyNum);
+
+ /**
+ Check the justifying subhistory with respect to history of m.
+ */
+ bool checkJustifyingSubhistory(MethodList *subhistory, Method cur,
+ bool verbose, int historyIndex);
+
+ /** Print a problematic thread list */
+ void printActions(action_list_t *actions, const char *header = "The problematic thread list:");
+
+ /** Print one jusifying subhistory of method call cur */
+ void printOneSubhistory(MethodList *history, Method cur,
+ CSTR header);
+};
+
+#endif
diff --git a/spec-analysis/include/specannotation-api.h b/spec-analysis/include/specannotation-api.h
new file mode 100644
index 0000000..aee4196
--- /dev/null
+++ b/spec-analysis/include/specannotation-api.h
@@ -0,0 +1,38 @@
+#ifndef _SPECANNOTATION_API_H
+#define _SPECANNOTATION_API_H
+
+#define NEW_SIZE(type, size) (type*) malloc(size)
+#define NEW(type) NEW_SIZE(type, sizeof(type))
+
+struct MethodCall;
+typedef struct MethodCall *Method;
+typedef const char *CSTR;
+
+struct AnnoInterfaceInfo;
+typedef struct AnnoInterfaceInfo AnnoInterfaceInfo;
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+struct AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name);
+
+void _setInterfaceBeginAnnotationValue(struct AnnoInterfaceInfo *info, void *value);
+
+void _createInterfaceEndAnnotation(CSTR name);
+
+void _createOPDefineAnnotation();
+
+void _createPotentialOPAnnotation(CSTR label);
+
+void _createOPCheckAnnotation(CSTR label);
+
+void _createOPClearAnnotation();
+
+void _createOPClearDefineAnnotation();
+
+#ifdef __cplusplus
+};
+#endif
+
+#endif
diff --git a/spec-analysis/methodcall.cc b/spec-analysis/methodcall.cc
new file mode 100644
index 0000000..84c35ba
--- /dev/null
+++ b/spec-analysis/methodcall.cc
@@ -0,0 +1,125 @@
+#include <algorithm>
+#include "common.h"
+#include "threads-model.h"
+#include "methodcall.h"
+#include "spec_common.h"
+
+CSTR GRAPH_START = "START_NODE";
+CSTR GRAPH_FINISH = "FINISH_NODE";
+
+const unsigned int METHOD_ID_MAX = 0xffffffff;
+const unsigned int METHOD_ID_MIN = 0;
+
+MethodCall::MethodCall(CSTR name, void *value, ModelAction *begin) :
+ name(name), value(value), prev(new SnapSet<Method>), next(new
+ SnapSet<Method>), concurrent(new SnapSet<Method>), justifiedMethod(NULL),
+ justified(false), end(NULL), orderingPoints(new action_list_t), allPrev(new
+ SnapSet<Method>), allNext(new SnapSet<Method>), exist(true) {
+ if (name == GRAPH_START) {
+ this->begin = NULL;
+ id = METHOD_ID_MIN;
+ tid = 1; // Considered to be the main thread
+ } else if (name == GRAPH_FINISH) {
+ this->begin = NULL;
+ id = METHOD_ID_MAX;
+ tid = 1; // Considered to be the main thread
+ } else {
+ this->begin = begin;
+ ASSERT (begin);
+ id = begin->get_seq_number();
+ tid = id_to_int(begin->get_tid());
+ }
+}
+
+void MethodCall::addPrev(Method m) { prev->insert(m); }
+
+void MethodCall::addNext(Method m) { next->insert(m); }
+
+void MethodCall::addConcurrent(Method m) { concurrent->insert(m); }
+
+void MethodCall::addOrderingPoint(ModelAction *act) {
+ bool hasIt = orderingPoints->end() != std::find(orderingPoints->begin(),
+ orderingPoints->end(), act);
+ if (!hasIt)
+ orderingPoints->push_back(act);
+}
+
+
+bool MethodCall::before(Method another) {
+ return belong(allNext, another);
+}
+
+bool MethodCall::belong(MethodSet s, Method m) {
+ return s->end() != std::find(s->begin(), s->end(), m);
+}
+
+bool MethodCall::identical(MethodSet s1, MethodSet s2) {
+ if (s1->size() != s2->size())
+ return false;
+ SnapSet<Method>::iterator it;
+ for (it = s1->begin(); it != s1->end(); it++) {
+ Method m1 = *it;
+ if (belong(s2, m1))
+ return false;
+ }
+ return true;
+}
+
+/**
+ Put the union of src and dest to dest.
+*/
+void MethodCall::Union(MethodSet dest, MethodSet src) {
+ SnapSet<Method>::iterator it;
+ for (it = src->begin(); it != src->end(); it++) {
+ Method m = *it;
+ dest->insert(m);
+ }
+}
+
+MethodSet MethodCall::intersection(MethodSet s1, MethodSet s2) {
+ MethodSet res = new SnapSet<Method>;
+ SnapSet<Method>::iterator it;
+ for (it = s1->begin(); it != s1->end(); it++) {
+ Method m = *it;
+ if (belong(s2, m))
+ res->insert(m);
+ }
+ return res;
+}
+
+bool MethodCall::disjoint(MethodSet s1, MethodSet s2) {
+ SnapSet<Method>::iterator it;
+ for (it = s1->begin(); it != s1->end(); it++) {
+ Method m = *it;
+ if (belong(s2, m))
+ return false;
+ }
+ return true;
+}
+
+void MethodCall::print(bool printOP, bool breakAtEnd) {
+ if (name == GRAPH_START) {
+ model_print("%s", GRAPH_START);
+ if (breakAtEnd)
+ model_print("\n");
+ return;
+ }
+ if (name == GRAPH_FINISH) {
+ model_print("%s", GRAPH_FINISH);
+ if (breakAtEnd)
+ model_print("\n");
+ return;
+ }
+ model_print("%u.%s(T%d)", id, name, id_to_int(begin->get_tid()));
+ if (breakAtEnd)
+ model_print("\n");
+ if (!printOP)
+ return;
+ int i = 1;
+ for (action_list_t::iterator it = orderingPoints->begin(); it !=
+ orderingPoints->end(); it++) {
+ ModelAction *op = *it;
+ model_print("\t-> %d. ", i++);
+ op->print();
+ }
+}
diff --git a/spec-analysis/methodcall.h b/spec-analysis/methodcall.h
new file mode 100644
index 0000000..a88b651
--- /dev/null
+++ b/spec-analysis/methodcall.h
@@ -0,0 +1,114 @@
+#ifndef _METHODCALL_H
+#define _METHODCALL_H
+
+#include "stl-model.h"
+#include "action.h"
+#include "spec_common.h"
+
+class MethodCall;
+
+typedef MethodCall *Method;
+typedef SnapSet<Method> *MethodSet;
+typedef SnapList<ModelAction *> action_list_t;
+
+typedef SnapList<Method> MethodList;
+typedef SnapVector<Method> MethodVector;
+typedef SnapVector<MethodList*> MethodListVector;
+
+/**
+ This is the core class on which the whole checking process will be
+ executing. With the original execution (with the raw annotation
+ information), we construct an execution graph whose nodes represent method
+ calls, and whose edges represent the hb/SC relation between the ordering
+ points of method calls. In that graph, the MethodCall class acts as the node
+ that contains the core information for checking --- the name of the
+ interface, the value (return value and arguments), the state of the current
+ method call, and a set of previous, next and concurrent method calls.
+
+ Plus, this class contains extra info about the ordering points, a set of all
+ method calls that are hb/SC before me (for evaluating the state), and also
+ some other helping internal member variable for generating checking schemes.
+*/
+class MethodCall {
+ public:
+ unsigned int id; // The method call id (the seq_num of the begin action)
+ int tid; // The thread id
+ CSTR name; // The interface label name
+ void *value; // The pointer that points to the struct that have the return
+ // value and the arguments
+ void *state; // The pointer that points to the struct that represents
+ // the state
+ MethodSet prev; // Method calls that are hb right before me
+ MethodSet next; // Method calls that are hb right after me
+ MethodSet concurrent; // Method calls that are concurrent with me
+
+ Method justifiedMethod; // The method before me and is not concurrent with
+ // any other mehtods in my allPrev set
+
+ /**
+ This indicates if the non-deterministic behaviors of this method call
+ has been justified by any of its justifying subhistory. If so, we do not
+ need to check on its justifying subhistory. Initially it is false.
+ */
+ bool justified;
+
+ MethodCall(CSTR name, void *value = NULL, ModelAction *begin = NULL);
+
+ void addPrev(Method m);
+
+ void addNext(Method m);
+
+ void addConcurrent(Method m);
+
+ void addOrderingPoint(ModelAction *act);
+
+ bool before(Method another);
+
+ static bool belong(MethodSet s, Method m);
+
+ static bool identical(MethodSet s1, MethodSet s2);
+
+ /** Put the union of src and dest to dest */
+ static void Union(MethodSet dest, MethodSet src);
+
+ static MethodSet intersection(MethodSet s1, MethodSet s2);
+
+ static bool disjoint(MethodSet s1, MethodSet s2);
+
+ /**
+ Print the method all name with the seq_num of the begin annotation and
+ its thread id.
+
+ printOP == true -> Add each line with the ordering point operation's
+ print()
+
+ breakAtEnd == true -> Add a line break at the end of the print;
+ otherwise, the print will be a string without line breaker when printOP
+ is false.
+ */
+ void print(bool printOP = true, bool breakAtEnd = true);
+
+ /**
+ FIXME: The end action is not really used or necessary here, maybe we
+ should clean this
+ */
+ ModelAction *begin;
+ ModelAction *end;
+ action_list_t *orderingPoints;
+
+ /**
+ Keep a set of all methods that are hb/SC before&after me to calculate my
+ state
+ */
+ MethodSet allPrev;
+ MethodSet allNext;
+
+ /** Logically exist (for generating all possible topological sortings) */
+ bool exist;
+
+ SNAPSHOTALLOC
+};
+
+
+
+#endif
diff --git a/spec-analysis/spec_common.h b/spec-analysis/spec_common.h
new file mode 100644
index 0000000..b8c3a46
--- /dev/null
+++ b/spec-analysis/spec_common.h
@@ -0,0 +1,47 @@
+#ifndef _SPEC_COMMON_H
+#define _SPEC_COMMON_H
+
+#include <set>
+#include <stdlib.h>
+#include "mymemory.h"
+
+/** Comment this out if you don't want unnecessary debugging printing out */
+#define CDSSPEC_DEBUG
+
+#ifdef CDSSPEC_DEBUG
+#define debug_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+#else
+#define debug_print(fmt, ...) do { } while (0)
+#endif
+
+#define SPEC_ANALYSIS 1
+
+/** Null function pointer */
+#define NULL_FUNC NULL
+
+#define NEW_SIZE(type, size) (type*) malloc(size)
+#define NEW(type) NEW_SIZE(type, sizeof(type))
+
+#define EQ(str1, str2) (strcmp(str1, str2) == 0)
+
+extern const unsigned int METHOD_ID_MAX;
+extern const unsigned int METHOD_ID_MIN;
+
+typedef const char *CSTR;
+
+extern CSTR GRAPH_START;
+extern CSTR GRAPH_FINISH;
+
+/** Define a snapshotting set for CDSChecker backend analysis */
+template<typename _Tp>
+class SnapSet : public std::set<_Tp, std::less<_Tp>, SnapshotAlloc<_Tp> >
+{
+ public:
+ typedef std::set<_Tp, std::less<_Tp>, SnapshotAlloc<_Tp> > set;
+
+ SnapSet() : set() { }
+
+ SNAPSHOTALLOC
+};
+
+#endif
diff --git a/spec-analysis/specanalysis.cc b/spec-analysis/specanalysis.cc
new file mode 100644
index 0000000..e5a1f2c
--- /dev/null
+++ b/spec-analysis/specanalysis.cc
@@ -0,0 +1,226 @@
+#include "specanalysis.h"
+#include "action.h"
+#include "cyclegraph.h"
+#include "threads-model.h"
+#include "clockvector.h"
+#include "execution.h"
+#include <sys/time.h>
+#include <assert.h>
+#include "modeltypes.h"
+#include "executiongraph.h"
+
+
+SPECAnalysis::SPECAnalysis()
+{
+ execution = NULL;
+ stats = (struct spec_stats*) model_calloc(1, sizeof(struct spec_stats));
+ print_always = false;
+ print_inadmissible = true;
+ quiet = false;
+ checkCyclic = false;
+ stopOnFail = false;
+ checkRandomNum = 0;
+}
+
+SPECAnalysis::~SPECAnalysis() {
+}
+
+void SPECAnalysis::setExecution(ModelExecution * execution) {
+ this->execution = execution;
+}
+
+const char * SPECAnalysis::name() {
+ const char * name = "SPEC";
+ return name;
+}
+
+void SPECAnalysis::finish() {
+ model_print("\n");
+ model_print(">>>>>>>> SPECAnalysis finished <<<<<<<<\n");
+
+ model_print("Total execution checked: %d\n", stats->bugfreeCnt);
+ model_print("Detected by CDSChecker: %d\n", stats->buggyCnt);
+ model_print("Broken graph: %d\n", stats->brokenCnt);
+ model_print("Cyclic graph: %d\n", stats->cyclicCnt);
+ model_print("Inadmissible executions: %d\n", stats->inadmissibilityCnt);
+ model_print("Failed executions: %d\n", stats->failedCnt);
+
+ if (stats->cyclicCnt > 0 && checkCyclic) {
+ model_print("Warning: You have cycle in your execution graphs.\n");
+ }
+
+ if (stats->failedCnt == 0) {
+ model_print("Yay! All executions have passed the specification.\n");
+ if (stats->brokenCnt > 0)
+ model_print("However! You have executions with a broken graph.\n");
+ if (stats->cyclicCnt > 0) {
+ model_print("Warning: You have cyclic execution graphs!\n");
+ if (checkCyclic) {
+ model_print("Make sure that's what you expect.\n");
+ }
+ }
+ if (stats->inadmissibilityCnt > 0)
+ model_print("However! You have inadmissible executions.\n");
+ if (stats->noOrderingPointCnt > 0 && print_always)
+ model_print("You have execution graphs that have no ordering points.\n");
+
+ }
+}
+
+bool SPECAnalysis::isCheckRandomHistories(char *opt, int &num) {
+ char *p = opt;
+ bool res = false;
+ if (*p == 'c') {
+ p++;
+ if (*p == 'h') {
+ p++;
+ if (*p == 'e') {
+ p++;
+ if (*p == 'c') {
+ p++;
+ if (*p == 'k') {
+ res = true;
+ p++;
+ }
+ }
+ }
+ }
+ }
+ if (res) {
+ // p now should point to '-'
+ if (*p == '-') {
+ p++;
+ num = atoi(p);
+ if (num > 0)
+ return true;
+ }
+ return false;
+ }
+ return res;
+}
+
+bool SPECAnalysis::option(char * opt) {
+ if (strcmp(opt, "verbose")==0) {
+ print_always=true;
+ return false;
+ } else if (strcmp(opt, "no-admissible")==0) {
+ print_inadmissible = false;
+ return false;
+ } else if (strcmp(opt, "quiet")==0) {
+ quiet = true;
+ return false;
+ } else if (strcmp(opt, "check-cyclic") == 0) {
+ checkCyclic = true;
+ return false;
+ } else if (strcmp(opt, "stop-on-fail")==0) {
+ stopOnFail = true;
+ return false;
+ } else if (isCheckRandomHistories(opt, checkRandomNum)) {
+ return false;
+ } else if (strcmp(opt, "help") != 0) {
+ model_print("Unrecognized option: %s\n", opt);
+ }
+
+ model_print("SPEC Analysis options\n"
+ "By default SPEC outputs the graphs of those failed execution\n"
+ "verbose -- print graphs of any traces\n"
+ "quiet -- do not print out graphs\n"
+ "inadmissible-quiet -- print the inadmissible\n"
+ "check-one -- only check one random possible topological"
+ "sortings (check all possible by default)\n"
+ );
+ model_print("\n");
+
+ return true;
+}
+
+void SPECAnalysis::analyze(action_list_t *actions) {
+ /* Count the number traces */
+ stats->traceCnt++;
+ if (execution->have_bug_reports()) {
+ /* Count the number traces */
+ stats->buggyCnt++;
+ return;
+ }
+
+ /* Count the number bug-free traces */
+ stats->bugfreeCnt++;
+
+ // FIXME: Make checkCyclic false by default
+ ExecutionGraph *graph = new ExecutionGraph(execution, checkCyclic);
+ graph->buildGraph(actions);
+ if (graph->isBroken()) {
+ stats->brokenCnt++;
+ if (print_always && !quiet) { // By default not printing
+ model_print("Execution #%d has a broken graph.\n\n",
+ execution->get_execution_number());
+ }
+ return;
+ }
+
+ if (print_always) {
+ model_print("------------------ Checking execution #%d"
+ " ------------------\n", execution->get_execution_number());
+ }
+
+ // Count how many executions that have no-ordering-point method calls
+ if (graph->isNoOrderingPoint()) {
+ stats->noOrderingPointCnt++;
+ }
+
+ if (!graph->checkAdmissibility()) {
+ /* One more inadmissible trace */
+ stats->inadmissibilityCnt++;
+ if (print_inadmissible && !quiet) {
+ model_print("Execution #%d is NOT admissible\n",
+ execution->get_execution_number());
+ graph->print();
+ if (print_always)
+ graph->printAllMethodInfo(true);
+ }
+ return;
+ }
+
+ bool pass = false;
+ if (graph->hasCycle()) {
+ /* One more trace with a cycle */
+ stats->cyclicCnt++;
+ if (!checkCyclic) {
+ if (!quiet)
+ graph->print();
+ if (print_always && !quiet) { // By default not printing
+ model_print("Execution #%d has a cyclic graph.\n\n",
+ execution->get_execution_number());
+ }
+ } else {
+ if (print_always && !quiet) {
+ model_print("Checking cyclic execution #%d...\n",
+ execution->get_execution_number());
+ }
+ pass = graph->checkCyclicGraphSpec(print_always && !quiet);
+ }
+ } else if (checkRandomNum > 0) { // Only a few random histories
+ if (print_always && !quiet)
+ model_print("Check %d random histories...\n", checkRandomNum);
+ pass = graph->checkRandomHistories(checkRandomNum, true, print_always && !quiet);
+ } else { // Check all histories
+ if (print_always && !quiet)
+ model_print("Check all histories...\n");
+ pass = graph->checkAllHistories(true, print_always && !quiet);
+ }
+
+ if (!pass) {
+ /* One more failed trace */
+ stats->failedCnt++;
+ model_print("Execution #%d failed.\n\n",
+ execution->get_execution_number());
+ } else {
+ /* One more passing trace */
+ stats->passCnt++;
+
+ if (print_always && !quiet) { // By default not printing
+ model_print("Execution #%d passed.\n\n",
+ execution->get_execution_number());
+ }
+ }
+}
diff --git a/spec-analysis/specanalysis.h b/spec-analysis/specanalysis.h
new file mode 100644
index 0000000..1c77156
--- /dev/null
+++ b/spec-analysis/specanalysis.h
@@ -0,0 +1,77 @@
+#ifndef _SPECANALYSIS_H
+#define _SPECANALYSIS_H
+
+#include <stack>
+
+#include "traceanalysis.h"
+#include "mymemory.h"
+#include "modeltypes.h"
+#include "action.h"
+
+struct spec_stats {
+ /** The number of traces that have passed the checking */
+ unsigned passCnt;
+
+ /** The number of inadmissible traces */
+ unsigned inadmissibilityCnt;
+
+ /** The number of all checked traces */
+ unsigned traceCnt;
+
+ /** The number of traces with a cyclic graph */
+ unsigned cyclicCnt;
+
+ /** The number of traces with broken graphs */
+ unsigned brokenCnt;
+
+ /** The number of traces with graphs that has no ordering points */
+ unsigned noOrderingPointCnt;
+
+ /** The number of traces that failed */
+ unsigned failedCnt;
+
+ /** The number of buggy and bug-free traces (by CDSChecker) */
+ unsigned buggyCnt;
+ unsigned bugfreeCnt;
+};
+
+class SPECAnalysis : public TraceAnalysis {
+ public:
+ SPECAnalysis();
+ ~SPECAnalysis();
+
+ virtual void setExecution(ModelExecution * execution);
+ virtual void analyze(action_list_t *actions);
+ virtual const char * name();
+ virtual bool option(char *);
+ virtual void finish();
+
+ /** Some stats */
+ spec_stats *stats;
+
+ SNAPSHOTALLOC
+ private:
+ /** The execution */
+ ModelExecution *execution;
+
+ /** A few useful options */
+ /* Print out the graphs of all executions */
+ bool print_always;
+ /* Print out the graphs of the inadmissible traces */
+ bool print_inadmissible;
+ /* Never print out the graphs of any traces */
+ bool quiet;
+ /* Whether we still want to check cyclic executions */
+ bool checkCyclic;
+ /* Stop checking when seeing one failed history */
+ bool stopOnFail;
+ /* The number of random histories to be checked; If 0, we check all possible
+ * histories */
+ int checkRandomNum;
+
+ /** Whether this is a "check-12" like option */
+ bool isCheckRandomHistories(char *opt, int &num);
+};
+
+
+#endif
diff --git a/spec-analysis/specannotation.cc b/spec-analysis/specannotation.cc
new file mode 100644
index 0000000..84a9795
--- /dev/null
+++ b/spec-analysis/specannotation.cc
@@ -0,0 +1,96 @@
+#include <algorithm>
+#include "specannotation.h"
+#include "cdsannotate.h"
+
+/********** Annotations **********/
+
+SpecAnnotation::SpecAnnotation(SpecAnnoType type, const void *anno) : type(type),
+ annotation(anno) { }
+
+
+CommutativityRule::CommutativityRule(CSTR method1, CSTR method2, CSTR rule,
+ CheckCommutativity_t condition) : method1(method1),
+ method2(method2), rule(rule), condition(condition) {}
+
+bool CommutativityRule::isRightRule(Method m1, Method m2) {
+ return (m1->name == method1 && m2->name == method2) ||
+ (m1->name == method2 && m2->name == method1);
+}
+
+bool CommutativityRule::checkCondition(Method m1, Method m2) {
+ if (m1->name == method1 && m2->name == method2)
+ return (*condition)(m1, m2);
+ else if (m1->name == method2 && m2->name == method1)
+ return (*condition)(m2, m1);
+ else // The checking should only be called on the right rule
+ ASSERT(false);
+ return false;
+}
+
+NamedFunction::NamedFunction(CSTR name, CheckFunctionType type, void *function) : name(name),
+ type(type), function(function) { }
+
+StateFunctions::StateFunctions(NamedFunction *transition, NamedFunction
+ *preCondition, NamedFunction * justifyingPrecondition,
+ NamedFunction *justifyingPostcondition,
+ NamedFunction *postCondition, NamedFunction *print) : transition(transition),
+ preCondition(preCondition), justifyingPrecondition(justifyingPrecondition),
+ justifyingPostcondition(justifyingPostcondition),
+ postCondition(postCondition), print(print) { }
+
+
+AnnoInit::AnnoInit(NamedFunction *initial, NamedFunction *final, NamedFunction
+ *copy, NamedFunction *clear, NamedFunction *printState, CommutativityRule
+ *commuteRules, int ruleNum) : initial(initial), final(final), copy(copy),
+ clear(clear), printState(printState), commuteRules(commuteRules),
+ commuteRuleNum(ruleNum)
+{
+ funcMap = new StateFuncMap;
+}
+
+
+void AnnoInit::addInterfaceFunctions(CSTR name, StateFunctions *funcs) {
+ funcMap->put(name, funcs);
+}
+
+AnnoInterfaceInfo::AnnoInterfaceInfo(CSTR name) : name(name), value(NULL) { }
+
+
+/********** Universal functions for rewriting the program **********/
+
+AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name) {
+ AnnoInterfaceInfo *info = new AnnoInterfaceInfo(name);
+ // Create and instrument with the INTERFACE_BEGIN annotation
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_BEGIN, info));
+ return info;
+}
+
+void _createInterfaceEndAnnotation(CSTR name) {
+ // Create and instrument with the INTERFACE_END annotation
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_END, (void*) name));
+}
+
+
+void _setInterfaceBeginAnnotationValue(AnnoInterfaceInfo *info, void *value) {
+ info->value = value;
+}
+
+void _createOPDefineAnnotation() {
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_DEFINE, NULL));
+}
+
+void _createPotentialOPAnnotation(CSTR label) {
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(POTENTIAL_OP, label));
+}
+
+void _createOPCheckAnnotation(CSTR label) {
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CHECK, label));
+}
+
+void _createOPClearAnnotation() {
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR, NULL));
+}
+
+void _createOPClearDefineAnnotation() {
+ cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR_DEFINE, NULL));
+}
diff --git a/spec-analysis/specannotation.h b/spec-analysis/specannotation.h
new file mode 100644
index 0000000..5ab80ef
--- /dev/null
+++ b/spec-analysis/specannotation.h
@@ -0,0 +1,230 @@
+#ifndef _SPECANNOTATION_H
+#define _SPECANNOTATION_H
+
+#include "modeltypes.h"
+#include "model-assert.h"
+#include "methodcall.h"
+#include "action.h"
+#include "spec_common.h"
+#include "hashtable.h"
+
+using namespace std;
+
+/**
+ We can only pass a void* pointer from the real program execution to the
+ checking engine, so we need to wrap the key information into that pointer.
+ We use the SpecAnntotation struct to represent that info. Different types
+ here mean different annotations.
+
+ FIXME: Currently we actually do not need to have the INTERFACE_END types. We
+ basically wrap the MethodCall* pointer of the method call in the
+ INTERFACE_BEGIN type of annotation.
+*/
+typedef enum SpecAnnoType {
+ INIT, POTENTIAL_OP, OP_DEFINE, OP_CHECK, OP_CLEAR, OP_CLEAR_DEFINE,
+ INTERFACE_BEGIN, INTERFACE_END
+} SpecAnnoType;
+
+inline CSTR specAnnoType2Str(SpecAnnoType type) {
+ switch (type) {
+ case INIT:
+ return "INIT";
+ case POTENTIAL_OP:
+ return "POTENTIAL_OP";
+ case OP_DEFINE:
+ return "OP_DEFINE";
+ case OP_CHECK:
+ return "OP_CHECK";
+ case OP_CLEAR:
+ return "OP_CLEAR";
+ case OP_CLEAR_DEFINE:
+ return "OP_CLEAR_DEFINE";
+ case INTERFACE_BEGIN:
+ return "INTERFACE_BEGIN";
+ case INTERFACE_END:
+ return "INTERFACE_END";
+ default:
+ return "UNKNOWN_TYPE";
+ }
+}
+
+typedef
+struct SpecAnnotation {
+ SpecAnnoType type;
+ const void *annotation;
+
+ SpecAnnotation(SpecAnnoType type, const void *anno);
+
+} SpecAnnotation;
+
+typedef bool (*CheckCommutativity_t)(Method, Method);
+/**
+ The first method is the target (to update its state), and the second method
+ is the method that should be executed (to access its method call info (ret
+ & args)
+*/
+typedef bool (*StateTransition_t)(Method, Method);
+typedef bool (*CheckState_t)(Method, Method);
+typedef void (*UpdateState_t)(Method);
+// Copy the second state to the first state
+typedef void (*CopyState_t)(Method, Method);
+
+/**
+ This struct contains a commutativity rule: two method calls represented by
+ two unique integers and a function that takes two "info" pointers (with the
+ return value and the arguments) and returns a boolean to represent whether
+ the two method calls are commutable.
+*/
+typedef
+struct CommutativityRule {
+ CSTR method1;
+ CSTR method2;
+
+ /** The plain text of the rule (debugging purpose) */
+ CSTR rule;
+ CheckCommutativity_t condition;
+
+ CommutativityRule(CSTR method1, CSTR method2, CSTR rule,
+ CheckCommutativity_t condition);
+
+ bool isRightRule(Method m1, Method m2);
+
+ bool checkCondition(Method m1, Method m2);
+
+} CommutativityRule;
+
+typedef enum CheckFunctionType {
+ INITIAL, COPY, CLEAR, FINAL, PRINT_STATE, TRANSITION, PRE_CONDITION,
+ JUSTIFYING_PRECONDITION, SIDE_EFFECT, JUSTIFYING_POSTCONDITION,
+ POST_CONDITION, PRINT_VALUE
+} CheckFunctionType;
+
+typedef struct NamedFunction {
+ CSTR name;
+ CheckFunctionType type;
+ void *function;
+
+ /**
+ StateTransition_t transition;
+ CheckState_t preCondition;
+ CheckState_t postCondition;
+ */
+ NamedFunction(CSTR name, CheckFunctionType type, void *function);
+} NamedFunction;
+
+typedef
+struct StateFunctions {
+ NamedFunction *transition;
+ NamedFunction *preCondition;
+ NamedFunction *justifyingPrecondition;
+ NamedFunction *justifyingPostcondition;
+ NamedFunction *postCondition;
+ NamedFunction *print;
+
+ StateFunctions(NamedFunction *transition, NamedFunction *preCondition,
+ NamedFunction *justifyingPrecondition,
+ NamedFunction *justifyingPostcondition,
+ NamedFunction *postCondition, NamedFunction *print);
+
+} StateFunctions;
+
+/** A map from a constant c-string to its set of checking functions */
+typedef HashTable<CSTR, StateFunctions*, uintptr_t, 4, malloc, calloc, free > StateFuncMap;
+
+typedef
+struct AnnoInit {
+ /**
+ For the initialization of a state; We actually assume there are two
+ special nodes --- INITIAL & FINAL. They actually have a special
+ MethodCall class representing these two nodes, and their interface name
+ would be INITIAL and FINAL. For the initial function, we actually also
+ use it as the state copy function when evaluating the state of other
+ method calls
+
+ UpdateState_t --> initial
+ */
+ NamedFunction *initial;
+
+ /**
+ TODO: Currently we just have this "final" field, which was supposed to
+ be a final checking function after all method call nodes have been
+ executed on the graph. However, before we think it through, this might
+ potentially be a violation of composability
+
+ CheckState_t --> final;
+ */
+ NamedFunction *final;
+
+ /**
+ For copying out an existing state from a previous method call
+
+ CopyState_t --> copy
+ */
+ NamedFunction *copy;
+
+ /**
+ For clearing out an existing state object
+
+ UpdateState_t --> delete
+ */
+ NamedFunction *clear;
+
+
+ /**
+ For printing out the state
+
+ UpdateState_t --> printState
+ */
+ NamedFunction *printState;
+
+ /** For the state functions. We can conveniently access to the set of state
+ * functions with a hashmap */
+ StateFuncMap *funcMap;
+
+ /** For commutativity rules */
+ CommutativityRule *commuteRules;
+ int commuteRuleNum;
+
+ AnnoInit(NamedFunction *initial, NamedFunction *final, NamedFunction *copy,
+ NamedFunction *clear, NamedFunction *printState, CommutativityRule
+ *commuteRules, int ruleNum);
+
+ void addInterfaceFunctions(CSTR name, StateFunctions *funcs);
+
+} AnnoInit;
+
+typedef
+struct AnnoInterfaceInfo {
+ CSTR name;
+ void *value;
+
+ AnnoInterfaceInfo(CSTR name);
+} AnnoInterfaceInfo;
+
+/********** Universal functions for rewriting the program **********/
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name);
+
+void _createInterfaceEndAnnotation(CSTR name);
+
+void _setInterfaceBeginAnnotationValue(AnnoInterfaceInfo *info, void *value);
+
+void _createOPDefineAnnotation();
+
+void _createPotentialOPAnnotation(CSTR label);
+
+void _createOPCheckAnnotation(CSTR label);
+
+void _createOPClearAnnotation();
+
+void _createOPClearDefineAnnotation();
+
+#ifdef __cplusplus
+};
+#endif
+
+#endif
diff --git a/test/Makefile b/test/Makefile
index 9d7acb0..8f19b46 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -11,13 +11,14 @@ include $(DIR)/Makefile
DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
CPPFLAGS += -I$(BASE) -I$(BASE)/include
+CFLAGS += -I$(BASE) -I$(BASE)/include
all: $(OBJECTS)
-include $(DEPS)
%.o: %.c
- $(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
+ $(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CFLAGS) -L$(BASE) -l$(LIB_NAME)
%.o: %.cc
$(CXX) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
diff --git a/test/iriw.cc b/test/iriw.cc
deleted file mode 100644
index fddbf1a..0000000
--- a/test/iriw.cc
+++ /dev/null
@@ -1,66 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4; /* "local" variables */
-
-static void a(void *obj)
-{
- x.store(1, memory_order_seq_cst);
-}
-
-static void b(void *obj)
-{
- y.store(1, memory_order_seq_cst);
-}
-
-static void c(void *obj)
-{
- r1 = x.load(memory_order_acquire);
- r2 = y.load(memory_order_seq_cst);
-}
-
-static void d(void *obj)
-{
- r3 = y.load(memory_order_acquire);
- r4 = x.load(memory_order_seq_cst);
-}
-
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 4 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
- thrd_create(&t3, (thrd_start_t)&c, NULL);
- thrd_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- /*
- * This condition should not be hit if the execution is SC */
- bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
- printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4);
- MODEL_ASSERT(!sc);
- return 0;
-}
diff --git a/test/iriw_wildcard.cc b/test/iriw_wildcard.cc
deleted file mode 100644
index 5c52455..0000000
--- a/test/iriw_wildcard.cc
+++ /dev/null
@@ -1,66 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4; /* "local" variables */
-
-static void a(void *obj)
-{
- x.store(1, wildcard(1));
-}
-
-static void b(void *obj)
-{
- y.store(1, wildcard(2));
-}
-
-static void c(void *obj)
-{
- r1 = x.load(wildcard(3));
- r2 = y.load(wildcard(4));
-}
-
-static void d(void *obj)
-{
- r3 = y.load(wildcard(5));
- r4 = x.load(wildcard(6));
-}
-
-
-int user_main(int argc, char **argv)
-{
- thrd_t t1, t2, t3, t4;
-
- atomic_init(&x, 0);
- atomic_init(&y, 0);
-
- printf("Main thread: creating 4 threads\n");
- thrd_create(&t1, (thrd_start_t)&a, NULL);
- thrd_create(&t2, (thrd_start_t)&b, NULL);
- thrd_create(&t3, (thrd_start_t)&c, NULL);
- thrd_create(&t4, (thrd_start_t)&d, NULL);
-
- thrd_join(t1);
- thrd_join(t2);
- thrd_join(t3);
- thrd_join(t4);
- printf("Main thread is finished\n");
-
- /*
- * This condition should not be hit if the execution is SC */
- bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
- //MODEL_ASSERT(!sc);
-
- return 0;
-}
diff --git a/threads.cc b/threads.cc
index a06af84..a0bc029 100644
--- a/threads.cc
+++ b/threads.cc
@@ -16,13 +16,13 @@
/** Allocate a stack for a new thread. */
static void * stack_allocate(size_t size)
{
- return Thread_malloc(size);
+ return snapshot_malloc(size);
}
/** Free a stack for a terminated thread. */
static void stack_free(void *stack)
{
- Thread_free(stack);
+ snapshot_free(stack);
}
/**
diff --git a/traceanalysis.h b/traceanalysis.h
index d363150..df3356a 100644
--- a/traceanalysis.h
+++ b/traceanalysis.h
@@ -2,7 +2,6 @@
#define TRACE_ANALYSIS_H
#include "model.h"
-
class TraceAnalysis {
public:
/** setExecution is called once after installation with a reference to
@@ -31,20 +30,6 @@ 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