From 6638984b8e5be62d7a972c01d6f91db96c907bbe Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 Mar 2018 12:56:13 +0100 Subject: [PATCH 1/2] fixed an issue in sylvan refiner when not reusing block numbers --- .../InternalSylvanSignatureRefiner.cpp | 36 +++++++++++-------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp index 07c46fc3c..9d47e648e 100644 --- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp @@ -49,7 +49,7 @@ namespace storm { LACE_ME; - nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 1; signatures.resize(nextFreeBlockIndex); // Perform the actual recursive refinement step. @@ -161,6 +161,8 @@ namespace storm { } } + static const uint64_t NO_ELEMENT_MARKER = -1ull; + static uint64_t sylvan_search_or_insert(uint64_t sig, uint64_t previous_block, InternalSylvanSignatureRefinerBase* refiner) { uint64_t hash = sylvan_hash(sig, previous_block); @@ -189,7 +191,7 @@ namespace storm { } pos++; if (pos >= refiner->currentCapacity) pos = 0; - if (++count >= 128) return 0; + if (++count >= 128) return NO_ELEMENT_MARKER; } } @@ -219,11 +221,11 @@ namespace storm { } return sylvan_cube(vars, e.data()); } - + TASK_3(BDD, sylvan_assign_block, BDD, sig, BDD, previous_block, InternalSylvanSignatureRefinerBase*, refiner) { assert(previous_block != mtbdd_false); // if so, incorrect call! - + // maybe do garbage collection sylvan_gc_test(); @@ -232,21 +234,25 @@ namespace storm { sig = (uint64_t)-1; } - // try to claim previous block number - assert(previous_block != sylvan_false); - const uint64_t p_b = CALL(sylvan_decode_block, previous_block); - assert(p_b < refiner->signatures.size()); - - for (;;) { - BDD cur = *(volatile BDD*)&refiner->signatures[p_b]; - if (cur == sig) return previous_block; - if (cur != 0) break; - if (cas(&refiner->signatures[p_b], 0, sig)) return previous_block; + if (refiner->options.reuseBlockNumbers) { + // try to claim previous block number + assert(previous_block != sylvan_false); + const uint64_t p_b = CALL(sylvan_decode_block, previous_block); + assert(p_b < refiner->signatures.size()); + + for (;;) { + BDD cur = *(volatile BDD*)&refiner->signatures[p_b]; + if (cur == sig) return previous_block; + if (cur != 0) break; + if (cas(&refiner->signatures[p_b], 0, sig)) return previous_block; + } } // no previous block number, search or insert uint64_t c; - while ((c = sylvan_search_or_insert(sig, previous_block, refiner)) == 0) CALL(sylvan_grow, refiner); + while ((c = sylvan_search_or_insert(sig, refiner->options.reuseBlockNumbers ? previous_block : sig, refiner)) == NO_ELEMENT_MARKER) { + CALL(sylvan_grow, refiner); + } return CALL(sylvan_encode_block, refiner->blockCube.getInternalBdd().getSylvanBdd().GetBDD(), refiner->numberOfBlockVariables, c); } From ea21aca117f6fef689e7f38f5aab269fe7ae2d8a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 Mar 2018 13:34:19 +0100 Subject: [PATCH 2/2] second attempt at fixing issue when not reusing blocks --- .../InternalSylvanSignatureRefiner.cpp | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp index 9d47e648e..ce14cd837 100644 --- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp @@ -11,13 +11,15 @@ namespace storm { namespace dd { namespace bisimulation { + static const uint64_t NO_ELEMENT_MARKER = -1ull; + InternalSylvanSignatureRefinerBase::InternalSylvanSignatureRefinerBase(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), currentCapacity(1ull << 20), resizeFlag(0) { // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); - table.resize(3 * currentCapacity); + table.resize(3 * currentCapacity, NO_ELEMENT_MARKER); } template @@ -30,13 +32,14 @@ namespace storm { Partition InternalSignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); ++numberOfRefinements; + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); } template void InternalSignatureRefiner::clearCaches() { for (auto& e : this->table) { - e = 0ull; + e = NO_ELEMENT_MARKER; } for (auto& e : this->signatures) { e = 0ull; @@ -49,7 +52,7 @@ namespace storm { LACE_ME; - nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 1; + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; signatures.resize(nextFreeBlockIndex); // Perform the actual recursive refinement step. @@ -142,7 +145,7 @@ namespace storm { uint64_t oldCapacity = refiner->currentCapacity; refiner->currentCapacity <<= 1; - refiner->table = std::vector(3 * refiner->currentCapacity); + refiner->table = std::vector(3 * refiner->currentCapacity, NO_ELEMENT_MARKER); CALL(sylvan_rehash, 0, oldCapacity, refiner); @@ -161,8 +164,6 @@ namespace storm { } } - static const uint64_t NO_ELEMENT_MARKER = -1ull; - static uint64_t sylvan_search_or_insert(uint64_t sig, uint64_t previous_block, InternalSylvanSignatureRefinerBase* refiner) { uint64_t hash = sylvan_hash(sig, previous_block); @@ -175,13 +176,13 @@ namespace storm { ptr = refiner->table.data() + pos*3; a = *ptr; if (a == sig) { - while ((b=ptr[1]) == 0) continue; + while ((b=ptr[1]) == NO_ELEMENT_MARKER) continue; if (b == previous_block) { - while ((c=ptr[2]) == 0) continue; + while ((c=ptr[2]) == NO_ELEMENT_MARKER) continue; return c; } - } else if (a == 0) { - if (cas(ptr, 0, sig)) { + } else if (a == NO_ELEMENT_MARKER) { + if (cas(ptr, NO_ELEMENT_MARKER, sig)) { c = ptr[2] = __sync_fetch_and_add(&refiner->nextFreeBlockIndex, 1); ptr[1] = previous_block; return c; @@ -250,7 +251,7 @@ namespace storm { // no previous block number, search or insert uint64_t c; - while ((c = sylvan_search_or_insert(sig, refiner->options.reuseBlockNumbers ? previous_block : sig, refiner)) == NO_ELEMENT_MARKER) { + while ((c = sylvan_search_or_insert(sig, previous_block, refiner)) == NO_ELEMENT_MARKER) { CALL(sylvan_grow, refiner); }