diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cbf7ecbe4c2dff51b7fd521589cd4de86c59af78..2c4427474288d2513d76d55ca80a3d522fdb1ccc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -65,6 +65,8 @@ add_executable(mc-sog main.cpp
ModelCheckerTh.h
stacksafe.cpp
stacksafe.h
+ SafeDequeue.cpp
+ SafeDequeue.h
ModelCheckerThV2.cpp
ModelCheckerThV2.h
MCHybridSOG.cpp
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index eaba61f91f4271dfe4c626036c38da531aac1f10..87d9c6af123025054d66a0988602588d75e10af1 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -22,8 +22,8 @@ LDDState* LDDGraph::getInitialState() const {
/*----------------------find()----------------*/
LDDState * LDDGraph::find(LDDState* c)
{
- for(MetaLDDNodes::const_iterator i=m_GONodes.begin();!(i==m_GONodes.end());i++)
- //if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
+ std::scoped_lock lock(m_mutex);
+ for(MetaLDDNodes::const_iterator i=m_GONodes.begin();!(i==m_GONodes.end());i++)
if(c->m_lddstate==(*i)->m_lddstate)
return *i;
return NULL;
@@ -62,7 +62,7 @@ size_t LDDGraph::findSHAPos(unsigned char* c,bool &res)
/*----------------------insert() ------------*/
void LDDGraph::insert(LDDState *c)
{
-
+ std::scoped_lock lock(m_mutex);
this->m_GONodes.push_back(c);
m_nbStates++;
}
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index f2a562e93190ab7f798521888fee6c8fdd2363e3..533e07fdd4f35c384304b191eba730560a70a0cd 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -2,7 +2,8 @@
#define LDDGRAPH_H
#include "LDDState.h"
#include "CommonSOG.h"
-
+#include <mutex>
+#include <atomic>
//#include "LDDStateExtend.h"
using namespace std;
#include <iostream>
@@ -14,6 +15,7 @@ class CommonSOG;
class LDDGraph
{
private:
+ mutable std::mutex m_mutex;
map<string,uint16_t>* m_transition;
map<uint16_t,string>* m_places;
void printGraph(LDDState *, size_t &);
@@ -31,7 +33,7 @@ class LDDGraph
LDDState *m_currentstate;
long m_nbStates;
long m_nbMarking;
- long m_nbArcs;
+ atomic<uint32_t> m_nbArcs;
LDDState* find(LDDState*);
LDDState* findSHA(unsigned char*);
size_t findSHAPos(unsigned char*,bool &res);
diff --git a/src/LDDState.h b/src/LDDState.h
index 6734ac949b229d5e6e331fc833dd642059a9bff1..a56dbe4afbbed7069e3cfef96a2160b7c7de848f 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -49,7 +49,7 @@ class LDDState {
private:
bool m_virtual = false;
bool m_visited=false;
- bool m_completed=false;
+ volatile bool m_completed=false;
uint16_t m_process=0;
};
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 8a7e0f15c28cde66c4633d5210aac59953c68091..8c900027da85ff70b82fcc7facdb45c0e1235438 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/src/ModelCheckerThV2.cpp
@@ -104,34 +104,29 @@ LDDState* ModelCheckerThV2::getInitialMetaState()
{
while ( !m_finish_initial ) ;
LDDState *initial_metastate = m_graph->getInitialState();
- if ( !initial_metastate->isVisited() ) {
- initial_metastate->setVisited();
- while ( !initial_metastate->isCompletedSucc() )
- ;
- }
+ buildSucc(initial_metastate);
return initial_metastate;
}
void ModelCheckerThV2::buildSucc ( LDDState *agregate )
{
if ( !agregate->isVisited() ) {
- agregate->setVisited();
- while ( !agregate->isCompletedSucc() )
- ;
+ agregate->setVisited();
+ std::unique_lock<std::mutex> lk ( m_mutexStack );
+ m_condBuild.wait(lk,[&agregate]{return agregate->isCompletedSucc();});
+ lk.unlock();
}
}
void ModelCheckerThV2::Compute_successors()
{
int id_thread;
- {
- std::scoped_lock guard ( m_mutex );
- id_thread = m_id_thread++;
- }
+
+ id_thread = m_id_thread++;
+
//cout<<" I'm here thread id " <<m_id_thread<<endl;
- Set fire;
- int min_charge = 0;
- m_started=false;
+ Set fire;
+
if ( id_thread == 0 ) {
LDDState *c = new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
@@ -141,8 +136,7 @@ void ModelCheckerThV2::Compute_successors()
c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
c->setDiv ( Set_Div ( Complete_meta_state ) );
m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
- m_condStack.notify_one();
- m_started=true;
+ m_condStack.notify_one();
m_graph->setInitialState ( c );
m_graph->insert ( c );
m_finish_initial = true;
@@ -151,96 +145,55 @@ void ModelCheckerThV2::Compute_successors()
LDDState *reached_class;
//pthread_barrier_wait ( &m_barrier_builder );
Pair e;
- do {
-
-
+ do {
std::unique_lock<std::mutex> lk ( m_mutexStack );
m_condStack.wait(lk,std::bind(&ModelCheckerThV2::hasToProcess,this));
lk.unlock();
-
- if (!m_finish ) {
- m_terminaison++;
- bool advance=true;
- try {
- m_common_stack.pop ( e );
- } catch ( ... ) {
- advance=false;
- }
-
- if ( advance ) {
+
+ if ( m_common_stack.try_pop ( e ) && !m_finish ) {
while ( !e.second.empty() && !m_finish ) {
int t = *e.second.begin();
e.second.erase ( t );
- if ( id_thread ) {
- std::scoped_lock supervise ( m_supervise_gc_mutex );
- m_gc++;
- if ( m_gc == 1 ) {
- m_gc_mutex.lock();
- }
- }
-
- //MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
- /*ldd_refs_push(reduced_meta);*/
- if ( id_thread == 0 ) {
- std::scoped_lock guard ( m_gc_mutex );
- // #ifdef DEBUG_GC
- //displayMDDTableInfo();
- // #endif // DEBUG_GC
- sylvan_gc_seq();
- // #ifdef DEBUG_GC
- //displayMDDTableInfo();
- // #endif // DEBUG_GC
- }
-
- //pthread_spin_lock(&m_accessible);
-
+
MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
ldd_refs_push ( reduced_meta );
reached_class = new LDDState();
- reached_class->m_lddstate = reduced_meta;
- m_graph_mutex.lock();
+ reached_class->m_lddstate = reduced_meta;
LDDState *pos = m_graph->find ( reached_class );
- if ( !pos ) {
- // cout<<"not found"<<endl;
+ if ( !pos ) {
m_graph->addArc();
- m_graph->insert ( reached_class );
- m_graph_mutex.unlock();
- //reached_class->setDiv(Set_Div(reduced_meta));
- //reached_class->setDeadLock(Set_Bloc(reduced_meta));
+ m_graph->insert ( reached_class );
+
fire = firable_obs ( reduced_meta );
reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
reached_class->setDiv ( Set_Div ( reduced_meta ) );
m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
m_condStack.notify_one();
-
+ 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();
} else {
+ delete reached_class;
m_graph->addArc();
- m_graph_mutex.unlock();
+ 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 ) );
- delete reached_class;
- }
- if ( id_thread ) {
- std::scoped_lock guard ( m_supervise_gc_mutex );
- m_gc--;
- if ( m_gc == 0 ) {
- m_gc_mutex.unlock();
- }
-
+ m_graph_mutex.unlock();
+
}
+
}
- e.first.first->setCompletedSucc();
+ e.first.first->setCompletedSucc();m_condBuild.notify_one();
} //end advance
- m_terminaison--;
- }
+
+
} while ( !m_finish );
- pthread_barrier_wait ( &m_barrier_builder );
+ //pthread_barrier_wait ( &m_barrier_builder );
}
@@ -258,10 +211,7 @@ void ModelCheckerThV2::ComputeTh_Succ()
/* pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);*/
pthread_barrier_init ( &m_barrier_builder, NULL, m_nb_thread + 1 );
-
-
- m_gc=0;
- m_terminaison=0;
+
m_finish=false;
for ( int i = 0; i < m_nb_thread; i++ ) {
int rc;
@@ -276,7 +226,7 @@ ModelCheckerThV2::~ModelCheckerThV2()
{
m_finish = true;
m_condStack.notify_all();
- pthread_barrier_wait ( &m_barrier_builder );
+ //pthread_barrier_wait ( &m_barrier_builder );
for ( int i = 0; i < m_nb_thread; i++ ) {
m_list_thread[i]->join();
delete m_list_thread[i];
@@ -287,3 +237,4 @@ bool ModelCheckerThV2::hasToProcess() const {
return m_finish || !m_common_stack.empty();
}
+
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
index 84ec05c648bc106f8ab160896309b549719edeea..ff0ada167db6927e45e106be601fe39d1c6e72f8 100644
--- a/src/ModelCheckerThV2.h
+++ b/src/ModelCheckerThV2.h
@@ -2,6 +2,7 @@
#define MODELCHECKERTHV2_H
#include "ModelCheckBaseMT.h"
#include "stacksafe.h"
+#include "SafeDequeue.h"
#include <atomic>
#include <thread>
#include <mutex>
@@ -21,18 +22,15 @@ public:
void ComputeTh_Succ();
private:
void preConfigure();
- bool ModelCheckerThV2::hasToProcess() const;
-
- StackSafe<Pair> m_common_stack;
- bool m_started=false;
-
- int m_id_thread;
+ bool hasToProcess() const;
+ 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;
- pthread_barrier_t m_barrier_builder;
- atomic<uint32_t> m_gc,m_terminaison; //
+ pthread_barrier_t m_barrier_builder;
volatile bool m_finish=false;
bool m_finish_initial=false;
- std::condition_variable m_condStack;
+ std::condition_variable m_condStack,m_condBuild;
std::mutex m_mutexStack;
thread* m_list_thread[128];
};
diff --git a/src/SafeDequeue.cpp b/src/SafeDequeue.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..fd4b282f2c7cc907dda5cb656d283b130c51e844
--- /dev/null
+++ b/src/SafeDequeue.cpp
@@ -0,0 +1,100 @@
+/*
+ * <one line to give the library's name and an idea of what it does.>
+ * Copyright (C) 2020 chiheb <email>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "SafeDequeue.h"
+
+template<typename T>
+SafeDequeue<T>::SafeDequeue()
+{
+
+}
+
+template<typename T>
+SafeDequeue<T>::SafeDequeue ( const SafeDequeue& other )
+{
+ std::scoped_lock lk ( other.mut );
+ data_queue=other.data_queue;
+}
+
+template<typename T>
+SafeDequeue<T>::~SafeDequeue()
+{
+
+}
+
+template<typename T>
+void SafeDequeue<T>::push ( T new_value )
+{
+ std::scoped_lock lk ( mut );
+ data_queue.push ( new_value );
+ data_cond.notify_one();
+
+}
+
+/*template<typename T>
+void SafeDequeue<T>::wait_and_pop ( T& value )
+{
+
+}*/
+
+template<typename T>
+std::shared_ptr<T> SafeDequeue<T>::wait_and_pop()
+{
+ std::unique_lock<std::mutex> lk ( mut );
+ data_cond.wait ( lk,[this] {return !data_queue.empty();} );
+ std::shared_ptr<T> res ( std::make_shared<T> ( data_queue.front() ) );
+ data_queue.pop();
+ return res;
+}
+
+template<typename T>
+bool SafeDequeue<T>::try_pop ( T& value )
+{
+ std::scoped_lock lk ( mut );
+ if ( data_queue.empty() ) {
+ return false;
+ }
+ value=data_queue.front();
+ data_queue.pop();
+ return true;
+}
+
+
+template<typename T>
+std::shared_ptr<T> SafeDequeue<T>::try_pop()
+{
+ std::scoped_lock lk ( mut );
+ if ( data_queue.empty() ) {
+ return std::shared_ptr<T>();
+ }
+ std::shared_ptr<T> res ( std::make_shared<T> ( data_queue.front() ) );
+ data_queue.pop();
+ return res;
+}
+
+template<typename T>
+bool SafeDequeue<T>::empty() const
+{
+ std::scoped_lock lk ( mut );
+ return data_queue.empty();
+}
+
+
+template class SafeDequeue<Pair>;
+typedef pair<string *, unsigned int> MSG;
+template class SafeDequeue<MSG>;
diff --git a/src/SafeDequeue.h b/src/SafeDequeue.h
new file mode 100644
index 0000000000000000000000000000000000000000..22b983b5f1b410ffaa335c90b2a209ab8933f397
--- /dev/null
+++ b/src/SafeDequeue.h
@@ -0,0 +1,78 @@
+/*
+ * <one line to give the library's name and an idea of what it does.>
+ * Copyright (C) 2020 chiheb <email>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef SAFEDEQUEUE_H
+#define SAFEDEQUEUE_H
+#include <memory>
+#include "LDDState.h"
+#include <queue>
+#include <mutex>
+#include <functional>
+#include <condition_variable>
+
+typedef pair<LDDState *, MDD> couple;
+typedef pair<couple, Set> Pair;
+struct empty_queue: std::exception {
+ ~empty_queue() {};
+ const char* what() const noexcept {return "";}
+
+ };
+/**
+ * @todo write docs
+ */
+template<typename T>
+class SafeDequeue {
+ private:
+ std::mutex mut;
+ std::queue<T> data_queue;
+ std::condition_variable data_cond;
+
+ public:
+ /**
+ * Default constructor
+ */
+ SafeDequeue();
+
+ /**
+ * Copy constructor
+ *
+ * @param other TODO
+ */
+ SafeDequeue ( const SafeDequeue& other );
+
+ /**
+ * Destructor
+ */
+ ~SafeDequeue();
+ SafeDequeue& operator= ( const SafeDequeue& ) = delete;
+ void push ( T new_value );
+ bool try_pop ( T& value );
+ std::shared_ptr<T> try_pop();
+ void wait_and_pop ( T& value ) {
+ std::unique_lock<std::mutex> lk ( mut );
+ data_cond.wait ( lk,[this] {return !data_queue.empty();} );
+ value=data_queue.front();
+ data_queue.pop();
+ };
+
+
+ std::shared_ptr<T> wait_and_pop();
+ bool empty() const;
+ };
+
+#endif // SAFEDEQUEUE_H
diff --git a/src/stacksafe.cpp b/src/stacksafe.cpp
index de7f260f0ef86460ca808ac1f0e59367fd703f3f..6b381d20ab35c959886f279b974c85c50247b55b 100644
--- a/src/stacksafe.cpp
+++ b/src/stacksafe.cpp
@@ -48,16 +48,22 @@ void StackSafe<T>::pop(T& value)
value=m_data.top();
m_data.pop();
}
-
template<typename T>
-bool StackSafe<T>::empty() const
+bool StackSafe<T>::try_pop(T& value)
{
std::scoped_lock lock(m_mutex);
- return m_data.empty();
+ if(m_data.empty()) return false;
+ value=m_data.top();
+ m_data.pop();
+ return true;
}
- template class StackSafe<Pair>;
+
+template class StackSafe<Pair>;
+typedef pair<string *, unsigned int> MSG;
+template class StackSafe<MSG>;
+
diff --git a/src/stacksafe.h b/src/stacksafe.h
index af33910ec32b554ffb4e7b048a53562c5e6e1af8..723cf901259c03bfeebcb79346a8e1d666ead5a8 100644
--- a/src/stacksafe.h
+++ b/src/stacksafe.h
@@ -44,6 +44,10 @@ template<typename T> class StackSafe {
void push ( T new_value );
std::shared_ptr<T> pop();
void pop ( T& value );
- bool empty() const;
+ bool try_pop ( T& value );
+ bool empty() const {
+ std::scoped_lock lock(m_mutex);
+ return m_data.empty();
+ };
};
#endif // STACKSAFE_H
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index 1ed1663c17b1e68e816a2ba8d451ef2f9a3d86e8..d1c9d5a874d55846b4a908dc56eec361edb66c4b 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -77,50 +77,3 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
}
-
-
-/*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);
- return result;
- }
-
- mddnode_t n_cmark = GETNODE(cmark);
- mddnode_t n_plus = GETNODE(plus);
- mddnode_t n_minus = GETNODE(minus);
-
- result= lddmc_false;
- //lddmc_refs_pushptr(&result);
- 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_push(result);
- MDD left=CALL(lddmc_firing_lace, mddnode_getdown(n_cmark), mddnode_getdown(n_minus), mddnode_getdown(n_plus));
- lddmc_refs_push(left);
- MDD result2 =
- lddmc_makenode(value-value_minus+value_plus,left, lddmc_false);
- lddmc_refs_push(result2);
- result = lddmc_union( result, result2);
- lddmc_refs_pop(3);
- }
- cmark = mddnode_getright(n_cmark);
- if (cmark == lddmc_false) break;
- n_cmark = GETNODE(cmark);
- }
- //lddmc_refs_popptr(1);
- if (cache_put3(CACHE_FIRING_LACE, cmark, minus, plus,result)) sylvan_stats_count(CACHE_FIRING_LACE);
- return result;
-}
-*/
diff --git a/third-party/sylvan b/third-party/sylvan
index f7e4ec329a6accebb76647b7a93a738d379d7528..8582330575f48f010f175d9f2da630280f4cdb10 160000
--- a/third-party/sylvan
+++ b/third-party/sylvan
@@ -1 +1 @@
-Subproject commit f7e4ec329a6accebb76647b7a93a738d379d7528
+Subproject commit 8582330575f48f010f175d9f2da630280f4cdb10