🐛 bug fixed in predCP

Author: Moorvan

async/asyncTermSet.cpp

@@ -42,8 +42,7 @@ namespace wamcer {
 
     void AsyncTermSet::pop(smt::Term& term) {
         auto lck = std::unique_lock(mux);
-        // pop one term in data and assign it to term
-        if (size() > 0) {
+        if (!data.empty()) {
             term = *data.begin();
             data.erase(term);
         }

core/runner.cpp

@@ -229,6 +229,7 @@ namespace wamcer {
         }
     }
 
+    // There are bugs in the solver's data for concurrent access.
     bool
     Runner::runPredCP(std::string path,
                       const std::function<void(std::string &, TransitionSystem &, Term &)> &decoder,
@@ -244,7 +245,8 @@ namespace wamcer {
         // pred generation
         auto preds = AsyncTermSet();
         auto predsGen = new DirectConstructor(ts, p, preds, s);
-        predsGen->generatePreds(0, 1);
+        predsGen->generatePreds();
+        logger.log(defines::logPredCP, 1, "Predicates size: {}.", preds.size());
 
         predCP.insert(preds, 0);
         auto threads = std::vector<std::thread>();
@@ -253,15 +255,19 @@ namespace wamcer {
             predCP.propBMC();
         });
         threads.push_back(std::move(t1));
-        for (int i = 0; i < bound; ++i) {
-            auto check = std::thread([&] {
+
+        // pred in pools[k] means that safe in k steps
+        // check 0 - bound-1 pools
+        for (int i = 0; i < bound; i++) {
+            threads.emplace_back([&](int i) {
                 predCP.check(i);
-            });
-            threads.push_back(std::move(check));
-            auto prove = std::thread([&] {
+            }, i);
+        }
+        // prove 1 - bound pools
+        for (int i = 1; i <= bound; ++i) {
+            threads.emplace_back([&](int i) {
                 predCP.prove(i);
-            });
-            threads.push_back(std::move(prove));
+            }, i);
         }
 
         for (auto &t: threads) {

engines/PredCP.cpp

@@ -22,9 +22,12 @@ namespace wamcer {
         if (at >= max_step) {
             return false;
         }
+        auto lock = std::unique_lock<std::mutex>(global_mux);
         auto new_ts = TransitionSystem::copy(ts);
         auto bmc = BMCChecker(new_ts);
+        lock.unlock();
         while (true) {
+            logger.log(defines::logPredCP, 1, "PredCP: check at {}, with pred size: {}", at, preds.size(at));
             while (preds.size(at) == 0) {
                 auto lck = std::unique_lock(mutexes[at]);
                 cvs[at].wait(lck);
@@ -45,15 +48,17 @@ namespace wamcer {
     }
 
     bool PredCP::prove(int at) {
-        if (at >= max_step) {
+        if (at > max_step) {
             return false;
         }
         while (at > cur_step) {
             auto lck = std::unique_lock(prove_wait_mux);
             prove_wait_cv.wait(lck);
         }
+        auto lock = std::unique_lock<std::mutex>(global_mux);
         auto new_ts = TransitionSystem::copy(ts);
         auto prover = InductionProver(new_ts, prop);
+        lock.unlock();
         while (true) {
             {
                 auto lck = std::unique_lock(mutexes[at]);
@@ -78,8 +83,10 @@ namespace wamcer {
     }
 
     void PredCP::propBMC() {
+        auto lock = std::unique_lock<std::mutex>(global_mux);
         auto new_ts = TransitionSystem::copy(ts);
         auto bmc = BMCChecker(new_ts);
+        lock.unlock();
         while (true) {
             if (bmc.check(cur_step + 1, prop)) {
                 logger.log(defines::logPredCP, 1, "propBMC: prop is checked safe at {} step", cur_step + 1);
@@ -93,12 +100,12 @@ namespace wamcer {
         }
     }
 
-    void PredCP::insert(const smt::TermVec& terms, int at) {
+    void PredCP::insert(const smt::TermVec &terms, int at) {
         preds.insert(terms, at);
         cvs[at].notify_all();
     }
 
-    void PredCP::insert(AsyncTermSet& terms, int at) {
+    void PredCP::insert(AsyncTermSet &terms, int at) {
         terms.map([&](const smt::Term &t) {
             preds.insert({t}, at);
         });

engines/PredCP.h

@@ -5,6 +5,7 @@
 #ifndef WAMCER_PREDCP_H
 #define WAMCER_PREDCP_H
 
+#include <atomic>
 #include "async/asyncPreds.h"
 #include "core/unroller.h"
 #include "utils/logger.h"
@@ -27,6 +28,7 @@ namespace wamcer {
         void insert(AsyncTermSet &terms, int at);
 
     private:
+        std::mutex global_mux;
         std::vector<std::mutex> mutexes;
         std::vector<std::condition_variable> cvs;
         std::mutex prove_wait_mux;