diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4f9320561c5a0e2b75f6d3fb2c3f91bd5bcd9d0a..eb31e4d9f2804f346645b15cafe7d2974802cdc5 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -12,7 +12,7 @@ set(CMAKE_CXX_EXTENSIONS OFF)
# Add compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
#used flags -Og -DNDEBUG
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -Og -DNDEBUG")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -DNDEBUG -funswitch-loops -floop-interchange -floop-unroll-and-jam -fpeel-loops -fpredictive-commoning -fsplit-loops -fsplit-paths -fexpensive-optimizations -fcse-follow-jumps -fthread-jumps -finline-functions -finline-small-functions -findirect-inlining -foptimize-strlen -fpartial-inlining -fexpensive-optimizations -falign-functions -falign-jumps -falign-labels -falign-loops -fcaller-saves -fdelete-null-pointer-checks") #-Og
endif()
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 7d1b4b3f7caee717a848e245c10f3a790e3478ee..e43146644de0486cda224461e004233c6e93adf7 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -40,7 +40,7 @@ public:
}
else {
memcpy(m_id,e.id,16);
- MPI_Send(m_id,16,MPI_BYTE,e.pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
+ MPI_Send(m_id,16,MPI_BYTE,e.pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
MPI_Status status; //int nbytes;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD, &status);
@@ -92,36 +92,26 @@ public:
MPI_Probe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);
MPI_Get_count(&status, MPI_BYTE, &nbytes);
char inmsg[nbytes+1];
- //cout<<"Received bytes : "<<nbytes<<endl;
MPI_Recv(inmsg, nbytes, MPI_BYTE,status.MPI_SOURCE,TAG_ACK_SUCC,MPI_COMM_WORLD, &status);
uint32_t nb_succ;
memcpy(&nb_succ,inmsg,4);
- //cout<<"Number of successors "<<nb_succ<<endl;
indice=4;
- succ_t *succ_elt;
+ succ_t succ_elt;
//printf("List of successors of %.16s\n",m_id);
for (uint32_t i=0;i<nb_succ;i++) {
- succ_elt=new succ_t;
- memcpy(succ_elt->id,inmsg+indice,16);
+ //succ_elt=new succ_t;
+ memcpy(succ_elt.id,inmsg+indice,16);
indice+=16;
- memcpy(&(succ_elt->pcontainer),inmsg+indice,2);
+ memcpy(&(succ_elt.pcontainer),inmsg+indice,2);
indice+=2;
- memcpy(&(succ_elt->transition),inmsg+indice,2);
+ memcpy(&(succ_elt.transition),inmsg+indice,2);
indice+=2;
- succ_elt->_virtual=false;
- m_succ.push_back(*succ_elt);
- delete succ_elt;
+ succ_elt._virtual=false;
+ m_succ.push_back(succ_elt);
+ // delete succ_elt;
}
-
- if (m_div) {
- succ_t el;
- el.id[0]='v';
- el.transition=-1;
- el._virtual=true;
- //cout<<"yep..."<<endl;
- m_succ.push_back(el);
- }
+
if (m_deadlock) {
succ_t el;
el.id[0]='d';
@@ -130,6 +120,17 @@ public:
el.transition=-1;
m_succ.push_back(el);
}
+ if (m_div) {
+ /*succ_t el;
+ el.id[0]='v';
+ el.transition=-1;
+ el._virtual=true;
+ m_succ.push_back(el);*/
+ succ_t el=e;
+ el._virtual=false;
+ el.transition=-1;
+ m_succ.push_back(el);
+ }
}
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index c7f6fd7e3cd5f0ba8fb155fc4f5463f4b253afaf..8af0f1aa2bf9bdac749e48a9a969c83a5c35ed76 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -61,7 +61,7 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
liste_marques[i] =it_places->marking;
}
m_initialMarking=SylvanWrapper::lddmc_cube ( liste_marques,R.places.size() );
- //#ldd_refs_push ( m_initialMarking );
+ //SylvanWrapper::lddmc_refs_push( m_initialMarking );
delete []liste_marques;
// place names
@@ -93,10 +93,10 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
}
MDD _minus=SylvanWrapper::lddmc_cube ( prec,m_nbPlaces );
- //#ldd_refs_push ( _minus );
+ //SylvanWrapper::lddmc_refs_push ( _minus );
MDD _plus=SylvanWrapper::lddmc_cube ( postc,m_nbPlaces );
- //#ldd_refs_push ( _plus );
+ // SylvanWrapper::lddmc_refs_push ( _plus );
m_tb_relation.push_back ( TransSylvan ( _minus,_plus ) );
}
//sylvan_gc_seq();
@@ -130,7 +130,7 @@ void *MCHybridSOG::doCompute()
LDDState *c=new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
c->m_lddstate=Complete_meta_state;
- //#ldd_refs_push ( Complete_meta_state );
+ //SylvanWrapper::lddmc_refs_push ( Complete_meta_state );
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
SylvanWrapper::convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
@@ -229,23 +229,23 @@ void *MCHybridSOG::doCompute()
MDD ldd_reachedclass=Accessible_epsilon ( get_successor ( e.first.second,t ) );
- //#ldd_refs_push ( ldd_reachedclass );
+ // SylvanWrapper::lddmc_refs_push ( ldd_reachedclass );
- if ( id_thread==1 )
+ //if ( id_thread==1 ) {
//displayMDDTableInfo();
- if ( SylvanWrapper::isGCRequired() ) {
- m_gc_mutex.lock();
-#ifdef DEBUG_GC
-
- displayMDDTableInfo();
-#endif // DEBUG_GC
- // sylvan_gc_seq();
-#ifdef DEBUG_GC
-
- displayMDDTableInfo();
-#endif // DEBUG_GC
- m_gc_mutex.unlock();
- }
+ //if ( SylvanWrapper::isGCRequired() ) {
+ // m_gc_mutex.lock();
+//#ifdef DEBUG_GC
+
+ // SylvanWrapper::displayMDDTableInfo();
+//#endif // DEBUG_GC
+ //SylvanWrapper::sylvan_gc_seq();
+//#ifdef DEBUG_GC
+
+ // SylvanWrapper::displayMDDTableInfo();
+//#endif // DEBUG_GC
+ //m_gc_mutex.unlock();
+ // }
//pthread_spin_unlock(&m_spin_md5);
@@ -311,7 +311,7 @@ void *MCHybridSOG::doCompute()
#ifndef REDUCE
reached=Canonize ( ldd_reachedclass,0 );
-//# ldd_refs_push ( ldd_reachedclass );
+ // SylvanWrapper::lddmc_refs_push( reached );
#endif
//MDD Reduced=ldd_reachedclass;
@@ -401,7 +401,7 @@ void *MCHybridSOG::doCompute()
}
-
+ // cout<<"Finnnnnn...."<<endl;
}
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index db2b5c5a644b2a49db8d9ff361044d553c7714af..0251407e2fda74efca7076dc3db9a578a169e16f 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -111,7 +111,7 @@ private:
pthread_spinlock_t m_spin_md5;
- bool m_Terminated = false;
+ volatile bool m_Terminated = false;
unsigned long m_size_mess = 0;
int m_nbsend = 0, m_nbrecv = 0;
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 2517e0566eb01525a6ee7679df45eb9066d73d3e..80b1db9525a9d035a203384e75645b27995408b2 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -145,10 +145,10 @@ void* ModelCheckerTh::Compute_successors() {
reached_class = new LDDState();
reached_class->m_lddstate = reduced_meta;
//pthread_spin_lock(&m_accessible);
-
+ m_graph_mutex.lock();
LDDState *pos = m_graph->find(reached_class);
if (!pos) {
- m_graph_mutex.lock();
+
e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(), LDDEdge(e.first.first, t));
m_graph_mutex.unlock();
@@ -165,7 +165,7 @@ void* ModelCheckerTh::Compute_successors() {
m_charge[min_charge]++;
} else {
//m_graph_mutex.lock();
- m_graph_mutex.lock();
+
e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
m_graph_mutex.unlock();
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 7b09c764d8bb9a01c1a0467b35acd5ac881d577d..74b7e603255476e2ff2a546b56ddbcae3fd85902 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -13,7 +13,7 @@ SogKripkeIteratorTh::SogKripkeIteratorTh ( const LDDState* lddstate, bdd cnd ) :
m_lsucc.push_back ( pair<LDDState*,int> ( &m_deadlock,-1 ) );
}
if ( lddstate->isDiv() ) {
- m_lsucc.push_back ( pair<LDDState*,int> ( &m_div,-1 ) );
+ m_lsucc.push_back ( pair<LDDState*,int> ( (LDDState*)lddstate,-1 ) );
}
}
diff --git a/src/SylvanCacheWrapper.cpp b/src/SylvanCacheWrapper.cpp
index 83680b6dde6bf537993236c159faa4a9d3ca8c95..ebade573860194db1e540cdc001d5e63f0d7b5c3 100644
--- a/src/SylvanCacheWrapper.cpp
+++ b/src/SylvanCacheWrapper.cpp
@@ -133,8 +133,18 @@ int SylvanCacheWrapper::cache_put(uint64_t a, uint64_t b, uint64_t c, uint64_t r
return 1;
}
+void SylvanCacheWrapper::cache_clear()
+{
+ // a bit silly, but this works just fine, and does not require writing 0 everywhere...
+ cache_free();
+ cache_create(m_cache_size, m_cache_max);
+}
-
+void SylvanCacheWrapper::cache_free()
+{
+ munmap(m_cache_table, m_cache_max * sizeof(struct cache_entry));
+ munmap(m_cache_status, m_cache_max * sizeof(uint32_t));
+}
diff --git a/src/SylvanCacheWrapper.h b/src/SylvanCacheWrapper.h
index 3502e6dffc3cfea11d28d7d048e7df861c8dc87b..0e651e286432d22f1224c49822ed9ba90cb4f9bb 100644
--- a/src/SylvanCacheWrapper.h
+++ b/src/SylvanCacheWrapper.h
@@ -74,6 +74,7 @@ public:
static int __attribute__((unused)) cache_put3(uint64_t opid, uint64_t dd, uint64_t d2, uint64_t d3, uint64_t res);
static int cache_put(uint64_t a, uint64_t b, uint64_t c, uint64_t res);
static int cache_get(uint64_t a, uint64_t b, uint64_t c, uint64_t *res);
+ static void cache_clear();
private:
static size_t m_cache_size; // power of 2
static size_t m_cache_max;
@@ -81,6 +82,7 @@ private:
static uint32_t* m_cache_status;
static uint64_t m_next_opid;
static uint64_t cache_hash(uint64_t a, uint64_t b, uint64_t c);
+ static void cache_free();
};
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 7fdfb8e605d032d3cf5e48ceb13fd65d8c791411..77a128120a3eba5614baa37e7dfd60f88e073cb0 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -381,7 +381,6 @@ MDD SylvanWrapper::lddmc_makenode(uint32_t value, MDD ifeq, MDD ifneq) {
if (index == 0) {
/* lddmc_refs_push(ifeq);
lddmc_refs_push(ifneq);*/
-
// sylvan_gc();/*********************************************************************************************/
/*lddmc_refs_pop(1);*/
@@ -634,8 +633,8 @@ MDD SylvanWrapper::lddmc_union_mono(MDD a, MDD b) {
/* Access cache */
MDD result;
- if (SylvanCacheWrapper::cache_get3(CACHE_LDD_UNION, a, b, 0,&result)) {
- // std::cout<<"Cache succeeded!"<<std::endl;
+ if (SylvanCacheWrapper::cache_get3(CACHE_LDD_UNION, a, b, 0, &result)) {
+ // std::cout<<"Cache succeeded!"<<std::endl;
return result;
}
@@ -745,8 +744,7 @@ MDD SylvanWrapper::ldd_divide_internal(MDD a, int current_level, int level) {
if (a == lddmc_true) return lddmc_true;
MDD result;
- if (SylvanCacheWrapper::cache_get3(CACHE_MDD_DIVIDE, a, current_level, level, &result))
- {
+ if (SylvanCacheWrapper::cache_get3(CACHE_MDD_DIVIDE, a, current_level, level, &result)) {
return result;
}
@@ -827,9 +825,9 @@ MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, MDD minus, MDD plus) {
MDD _cmark = cmark, _minus = minus, _plus = plus;
if (SylvanCacheWrapper::cache_get3(CACHE_LDD_FIRE, cmark, minus, plus, &result)) {
- return result;
+ return result;
}
- MDD cache_cmark=cmark;
+ MDD cache_cmark = cmark;
mddnode_t n_cmark = GETNODE(_cmark);
mddnode_t n_plus = GETNODE(_plus);
mddnode_t n_minus = GETNODE(_minus);
@@ -860,18 +858,16 @@ MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, MDD minus, MDD plus) {
}
// so: proj: -2 (end; quantify rest), -1 (end; keep rest), 0 (quantify), 1 (keep)
-MDD SylvanWrapper::lddmc_project( const MDD mdd, const MDD proj)
-{
+MDD SylvanWrapper::lddmc_project(const MDD mdd, const MDD proj) {
if (mdd == lddmc_false) return lddmc_false; // projection of empty is empty
if (mdd == lddmc_true) return lddmc_true; // projection of universe is universe...
mddnode_t p_node = GETNODE(proj);
uint32_t p_val = mddnode_getvalue(p_node);
- if (p_val == (uint32_t)-1) return mdd;
- if (p_val == (uint32_t)-2) return lddmc_true; // because we always end with true.
+ if (p_val == (uint32_t) -1) return mdd;
+ if (p_val == (uint32_t) -2) return lddmc_true; // because we always end with true.
MDD result;
- if (SylvanCacheWrapper::cache_get3(CACHE_MDD_PROJECT, mdd, proj, 0, &result))
- {
+ if (SylvanCacheWrapper::cache_get3(CACHE_MDD_PROJECT, mdd, proj, 0, &result)) {
return result;
}
@@ -879,9 +875,9 @@ MDD SylvanWrapper::lddmc_project( const MDD mdd, const MDD proj)
if (p_val == 1) // keep
{
- MDD down = lddmc_project( mddnode_getdown(n), mddnode_getdown(p_node));
+ MDD down = lddmc_project(mddnode_getdown(n), mddnode_getdown(p_node));
//lddmc_refs_push(down);
- // MDD right = lddmc_refs_sync(SYNC(lddmc_project));
+ // MDD right = lddmc_refs_sync(SYNC(lddmc_project));
//lddmc_refs_pop(1);
result = lddmc_makenode(mddnode_getvalue(n), down, right);
} else // quantify
@@ -889,16 +885,13 @@ MDD SylvanWrapper::lddmc_project( const MDD mdd, const MDD proj)
if (mddnode_getdown(n) == lddmc_true) // assume lowest level
{
result = lddmc_true;
- }
- else
- {
+ } else {
int count = 0;
result = lddmc_false;
- MDD p_down = mddnode_getdown(p_node), _mdd=mdd;
- while (1)
- {
+ MDD p_down = mddnode_getdown(p_node), _mdd = mdd;
+ while (1) {
//lddmc_refs_spawn(SPAWN(lddmc_project, mddnode_getdown(n), p_down));
- MDD down= lddmc_project (mddnode_getdown(n), p_down);
+ MDD down = lddmc_project(mddnode_getdown(n), p_down);
result = lddmc_union_mono(result, down);
count++;
_mdd = mddnode_getright(n);
@@ -915,57 +908,282 @@ MDD SylvanWrapper::lddmc_project( const MDD mdd, const MDD proj)
return result;
}
-int SylvanWrapper::isGCRequired()
-{
- return (m_g_created>llmsset_get_size(m_nodes)/2);
+int SylvanWrapper::isGCRequired() {
+ return (m_g_created > llmsset_get_size(m_nodes) / 2);
}
-void SylvanWrapper::convert_wholemdd_stringcpp(MDD cmark,string &res)
-{
- typedef pair<string,MDD> Pair_stack;
+void SylvanWrapper::convert_wholemdd_stringcpp(MDD cmark, string &res) {
+ typedef pair<string, MDD> Pair_stack;
vector<Pair_stack> local_stack;
- unsigned int compteur=0;
- MDD explore_mdd=cmark;
+ unsigned int compteur = 0;
+ MDD explore_mdd = cmark;
string chaine;
- res=" ";
- local_stack.push_back(Pair_stack(chaine,cmark));
- do
- {
- Pair_stack element=local_stack.back();
- chaine=element.first;
- explore_mdd=element.second;
+ res = " ";
+ local_stack.push_back(Pair_stack(chaine, cmark));
+ do {
+ Pair_stack element = local_stack.back();
+ chaine = element.first;
+ explore_mdd = element.second;
local_stack.pop_back();
compteur++;
- while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true)
- {
+ while (explore_mdd != lddmc_false && explore_mdd != lddmc_true) {
mddnode_t n_val = GETNODE(explore_mdd);
- if (mddnode_getright(n_val)!=lddmc_false)
- {
- local_stack.push_back(Pair_stack(chaine,mddnode_getright(n_val)));
+ if (mddnode_getright(n_val) != lddmc_false) {
+ local_stack.push_back(Pair_stack(chaine, mddnode_getright(n_val)));
}
unsigned int val = mddnode_getvalue(n_val);
- chaine.push_back((unsigned char)(val)+1);
- explore_mdd=mddnode_getdown(n_val);
+ chaine.push_back((unsigned char) (val) + 1);
+ explore_mdd = mddnode_getdown(n_val);
}
/*printchaine(&chaine);printf("\n");*/
- res+=chaine;
- }
- while (local_stack.size()!=0);
+ res += chaine;
+ } while (local_stack.size() != 0);
//delete chaine;
- compteur=(compteur<<1) | 1;
- res[1]=(unsigned char)((compteur>>8)+1);
- res[0]=(unsigned char)(compteur & 255);
+ compteur = (compteur << 1) | 1;
+ res[1] = (unsigned char) ((compteur >> 8) + 1);
+ res[0] = (unsigned char) (compteur & 255);
+
+}
+
+void SylvanWrapper::sylvan_gc_seq() {
+ if (m_g_created > llmsset_get_size(m_nodes) / 1000) {
+ cout<<"Cache executed"<<endl;
+ SylvanCacheWrapper::cache_clear();
+ llmsset_clear_data(m_nodes);
+ ldd_gc_mark_protected();
+ llmsset_destroy_unmarked(m_nodes);
+ sylvan_rehash_all();
+ m_g_created = seq_llmsset_count_marked(m_nodes);
+ }
+}
+
+void SylvanWrapper::sylvan_rehash_all()
+{
+ // clear hash array
+ llmsset_clear_hashes_seq(m_nodes);
+
+ // rehash marked nodes
+ if (llmsset_rehash_seq(m_nodes) != 0) {
+ fprintf(stderr, "sylvan_gc_rehash error: not all nodes could be rehashed!\n");
+ exit(1);
+ }
}
+int SylvanWrapper::llmsset_rehash_seq (llmsset2_t dbs)
+{
+ return llmsset_rehash_par_seq( dbs, 0, dbs->table_size);
+}
+
+int SylvanWrapper::llmsset_rehash_par_seq(llmsset2_t dbs, size_t first, size_t count)
+{
+ if (count > 512) {
+ int bad = llmsset_rehash_par_seq(dbs, first + count/2, count - count/2);
+ return bad + llmsset_rehash_par_seq(dbs, first, count/2);
+ } else {
+ int bad = 0;
+ uint64_t *ptr = dbs->bitmap2 + (first / 64);
+ uint64_t mask = 0x8000000000000000LL >> (first & 63);
+ for (size_t k=0; k<count; k++) {
+ if (*ptr & mask) {
+ if (llmsset_rehash_bucket(dbs, first+k) == 0) bad++;
+ }
+ mask >>= 1;
+ if (mask == 0) {
+ ptr++;
+ mask = 0x8000000000000000LL;
+ }
+ }
+ return bad;
+ }
+}
+
+
+int SylvanWrapper::llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx)
+{
+ const uint64_t * const d_ptr = ((uint64_t*)dbs->data) + 2*d_idx;
+ const uint64_t a = d_ptr[0];
+ const uint64_t b = d_ptr[1];
+
+ uint64_t hash_rehash = 14695981039346656037LLU;
+ const int custom = is_custom_bucket(dbs, d_idx) ? 1 : 0;
+ if (custom) hash_rehash = dbs->hash_cb(a, b, hash_rehash);
+ else hash_rehash = llmsset_hash(a, b, hash_rehash);
+ const uint64_t step = (((hash_rehash >> 20) | 1) << 3);
+ const uint64_t new_v = (hash_rehash & MASK_HASH) | d_idx;
+ int i=0;
+
+ uint64_t idx, last;
+#if LLMSSET_MASK
+ last = idx = hash_rehash & dbs->mask;
+#else
+ last = idx = hash_rehash % dbs->table_size;
+#endif
+
+ for (;;) {
+ volatile uint64_t *bucket = &dbs->table[idx];
+ if (*bucket == 0 && cas(bucket, 0, new_v)) return 1;
+
+ // find next idx on probe sequence
+ idx = (idx & CL_MASK) | ((idx+1) & CL_MASK_R);
+ if (idx == last) {
+ if (++i == *(volatile int16_t*)&dbs->threshold) {
+ // failed to find empty spot in probe sequence
+ // solution: increase probe sequence length...
+ __sync_fetch_and_add(&dbs->threshold, 1);
+ }
+
+ // go to next cache line in probe sequence
+ hash_rehash += step;
+
+#if LLMSSET_MASK
+ last = idx = hash_rehash & dbs->mask;
+#else
+ last = idx = hash_rehash % dbs->table_size;
+#endif
+ }
+ }
+}
+
+
+int SylvanWrapper::is_custom_bucket(const llmsset2_t dbs, uint64_t index)
+{
+ uint64_t *ptr = dbs->bitmapc + (index/64);
+ uint64_t mask = 0x8000000000000000LL >> (index&63);
+ return (*ptr & mask) ? 1 : 0;
+}
+
+
+
+
+
+
+void SylvanWrapper::llmsset_clear_hashes_seq( llmsset2_t dbs)
+{
+ // just reallocate...
+ if (mmap(dbs->table, dbs->max_size * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED, -1, 0) != (void*)-1) {
+#if defined(madvise) && defined(MADV_RANDOM)
+ madvise(dbs->table, sizeof(uint64_t[dbs->max_size]), MADV_RANDOM);
+#endif
+ } else {
+ // reallocate failed... expensive fallback
+ memset(dbs->table, 0, dbs->max_size * 8);
+ }
+}
+
+
+
+void SylvanWrapper::llmsset_destroy_unmarked(llmsset2_t dbs) {
+ if (dbs->destroy_cb == NULL) return; // no custom function
+ llmsset_destroy(dbs, 0, dbs->table_size);
+}
+
+void SylvanWrapper::llmsset_destroy(llmsset2_t dbs, size_t first, size_t count) {
+ if (count > 1024) {
+ size_t split = count / 2;
+ llmsset_destroy(dbs, first, split);
+ llmsset_destroy(dbs, first + split, count - split);
+
+ } else {
+ for (size_t k = first; k < first + count; k++) {
+ volatile uint64_t *ptr2 = dbs->bitmap2 + (k / 64);
+ volatile uint64_t *ptrc = dbs->bitmapc + (k / 64);
+ uint64_t mask = 0x8000000000000000LL >> (k & 63);
+
+// if not marked but is custom
+ if ((*ptr2 & mask) == 0 && (*ptrc & mask)) {
+ uint64_t *d_ptr = ((uint64_t *) dbs->data) + 2 * k;
+ dbs->destroy_cb(d_ptr[0], d_ptr[1]);
+ *ptrc &= ~mask;
+ }
+ }
+ }
+}
+
+
+void SylvanWrapper::llmsset_clear_data(llmsset2_t dbs) {
+ if (mmap(dbs->bitmap1, dbs->max_size / (512 * 8), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED,
+ -1, 0) != (void *) -1) {
+
+ } else {
+
+ memset(dbs->bitmap1, 0, dbs->max_size / (512 * 8));
+ }
+
+ if (mmap(dbs->bitmap2, dbs->max_size / 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS | MAP_FIXED, -1, 0) !=
+ (void *) -1) {
+
+ } else {
+ memset(dbs->bitmap2, 0, dbs->max_size / 8);
+
+ }
+
+ // forbid first two positions (index 0 and 1)
+ dbs->bitmap2[0] = 0xc000000000000000LL;
+ /*LACE_ME;
+ TOGETHER(llmsset_reset_region);*/
+}
+
+void SylvanWrapper::ldd_gc_mark_protected() {
+ ldd_refs_mark_p_par(m_sequentiel_refs->pbegin, m_sequentiel_refs->pcur - m_sequentiel_refs->pbegin);
+ ldd_refs_mark_r_par(m_sequentiel_refs->rbegin, m_sequentiel_refs->rcur - m_sequentiel_refs->rbegin);
+}
+
+void SylvanWrapper::ldd_refs_mark_r_par(MDD *begin, size_t count) {
+ if (count < 32) {
+ while (count) {
+ ldd_gc_mark_rec(*begin++);
+ count--;
+ }
+ } else {
+ ldd_refs_mark_r_par(begin, count / 2);
+ ldd_refs_mark_r_par(begin + (count / 2), count - count / 2);
+
+ }
+}
+
+
+void SylvanWrapper::ldd_refs_mark_p_par(const MDD **begin, size_t count) {
+ if (count < 32) {
+ while (count) {
+ ldd_gc_mark_rec(**(begin++));
+ count--;
+ }
+ } else {
+ ldd_refs_mark_p_par(begin, count / 2);
+ ldd_refs_mark_p_par(begin + (count / 2), count - count / 2);
+
+ }
+}
+
+void SylvanWrapper::ldd_gc_mark_rec(MDD mdd) {
+ if (mdd <= lddmc_true) return;
+
+ if (llmsset_mark(m_nodes, mdd)) {
+ mddnode_t n = LDD_GETNODE(mdd);
+ ldd_gc_mark_rec(mddnode_getright(n));
+ ldd_gc_mark_rec(mddnode_getdown(n));
+
+ }
+}
+
+int SylvanWrapper::llmsset_mark(const llmsset2_t dbs, uint64_t index) {
+ volatile uint64_t *ptr = dbs->bitmap2 + (index / 64);
+ uint64_t mask = 0x8000000000000000LL >> (index & 63);
+ for (;;) {
+ uint64_t v = *ptr;
+ if (v & mask) return 0;
+ if (cas(ptr, v, v | mask)) return 1;
+ }
+}
size_t SylvanWrapper::m_table_min = 0;
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 8251052cc87d87b02f2a97d0ccd700c5c45aa8c5..97aeb28dbe46a65304c5679d6e6e5714105efb4e 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -240,7 +240,24 @@ public:
static MDD lddmc_project( const MDD mdd, const MDD proj);
static int isGCRequired();
static void convert_wholemdd_stringcpp(MDD cmark,std::string &res);
+ static void sylvan_gc_seq();
private:
+ static int is_custom_bucket(const llmsset2_t dbs, uint64_t index);
+ static int llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx);
+ static int llmsset_rehash_seq (llmsset2_t dbs);
+ static int llmsset_rehash_par_seq(llmsset2_t dbs, size_t first, size_t count);
+ static void llmsset_clear_hashes_seq( llmsset2_t dbs);
+ static void sylvan_rehash_all();
+ static void llmsset_destroy(llmsset2_t dbs, size_t first, size_t count);
+ static void llmsset_destroy_unmarked( llmsset2_t dbs);
+ static void llmsset_clear_data(llmsset2_t dbs);
+ static void ldd_gc_mark_protected();
+ static void ldd_refs_mark_p_par( const MDD** begin, size_t count);
+ static void ldd_gc_mark_rec(MDD mdd);
+ static int llmsset_mark(const llmsset2_t dbs, uint64_t index);
+ static void ldd_refs_mark_r_par( MDD* begin, size_t count);
+
+
static llmsset2_t m_nodes;
static size_t m_table_min, m_table_max, m_cache_min, m_cache_max;
static volatile int m_gc;
@@ -255,6 +272,8 @@ private:
static uint32_t m_g_created;
+
+
};
diff --git a/src/main.cpp b/src/main.cpp
index 87dc1b30a3d496d632a3229d820dcf2fbb5c3021..c0948776fb20e0b77aff46c7bee8d21d5d1b86ba 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -382,6 +382,7 @@ int main(int argc, char **argv) {
}*/
}
}
- MPI_Finalize();
+ MPI_Finalize();
+ exit(0);
return (EXIT_SUCCESS);
}