modifié : src/CMakeLists.txt

	modifié :         src/LDDGraph.cpp
	modifié :         src/LDDGraph.h
	modifié :         src/LDDState.h
	modifié :         src/ModelCheckerThV2.cpp
	modifié :         src/ModelCheckerThV2.h
	nouveau fichier : src/SafeDequeue.cpp
	nouveau fichier : src/SafeDequeue.h
	modifié :         src/stacksafe.cpp
	modifié :         src/stacksafe.h
	modifié :         src/sylvan_sog.c
	modifié :         third-party/sylvan

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

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++;
 }

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);

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;
 };
 

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();
 }
 
+

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];    
 };

src/SafeDequeue.cpp

+/*
+ * <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>;

src/SafeDequeue.h

+/*
+ * <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

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>;
+
 
 
 

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

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;
-}
-*/

sylvan @ 85823305

-Subproject commit f7e4ec329a6accebb76647b7a93a738d379d7528
+Subproject commit 8582330575f48f010f175d9f2da630280f4cdb10