Commit 365e60d5 authored by Thibault Allançon's avatar Thibault Allançon

mc: bitstate: add first bitstate hashing experiments

Basic benchmark with DFS and DFS with bitstate hashing (using Jenkins
lookup3 hash function).

* spot/mc/Makefile.am: add bitstate.hh
* spot/mc/bitstate.hh: implementation here
* spot/mc/mc.hh: add bitstate wrapper
* tests/ltsmin/modelcheck.cc: add bitstate CLI
parent 9dbfe13f
......@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc_HEADERS = bitstate.hh reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc.hh deadlock.hh bloemen.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la
......
// -*- 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 <bitset>
#include <spot/kripke/kripke.hh>
namespace spot
{
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class bitstate
{
public:
bitstate(kripkecube<State, SuccIterator>& sys, unsigned tid):
sys_(sys), tid_(tid)
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
seen_.reserve(2000000);
todo_.reserve(100000);
}
~bitstate()
{
// States will be destroyed by the system, so just clear map
seen_.clear();
}
unsigned int dfs()
{
unsigned int state_number = 1;
State initial = sys_.initial(tid_);
todo_.push_back(initial);
while (!todo_.empty())
{
State current = todo_.back();
todo_.pop_back();
seen_.insert(current);
for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
{
auto neighbor = it->state();
if (seen_.count(neighbor) == 0)
{
todo_.push_back(neighbor);
seen_.insert(neighbor);
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 state_number = 1;
State initial = sys_.initial(tid_);
StateHash state_hash;
todo_.push_back(initial);
while (!todo_.empty())
{
State current = todo_.back();
todo_.pop_back();
bs_[jenkins_hash(state_hash(current))] = 1;
for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
{
auto neighbor = it->state();
auto neighbor_hash = jenkins_hash(state_hash(neighbor));
if (bs_[neighbor_hash] == 0)
{
todo_.push_back(neighbor);
bs_[neighbor_hash] = 1;
state_number++;
}
}
}
return state_number;
}
protected:
kripkecube<State, SuccIterator>& sys_;
unsigned int tid_;
std::unordered_set<State, StateHash, StateEqual> seen_;
std::vector<State> todo_;
std::bitset<MEM_SIZE> bs_;
};
}
......@@ -26,6 +26,7 @@
#include <vector>
#include <utility>
#include <spot/kripke/kripke.hh>
#include <spot/mc/bitstate.hh>
#include <spot/mc/ec.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/cndfs.hh>
......@@ -413,4 +414,17 @@ namespace spot
return std::make_tuple(is_empty, trace, stats, tm);
}
template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
void bitstate_hashing(kripke_ptr sys)
{
using algo_name = spot::bitstate<State, Iterator, Hash, Equal>;
auto s = new algo_name(*sys, 0);
std::cout << "\nBitstate hashing:\n";
std::cout << "DFS: " << s->dfs() << '\n';
std::cout << "DFS (bitstate hashing): " << s->dfs_bitstate_hashing() << '\n';
delete s;
}
}
......@@ -77,6 +77,7 @@ struct mc_options_
bool bloemen = false;
bool bloemen_ec = false;
bool cndfs = false;
bool bitstate_hashing = false;
} mc_options;
......@@ -125,6 +126,8 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
mc_options.has_deadlock = true;
mc_options.selfloopize = false;
break;
case 'H':
mc_options.bitstate_hashing = true;
case 'k':
mc_options.kripke_output = true;
break;
......@@ -196,6 +199,10 @@ static const argp_option options[] =
"2 : (faster) assume all values in [0 .. 2^28-1]", 0 },
// ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "General options:", 5 },
// ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "Bitstate hashing", 6 },
{ "bitstate_hashing", 'H', nullptr, 0, "bitstate hashing", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
......@@ -307,6 +314,41 @@ static int checked_main()
}
}
if (mc_options.bitstate_hashing)
{
tm.start("load kripkecube");
spot::ltsmin_kripkecube_ptr modelcube = nullptr;
try
{
modelcube = spot::ltsmin_model::load(mc_options.model)
.kripkecube({}, spot::formula::ff(), mc_options.compress,
mc_options.nb_threads);
}
catch (const std::runtime_error& e)
{
std::cerr << e.what() << '\n';
}
tm.stop("load kripkecube");
int memused = spot::memusage();
tm.start("deadlock check");
spot::bitstate_hashing<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>(modelcube);
tm.stop("deadlock check");
memused = spot::memusage() - memused;
if (!modelcube)
{
exit_code = 2;
goto safe_exit;
}
return 0;
}
if (mc_options.nb_threads == 1 &&
mc_options.formula != nullptr &&
mc_options.model != nullptr &&
......
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