diff --git a/CMakeLists.txt b/CMakeLists.txt
index 21b7fc7d12c9c4e222e2ff15cfb3d00e42621de6..8e802acf57c6522e83c2c2089ed664366bac8556 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -33,7 +33,7 @@ if(NOT SPOT_LIBRARY)
ExternalProject_Add(SpotLibrary
PREFIX ${SPOT_DIR}
- URL http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz
+ URL http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz
DOWNLOAD_NO_PROGRESS YES
CONFIGURE_COMMAND ./configure --disable-doxygen --disable-python --enable-silent-rules --silent --prefix=<INSTALL_DIR>
BUILD_COMMAND make -j
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 83c235be5cc7ea52273993026ae53d157ec56658..f9035aa890d8a99c54455d89d0feee68da0191e8 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -122,11 +122,9 @@ void *MCHybridSOG::doCompute()
{
int min_charge=1;
int id_thread;
-
- pthread_mutex_lock ( &m_mutex );
+
id_thread=m_id_thread++;
- pthread_mutex_unlock ( &m_mutex );
-
+
unsigned char Identif[20];
m_Terminated=false;
@@ -160,16 +158,7 @@ void *MCHybridSOG::doCompute()
//cout<<"Initial marking is sent"<<endl;
m_graph->insertSHA ( c );
memcpy ( c->m_SHA2,Identif,16 );
- // MDD initialstate=Complete_meta_state;
-
- //pthread_spin_lock(&m_spin_md5);
- //pthread_spin_unlock(&m_spin_md5);
- //write_to_dot("reduced.dot",Reduced);
- //pthread_spin_unlock(&m_spin_md5);
- //#ifndef
-// if (strcmp(red,'C')==0)
-
- initialstate=Canonize ( Complete_meta_state,0 );
+ initialstate=Canonize ( Complete_meta_state,0 );
//#endif // REDUCE
convert_wholemdd_stringcpp ( initialstate,*chaine );
@@ -231,17 +220,10 @@ void *MCHybridSOG::doCompute()
else {
if ( !m_st[id_thread].empty() || !m_msg[id_thread].empty() ) {
- pthread_mutex_lock ( &m_spin_working );
- m_working++;
- pthread_mutex_unlock ( &m_spin_working );
-
- if ( id_thread>1 ) {
- pthread_mutex_lock ( &m_supervise_gc_mutex );
- m_gc++;
- if ( m_gc==1 ) {
+ if ( id_thread>1 ) {
+ if ( ++m_gc==1 ) {
pthread_mutex_lock ( &m_gc_mutex );
- }
- pthread_mutex_unlock ( &m_supervise_gc_mutex );
+ }
}
if ( !m_st[id_thread].empty() ) {
@@ -309,17 +291,19 @@ void *MCHybridSOG::doCompute()
reached_class->setProcess ( destination );
if ( destination==task_id ) {
// cout << " construction local de l'aggregat " <<endl;
- pthread_mutex_lock ( &m_graph_mutex );
+
LDDState* pos=m_graph->find ( reached_class );
if ( !pos ) {
reached_class->setDiv ( Set_Div ( ldd_reachedclass ) );
reached_class->setDeadLock ( Set_Bloc ( ldd_reachedclass ) );
m_graph->insert ( reached_class );
+ pthread_mutex_lock ( &m_graph_mutex );
memcpy ( reached_class->m_SHA2,Identif,16 );
- pthread_mutex_unlock ( &m_graph_mutex );
- m_graph->addArc();
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 ) );
+ pthread_mutex_unlock ( &m_graph_mutex );
+ m_graph->addArc();
+
Set fire=firable_obs ( ldd_reachedclass );
min_charge=minCharge();
@@ -332,10 +316,12 @@ void *MCHybridSOG::doCompute()
//pthread_mutex_unlock(&m_spin_charge);
// cout<<" I'm local destination "<<task_id<< " thread "<< id_thread<< " msg "<< msg<<endl;
} else {
- pthread_mutex_unlock ( &m_graph_mutex );
+
m_graph->addArc();
+ pthread_mutex_lock ( &m_graph_mutex );
e.first.first->Successors.insert ( e.first.first->Successors.begin(),LDDEdge ( pos,t ) );
pos->Predecessors.insert ( pos->Predecessors.begin(),LDDEdge ( e.first.first,t ) );
+ pthread_mutex_unlock ( &m_graph_mutex );
delete reached_class;
}
@@ -445,16 +431,12 @@ void *MCHybridSOG::doCompute()
}
if ( id_thread>1 ) {
- pthread_mutex_lock ( &m_supervise_gc_mutex );
- m_gc--;
- if ( m_gc==0 ) {
+ if ( --m_gc==0 ) {
pthread_mutex_unlock ( &m_gc_mutex );
}
- pthread_mutex_unlock ( &m_supervise_gc_mutex );
+
}
- pthread_mutex_lock ( &m_spin_working );
- m_working--;
- pthread_mutex_unlock ( &m_spin_working );
+
} // End while (m_msg[id_thread].size()>0 || m_st[id_thread].size()>0);
@@ -612,21 +594,16 @@ void MCHybridSOG::computeDSOG ( LDDGraph &g )
//pthread_barrier_init(&m_barrier1, 0, m_nb_thread);
//pthread_barrier_init(&m_barrier2, 0, m_nb_thread);
- pthread_mutex_init ( &m_mutex, NULL );
+
pthread_mutex_init ( &m_graph_mutex,NULL );
pthread_mutex_init ( &m_gc_mutex,NULL );
- pthread_mutex_init ( &m_supervise_gc_mutex,NULL );
m_gc=0;
pthread_spin_init ( &m_spin_md5,0 );
pthread_mutex_init ( &m_spin_working,0 );
- m_working=0;
-
-
+
for ( int i=0; i<m_nb_thread; i++ ) {
pthread_mutex_init ( &m_spin_stack[i], 0 );
- pthread_mutex_init ( &m_spin_msg[i], 0 );
-
-
+ pthread_mutex_init ( &m_spin_msg[i], 0 );
}
timespec start, finish;
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index f41218b0938aa3366e9bdf46efb07998b6ff56bd..eeb491ceb41951e56a1a7ab017a98339ee15b849 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -31,6 +31,9 @@
#include <chrono>
#include "CommonSOG.h"
#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -106,20 +109,19 @@ private:
/// receive state message
void read_state_message();
- /// send state message
void send_state_message();
- int m_nb_thread;
+ uint8_t m_nb_thread;
pthread_t m_list_thread[128];
- int m_id_thread;
+ atomic<uint8_t> m_id_thread;
/// Mutex declaration
- pthread_mutex_t m_mutex;
+
pthread_mutex_t m_graph_mutex;
pthread_mutex_t m_gc_mutex;
- pthread_mutex_t m_supervise_gc_mutex;
- unsigned int m_gc;
+
+ atomic<uint8_t> m_gc;
pthread_mutex_t m_mutex_stack[128];
pthread_mutex_t m_spin_stack[128];
@@ -127,7 +129,7 @@ private:
// pthread_mutex_t m_spin_charge;
pthread_spinlock_t m_spin_md5;
pthread_mutex_t m_spin_working;
- unsigned int m_working = 0;
+
// unsigned int m_count_thread_working;
bool m_Terminated = false;
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index 69af2039d3b6be2e1be3ad14caff030f45e46e66..c756b69a27eb522eff4c54fe0c0940b662f2ea7e 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -25,8 +25,23 @@ ModelCheckBaseMT::~ModelCheckBaseMT()
}
+void ModelCheckBaseMT::buildSucc ( LDDState *agregate )
+{
+ if ( !agregate->isVisited() ) {
+ agregate->setVisited();
+ std::unique_lock<std::mutex> lk ( m_mutexBuild );
+ m_condBuild.wait(lk,[&agregate]{return agregate->isCompletedSucc();});
+ lk.unlock();
+ }
+}
-
+LDDState* ModelCheckBaseMT::getInitialMetaState()
+{
+ while ( !m_finish_initial);
+ LDDState *initial_metastate = m_graph->getInitialState();
+ buildSucc(initial_metastate);
+ return initial_metastate;
+}
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
index d6dbd4cc30231fc7a25a5f9d7fac1cd90fe07c57..9388975e89c71dc969b985e2418d7a02d7862547 100644
--- a/src/ModelCheckBaseMT.h
+++ b/src/ModelCheckBaseMT.h
@@ -1,17 +1,22 @@
#ifndef MODELCHECKBASEMT_H
#define MODELCHECKBASEMT_H
#include "CommonSOG.h"
+#include <mutex>
+#include <condition_variable>
class ModelCheckBaseMT : public CommonSOG {
public:
ModelCheckBaseMT(const NewNet &R,int nbThread);
- virtual LDDState * getInitialMetaState()=0;
- virtual void buildSucc(LDDState *agregate)=0;
+ virtual LDDState * getInitialMetaState();
+ virtual void buildSucc(LDDState *agregate);
void loadNet();
virtual ~ModelCheckBaseMT();
protected:
- int m_nb_thread;
+ uint8_t m_nb_thread;
+ std::condition_variable m_condBuild;
+ bool m_finish_initial=false;
private:
- virtual void preConfigure()=0;
+ virtual void preConfigure()=0;
+ std::mutex m_mutexBuild;
};
#endif
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index 1b540b48da9477cbf35446669b70968a762e36a9..447af879e14b704d95e137906168ef73e5676741 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -5,7 +5,7 @@ class ModelCheckLace : public ModelCheckBaseMT {
public:
ModelCheckLace(const NewNet &R,int nbThread);
LDDState * getInitialMetaState() override;
- void buildSucc(LDDState *agregate) override;
+ void buildSucc(LDDState *agregate) override;
private:
void preConfigure();
bool m_built_initial=false;
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index dbf2c0cba200dbf3e83506d49e4bf4b698a94f69..67ba245d437b79c1c84107542e22213c2fb46205 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -95,25 +95,6 @@ void ModelCheckerTh::preConfigure() {
}
-LDDState* ModelCheckerTh::getInitialMetaState() {
- while (!m_finish_initial) ;
- LDDState *initial_metastate = m_graph->getInitialState();
- if (!initial_metastate->isVisited()) {
- initial_metastate->setVisited();
- while (!initial_metastate->isCompletedSucc())
- ;
- }
- return initial_metastate;
-}
-
-void ModelCheckerTh::buildSucc(LDDState *agregate) {
- if (!agregate->isVisited()) {
- agregate->setVisited();
- while (!agregate->isCompletedSucc())
- ;
- }
-}
-
void* ModelCheckerTh::Compute_successors() {
int id_thread;
id_thread = m_id_thread++;
@@ -206,7 +187,7 @@ void* ModelCheckerTh::Compute_successors() {
}
#endif
}
- e.first.first->setCompletedSucc();
+ e.first.first->setCompletedSucc();m_condBuild.notify_one();
}
m_terminaison[id_thread] = true;
} while (isNotTerminated() && !m_finish);
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index 9cd8cc500253c63f184de2aa29479fa06bf7830b..6ad3b9084c46576eaf6a451a257f130318fe5129 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -5,14 +5,12 @@
#include <mutex>
typedef pair<LDDState *, int> couple_th;
typedef stack<pair<LDDState *,int>> pile_t;
-
+#define MAXT 64
class ModelCheckerTh : public ModelCheckBaseMT
{
public:
ModelCheckerTh(const NewNet &R,int nbThread);
- ~ModelCheckerTh();
- LDDState * getInitialMetaState();
- void buildSucc(LDDState *agregate);
+ ~ModelCheckerTh();
static void *threadHandler(void *context);
void *Compute_successors();
void ComputeTh_Succ();
@@ -20,9 +18,9 @@ private:
void preConfigure();
bool isNotTerminated();
uint8_t minCharge();
- pile m_st[128];
- int m_charge[128];
- bool m_terminaison[128];
+ pile m_st[MAXT];
+ int m_charge[MAXT];
+ bool m_terminaison[MAXT];
atomic<uint8_t> m_id_thread;
std::mutex m_graph_mutex;
pthread_mutex_t m_gc_mutex;
@@ -30,8 +28,7 @@ private:
#ifdef GCENABLE
atomic<uint8_t> m_gc;
#endif
- volatile bool m_finish=false;
- bool m_finish_initial=false;
+ volatile bool m_finish=false;
pthread_mutex_t m_mutex_stack[128];
pthread_t m_list_thread[128];
pthread_spinlock_t m_spin_stack[128];
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 8c900027da85ff70b82fcc7facdb45c0e1235438..aab18aad56ca017476f03bbe42b51195bc4e1d88 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/src/ModelCheckerThV2.cpp
@@ -100,23 +100,8 @@ void ModelCheckerThV2::preConfigure()
}
-LDDState* ModelCheckerThV2::getInitialMetaState()
-{
- while ( !m_finish_initial ) ;
- LDDState *initial_metastate = m_graph->getInitialState();
- buildSucc(initial_metastate);
- return initial_metastate;
-}
-void ModelCheckerThV2::buildSucc ( LDDState *agregate )
-{
- if ( !agregate->isVisited() ) {
- agregate->setVisited();
- std::unique_lock<std::mutex> lk ( m_mutexStack );
- m_condBuild.wait(lk,[&agregate]{return agregate->isCompletedSucc();});
- lk.unlock();
- }
-}
+
void ModelCheckerThV2::Compute_successors()
{
@@ -182,8 +167,7 @@ void ModelCheckerThV2::Compute_successors()
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();
-
+ m_graph_mutex.unlock();
}
}
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
index ff0ada167db6927e45e106be601fe39d1c6e72f8..e6993625bb0311cf94b922b7c1ad16ea82da2f7b 100644
--- a/src/ModelCheckerThV2.h
+++ b/src/ModelCheckerThV2.h
@@ -15,22 +15,19 @@ class ModelCheckerThV2 : public ModelCheckBaseMT
public:
ModelCheckerThV2(const NewNet &R,int nbThread);
~ModelCheckerThV2();
- LDDState * getInitialMetaState();
- void buildSucc(LDDState *agregate);
static void threadHandler(void *context);
void Compute_successors();
void ComputeTh_Succ();
private:
void preConfigure();
bool hasToProcess() const;
- SafeDequeue<Pair> m_common_stack;
-
+ SafeDequeue<Pair> m_common_stack;
atomic<uint8_t> m_id_thread;
- std::mutex m_mutex,m_graph_mutex,m_gc_mutex,m_supervise_gc_mutex;
+ std::mutex m_mutex,m_graph_mutex,m_gc_mutex;
pthread_barrier_t m_barrier_builder;
volatile bool m_finish=false;
- bool m_finish_initial=false;
- std::condition_variable m_condStack,m_condBuild;
+
+ std::condition_variable m_condStack;
std::mutex m_mutexStack;
thread* m_list_thread[128];
};
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index d1c9d5a874d55846b4a908dc56eec361edb66c4b..5ded412ecf09ab85a412391f4e68c971e3c9a3d6 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -13,67 +13,109 @@
// VVVV RRRR RRRR RRRm | DDDD DDDD DDDc VVVV (big endian)
// Ensure our mddnode is 16 bytes
-typedef char __lddmc_check_mddnode_t_is_16_bytes[(sizeof(struct mddnode)==16) ? 1 : -1];
+typedef char __lddmc_check_mddnode_t_is_16_bytes[ ( sizeof ( struct mddnode ) ==16 ) ? 1 : -1];
-static const uint64_t CACHE_FIRING_LACE = (57LL<<40);
+static const uint64_t CACHE_FIRING_LACE = ( 57LL<<40 );
#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
-TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
-
- if (cmark == lddmc_true) return lddmc_true;
- if (minus == lddmc_false) return lddmc_false;
- if (plus == lddmc_false) return lddmc_false;
-
+TASK_IMPL_3 ( MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD,plus ) {
+
+ if ( cmark == lddmc_true ) return lddmc_true;
+ if ( minus == lddmc_false ) return lddmc_false;
+ if ( plus == lddmc_false ) return lddmc_false;
+
MDD result;
- if (cache_get3(CACHE_FIRING_LACE, cmark, minus, plus, &result)) {
- printf("cached\n");
- sylvan_stats_count(CACHE_FIRING_LACE);
+ if ( cache_get3 ( CACHE_FIRING_LACE, cmark, minus, plus, &result ) ) {
+ printf ( "cached\n" );
+ sylvan_stats_count ( CACHE_FIRING_LACE );
return result;
- }
+ }
+
+ mddnode_t n_cmark = GETNODE ( cmark );
+ mddnode_t n_plus = GETNODE ( plus );
+ mddnode_t n_minus = GETNODE ( minus );
+
- mddnode_t n_cmark = GETNODE(cmark);
- mddnode_t n_plus = GETNODE(plus);
- mddnode_t n_minus = GETNODE(minus);
-
-
//lddmc_refs_pushptr(&result);
uint32_t count=0;
uint32_t l_values[128];
- for (;;)
- {
+ for ( ;; ) {
uint32_t value;
- value = mddnode_getvalue(n_cmark);
- uint32_t value_minus = mddnode_getvalue(n_minus);
- uint32_t value_plus = mddnode_getvalue(n_plus);
- if (value>=value_minus)
- {
-
- lddmc_refs_spawn(SPAWN(lddmc_firing_lace, mddnode_getdown(n_cmark), mddnode_getdown(n_minus), mddnode_getdown(n_plus)));
+ value = mddnode_getvalue ( n_cmark );
+ uint32_t value_minus = mddnode_getvalue ( n_minus );
+ uint32_t value_plus = mddnode_getvalue ( n_plus );
+ if ( value>=value_minus ) {
+
+ lddmc_refs_spawn ( SPAWN ( lddmc_firing_lace, mddnode_getdown ( n_cmark ), mddnode_getdown ( n_minus ), mddnode_getdown ( n_plus ) ) );
l_values[count]=value-value_minus+value_plus;
- count++;
-
+ count++;
+
+ }
+ cmark = mddnode_getright ( n_cmark );
+ if ( cmark == lddmc_false ) break;
+ n_cmark = GETNODE ( cmark );
}
- cmark = mddnode_getright(n_cmark);
- if (cmark == lddmc_false) break;
- n_cmark = GETNODE(cmark);
- }
-
+
result= lddmc_false;
- while (count--) {
- lddmc_refs_push(result);
- MDD left=lddmc_refs_sync(SYNC(lddmc_firing_lace));
- lddmc_refs_push(left);
+ while ( count-- ) {
+ lddmc_refs_push ( result );
+ MDD left=lddmc_refs_sync ( SYNC ( lddmc_firing_lace ) );
+ lddmc_refs_push ( left );
MDD result2 =
- lddmc_makenode(l_values[count],left, lddmc_false);
- lddmc_refs_push(result2);
- result = lddmc_union( result, result2);
- lddmc_refs_pop(3);
- }
+ lddmc_makenode ( l_values[count],left, lddmc_false );
+ lddmc_refs_push ( result2 );
+ result = lddmc_union ( result, result2 );
+ lddmc_refs_pop ( 3 );
+ }
//lddmc_refs_popptr(1);
- if (cache_put3(CACHE_FIRING_LACE, cmark, minus, plus,result)) sylvan_stats_count(CACHE_FIRING_LACE);
+ if ( cache_put3 ( CACHE_FIRING_LACE, cmark, minus, plus,result ) ) sylvan_stats_count ( CACHE_FIRING_LACE );
return result;
-}
+ }
+MDD ldd_firing_fast ( MDD cmark, MDD minus, MDD plus ) {
+ // for an empty set of source states, or an empty transition relation, return the empty set
+ if ( cmark == lddmc_true ) return lddmc_true;
+ if ( minus == lddmc_false || plus == lddmc_false ) return lddmc_false;
+
+ MDD result;
+ MDD _cmark=cmark, _minus=minus, _plus=plus;
+
+
+ mddnode_t n_cmark = GETNODE ( _cmark );
+ mddnode_t n_plus = GETNODE ( _plus );
+ mddnode_t n_minus = GETNODE ( _minus );
+
+
+ result = lddmc_false;
+ uint16_t depth=0;
+ uint16_t new_ldd[256];
+
+ for ( ; _cmark!=lddmc_false; ) {
+ uint32_t value;
+ value = mddnode_getvalue ( n_cmark );
+ uint32_t value_minus = mddnode_getvalue ( n_minus );
+ uint32_t value_plus = mddnode_getvalue ( n_plus );
+ uint8_t res=1;
+ while ( _cmark!=lddmc_false && _cmark!=lddmc_true && res ) {
+ if ( value>=value_minus ) {
+ //new_ldd=value-value_minus+value_plus;
+ //push ( mddnode_getdown ( n_cmark ), mddnode_getdown ( n_minus ), mddnode_getdown ( n_plus ) );
+ MDD result2 =
+ ldd_makenode ( value-value_minus+value_plus,lddmc_firing_mono ( mddnode_getdown ( n_cmark ), mddnode_getdown ( n_minus ), mddnode_getdown ( n_plus ) ), lddmc_false );
+
+
+ if ( result2!=lddmc_false ) result = lddmc_union_mono ( result, result2 );
+ }
+ else res=0;
+ }
+ if (res) {/* Build LDD and Union*/}
+ cmark = mddnode_getright ( n_cmark );
+ if ( cmark == lddmc_false ) break;
+ n_cmark = GETNODE ( cmark );
+ }
+ //cache_put3(CACHE_LDD_FIRE, cmark, minus, plus, result);
+ return result;
+ }