Commit 64bcc008 authored by Thibault Allançon's avatar Thibault Allançon

mc: bloom_filter: move code out of bitstate.hh

- New bloom filter class (with only Jenkins hash for now)
- Use std::vector<bool> instead of std::bitset to allow dynamic bitset
  size
- Specify memory size with command line option: -H MEM_SIZE

* spot/mc/Makefile.am: add bloom_filter.hh
* spot/mc/bitstate.hh: implementation here
* spot/mc/bloom_filter.hh: implementation here
* spot/mc/mc.hh: modify bitstate wrapper
* tests/ltsmin/modelcheck.cc: specify mem size in CLI
parent 365e60d5
...@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) ...@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc mcdir = $(pkgincludedir)/mc
mc_HEADERS = bitstate.hh reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\ mc_HEADERS = bitstate.hh bloom_filter.hh reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc.hh deadlock.hh bloemen.hh cndfs.hh mc.hh deadlock.hh bloemen.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la noinst_LTLIBRARIES = libmc.la
......
...@@ -19,9 +19,8 @@ ...@@ -19,9 +19,8 @@
#pragma once #pragma once
#include <bitset>
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/mc/bloom_filter.hh>
namespace spot namespace spot
{ {
...@@ -30,8 +29,8 @@ namespace spot ...@@ -30,8 +29,8 @@ namespace spot
class bitstate class bitstate
{ {
public: public:
bitstate(kripkecube<State, SuccIterator>& sys, unsigned tid): bitstate(kripkecube<State, SuccIterator>& sys, uint32_t mem_size):
sys_(sys), tid_(tid) sys_(sys)
{ {
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys), static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value, State, SuccIterator>::value,
...@@ -39,6 +38,7 @@ namespace spot ...@@ -39,6 +38,7 @@ namespace spot
seen_.reserve(2000000); seen_.reserve(2000000);
todo_.reserve(100000); todo_.reserve(100000);
bf_ = std::make_unique<bloom_filter>(mem_size);
} }
~bitstate() ~bitstate()
...@@ -74,28 +74,6 @@ namespace spot ...@@ -74,28 +74,6 @@ namespace spot
return state_number; return state_number;
} }
// Must be a power of two minus 1 (it will be used as a bit mask)
static const unsigned MEM_SIZE = (1 << 30) - 1;
// https://burtleburtle.net/bob/c/lookup3.c
#define rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
uint32_t jenkins_hash(uint32_t k)
{
// Internal states
uint32_t s1, s2;
s1 = s2 = 0xdeadbeef;
s2 ^= s1; s2 -= rot(s1, 14);
k ^= s2; k -= rot(s2, 11);
s1 ^= k; s1 -= rot(k, 25);
s2 ^= s1; s2 -= rot(s1, 16);
k ^= s2; k -= rot(s2, 4);
s1 ^= k; s1 -= rot(k, 14);
s2 ^= s1; s2 -= rot(s1, 24);
return s2 & MEM_SIZE;
}
unsigned int dfs_bitstate_hashing() unsigned int dfs_bitstate_hashing()
{ {
unsigned int state_number = 1; unsigned int state_number = 1;
...@@ -107,16 +85,15 @@ namespace spot ...@@ -107,16 +85,15 @@ namespace spot
{ {
State current = todo_.back(); State current = todo_.back();
todo_.pop_back(); todo_.pop_back();
bs_[jenkins_hash(state_hash(current))] = 1; bf_->insert(state_hash(current));
for (auto it = sys_.succ(current, tid_); !it->done(); it->next()) for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
{ {
auto neighbor = it->state(); auto neighbor = it->state();
auto neighbor_hash = jenkins_hash(state_hash(neighbor)); if (bf_->contains(state_hash(neighbor)) == false)
if (bs_[neighbor_hash] == 0)
{ {
todo_.push_back(neighbor); todo_.push_back(neighbor);
bs_[neighbor_hash] = 1; bf_->insert(state_hash(neighbor));
state_number++; state_number++;
} }
} }
...@@ -131,6 +108,7 @@ namespace spot ...@@ -131,6 +108,7 @@ namespace spot
std::unordered_set<State, StateHash, StateEqual> seen_; std::unordered_set<State, StateHash, StateEqual> seen_;
std::vector<State> todo_; std::vector<State> todo_;
std::bitset<MEM_SIZE> bs_; // TODO: unique_ptr are not thread safe
std::unique_ptr<bloom_filter> bf_;
}; };
} }
// -*- coding: utf-8 -*-
// Copyright (C) 2020 Laboratoire de Recherche et Developpement de
// l'Epita
//
// This file is part of Spot, a model checking library.
//
// Spot 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.
//
// Spot 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/>.
#pragma once
#include <functional>
namespace spot
{
class bloom_filter
{
using hash_t = uint32_t;
using hash_function_t = std::function<hash_t(hash_t)>;
// https://burtleburtle.net/bob/c/lookup3.c
#define rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
static hash_t jenkins_hash_function(hash_t k)
{
hash_t s1, s2;
s1 = s2 = 0xdeadbeef;
s2 ^= s1; s2 -= rot(s1, 14);
k ^= s2; k -= rot(s2, 11);
s1 ^= k; s1 -= rot(k, 25);
s2 ^= s1; s2 -= rot(s1, 16);
k ^= s2; k -= rot(s2, 4);
s1 ^= k; s1 -= rot(k, 14);
s2 ^= s1; s2 -= rot(s1, 24);
return s2;
}
public:
bloom_filter(uint32_t mem_size)
: mem_size_(mem_size)
{
bitset_.assign(mem_size, false);
// Internal hash functions
hash_functions_.push_back(jenkins_hash_function);
}
void insert(hash_t elem)
{
for (const auto& f : hash_functions_)
{
hash_t hash = f(elem) % mem_size_;
bitset_[hash] = true;
}
}
bool contains(hash_t elem)
{
for (const auto& f : hash_functions_)
{
hash_t hash = f(elem) % mem_size_;
if (bitset_[hash] == false)
return false;
}
return true;
}
private:
std::vector<hash_function_t> hash_functions_;
std::vector<bool> bitset_;
uint32_t mem_size_;
};
}
...@@ -27,11 +27,12 @@ ...@@ -27,11 +27,12 @@
#include <utility> #include <utility>
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/mc/bitstate.hh> #include <spot/mc/bitstate.hh>
#include <spot/mc/ec.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/cndfs.hh>
#include <spot/mc/bloemen.hh> #include <spot/mc/bloemen.hh>
#include <spot/mc/bloemen_ec.hh> #include <spot/mc/bloemen_ec.hh>
#include <spot/mc/bloom_filter.hh>
#include <spot/mc/cndfs.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/ec.hh>
#include <spot/misc/common.hh> #include <spot/misc/common.hh>
#include <spot/misc/timer.hh> #include <spot/misc/timer.hh>
...@@ -417,10 +418,10 @@ namespace spot ...@@ -417,10 +418,10 @@ namespace spot
template<typename kripke_ptr, typename State, template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal> typename Iterator, typename Hash, typename Equal>
void bitstate_hashing(kripke_ptr sys) void bitstate_hashing(kripke_ptr sys, uint32_t mem_size)
{ {
using algo_name = spot::bitstate<State, Iterator, Hash, Equal>; using algo_name = spot::bitstate<State, Iterator, Hash, Equal>;
auto s = new algo_name(*sys, 0); auto s = new algo_name(*sys, mem_size);
std::cout << "\nBitstate hashing:\n"; std::cout << "\nBitstate hashing:\n";
std::cout << "DFS: " << s->dfs() << '\n'; std::cout << "DFS: " << s->dfs() << '\n';
......
...@@ -77,7 +77,7 @@ struct mc_options_ ...@@ -77,7 +77,7 @@ struct mc_options_
bool bloemen = false; bool bloemen = false;
bool bloemen_ec = false; bool bloemen_ec = false;
bool cndfs = false; bool cndfs = false;
bool bitstate_hashing = false; unsigned bitstate_mem_size = 0;
} mc_options; } mc_options;
...@@ -127,7 +127,8 @@ parse_opt_finput(int key, char* arg, struct argp_state*) ...@@ -127,7 +127,8 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
mc_options.selfloopize = false; mc_options.selfloopize = false;
break; break;
case 'H': case 'H':
mc_options.bitstate_hashing = true; mc_options.bitstate_mem_size = to_unsigned(arg, "-H/--bitstate-hashing");
break;
case 'k': case 'k':
mc_options.kripke_output = true; mc_options.kripke_output = true;
break; break;
...@@ -201,7 +202,7 @@ static const argp_option options[] = ...@@ -201,7 +202,7 @@ static const argp_option options[] =
{ nullptr, 0, nullptr, 0, "General options:", 5 }, { nullptr, 0, nullptr, 0, "General options:", 5 },
// ------------------------------------------------------------ // ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "Bitstate hashing", 6 }, { nullptr, 0, nullptr, 0, "Bitstate hashing", 6 },
{ "bitstate_hashing", 'H', nullptr, 0, "bitstate hashing", 0 }, { "bitstate_hashing", 'H', "INT", 0, "bitstate hashing memory size", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 } { nullptr, 0, nullptr, 0, nullptr, 0 }
}; };
...@@ -314,7 +315,7 @@ static int checked_main() ...@@ -314,7 +315,7 @@ static int checked_main()
} }
} }
if (mc_options.bitstate_hashing) if (mc_options.bitstate_mem_size != 0)
{ {
tm.start("load kripkecube"); tm.start("load kripkecube");
spot::ltsmin_kripkecube_ptr modelcube = nullptr; spot::ltsmin_kripkecube_ptr modelcube = nullptr;
...@@ -336,7 +337,8 @@ static int checked_main() ...@@ -336,7 +337,8 @@ static int checked_main()
spot::cspins_state, spot::cspins_state,
spot::cspins_iterator, spot::cspins_iterator,
spot::cspins_state_hash, spot::cspins_state_hash,
spot::cspins_state_equal>(modelcube); spot::cspins_state_equal>
(modelcube, mc_options.bitstate_mem_size);
tm.stop("deadlock check"); tm.stop("deadlock check");
memused = spot::memusage() - memused; memused = spot::memusage() - memused;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment