bricks: add bricks for concurrent hashmap

* Makefile.am, README, bricks/brick-assert.h,
bricks/brick-bitlevel.h, bricks/brick-hash.h,
bricks/brick-hashset.h, bricks/brick-shmem.h,
bricks/brick-types.h, configure.ac,
debian/copyright, debian/libspot-dev.install,
m4/bricks.m4, tests/Makefile.am,
tests/core/.gitignore, tests/core/bricks.cc: here.

Makefile.am

@@ -39,6 +39,10 @@ SUBDIRS = picosat buddy lib ltdl spot bin tests $(PYTHON_SUBDIR) $(DOC_SUBDIR) \
 UTF8 = utf8/README.md utf8/utf8.h	\
   utf8/utf8/checked.h utf8/utf8/core.h utf8/utf8/unchecked.h
 
+nobase_include_HEADERS= bricks/brick-assert.h bricks/brick-bitlevel.h \
+	bricks/brick-hash.h bricks/brick-hashset.h  bricks/brick-shmem.h \
+	bricks/brick-types.h
+
 DEBIAN =					\
   debian/changelog				\
   debian/changelog.in				\

README

@@ -229,6 +229,7 @@ Third party software
 --------------------
 
 buddy/            A customized version of BuDDy 2.3 (a BDD library).
+bricks/           A collection of useful C++ code provided by DiVinE 3.3.2
 ltdl/             Libtool's portable dlopen() wrapper library.
 lib/              Gnulib's portability modules.
 utf8/             Nemanja Trifunovic's utf-8 routines.

bricks/brick-assert.h

+// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
+
+/*
+ * Various assert macros based on C++ exceptions and their support code.
+ */
+
+/*
+ * (c) 2006-2014 Petr Ročkai <me@mornfall.net>
+ */
+
+/* Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * 1. Redistributions of source code must retain the above copyright notice,
+ *    this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE. */
+
+#include <exception>
+#include <string>
+#include <sstream>
+
+#ifdef __divine__
+#include <divine.h>
+#endif
+
+#ifndef TEST
+#define TEST(n)         void n()
+#define TEST_FAILING(n) void n()
+#endif
+
+#ifdef __divine__
+#define ASSERT(x) assert( x )
+#define ASSERT_PRED(p, x) assert( p( x ) )
+#define ASSERT_EQ(x, y) assert( (x) == (y) )
+#define ASSERT_LEQ(x, y) assert( (x) <= (y) )
+#define ASSERT_NEQ(x, y) assert ( (x) != (y) )
+#define ASSERT_EQ_IDX(i, x, y) assert( (x) == (y) )
+
+#elif !defined NDEBUG
+#define ASSERT(x) ::brick::_assert::assert_fn( BRICK_LOCWRAP( BRICK_LOCATION( #x ) ), x )
+#define ASSERT_PRED(p, x) ::brick::_assert::assert_pred_fn( BRICK_LOCWRAP( BRICK_LOCATION( #p "( " #x " )" ) ), x, p( x ) )
+#define ASSERT_EQ(x, y) ::brick::_assert::assert_eq_fn( BRICK_LOCWRAP( BRICK_LOCATION( #x " == " #y ) ), x, y )
+#define ASSERT_LEQ(x, y) ::brick::_assert::assert_leq_fn( BRICK_LOCWRAP( BRICK_LOCATION( #x " <= " #y ) ), x, y )
+#define ASSERT_NEQ(x, y) ::brick::_assert::assert_neq_fn( BRICK_LOCWRAP( BRICK_LOCATION( #x " != " #y ) ), x, y )
+#define ASSERT_EQ_IDX(i, x, y) ::brick::_assert::assert_eq_fn( BRICK_LOCWRAP( BRICK_LOCATION_I( #x " == " #y, i ) ), x, y )
+
+#else
+
+#define ASSERT(x) ((void)0)
+#define ASSERT_PRED(p, x) ((void)0)
+#define ASSERT_EQ(x, y) ((void)0)
+#define ASSERT_LEQ(x, y) ((void)0)
+#define ASSERT_NEQ(x, y) ((void)0)
+#define ASSERT_EQ_IDX(i, x, y) ((void)0)
+#endif
+
+/* you must #include <brick-string.h> to use ASSERT_UNREACHABLE_F */
+#define ASSERT_UNREACHABLE_F(...) ::brick::_assert::assert_die_fn( BRICK_LOCATION( brick::string::fmtf(__VA_ARGS__) ) )
+#define ASSERT_UNREACHABLE(x) ::brick::_assert::assert_die_fn( BRICK_LOCATION( x ) )
+#define ASSERT_UNIMPLEMENTED() ::brick::_assert::assert_die_fn( BRICK_LOCATION( "not imlemented" ) )
+
+#ifdef _MSC_VER
+#define UNUSED
+#define noexcept
+#else
+#define UNUSED __attribute__((unused))
+#endif
+
+#ifndef BRICK_ASSERT_H
+#define BRICK_ASSERT_H
+
+namespace brick {
+namespace _assert {
+
+/* discard any number of paramentets, taken as const references */
+template< typename... X >
+void unused( const X&... ) { }
+
+struct Location {
+    const char *file;
+    int line, iteration;
+    std::string stmt;
+    Location( const char *f, int l, std::string st, int iter = -1 )
+        : file( f ), line( l ), iteration( iter ), stmt( st ) {}
+};
+
+#define BRICK_LOCATION(stmt) ::brick::_assert::Location( __FILE__, __LINE__, stmt )
+#define BRICK_LOCATION_I(stmt, i) ::brick::_assert::Location( __FILE__, __LINE__, stmt, i )
+
+// lazy location construction in C++11
+#if __cplusplus >= 201103L
+#define BRICK_LOCWRAP(x) [&]{ return (x); }
+#define BRICK_LOCUNWRAP(x) (x)()
+#else
+#define BRICK_LOCWRAP(x) (x)
+#define BRICK_LOCUNWRAP(x) (x)
+#endif
+
+
+struct AssertFailed : std::exception {
+    std::string str;
+
+    template< typename X >
+    friend inline AssertFailed &operator<<( AssertFailed &f, X x )
+    {
+        std::stringstream str;
+        str << x;
+        f.str += str.str();
+        return f;
+    }
+
+    AssertFailed( Location l )
+    {
+        (*this) << l.file << ": " << l.line;
+        if ( l.iteration != -1 )
+            (*this) << " (iteration " << l.iteration << ")";
+        (*this) << ": assertion `" << l.stmt << "' failed;";
+    }
+
+    const char *what() const noexcept { return str.c_str(); }
+};
+
+template< typename Location, typename X >
+void assert_fn( Location l, X x )
+{
+    if ( !x ) {
+        throw AssertFailed( BRICK_LOCUNWRAP( l ) );
+    }
+}
+
+inline void assert_die_fn( Location l ) __attribute__((noreturn));
+
+inline void assert_die_fn( Location l )
+{
+    throw AssertFailed( l );
+}
+
+template< typename Location, typename X, typename Y >
+void assert_eq_fn( Location l, X x, Y y )
+{
+    if ( !( x == y ) ) {
+        AssertFailed f( BRICK_LOCUNWRAP( l ) );
+        f << " got ["
+          << x << "] != [" << y
+          << "] instead";
+        throw f;
+    }
+}
+
+template< typename Location, typename X, typename Y >
+void assert_leq_fn( Location l, X x, Y y )
+{
+    if ( !( x <= y ) ) {
+        AssertFailed f( BRICK_LOCUNWRAP( l ) );
+        f << " got ["
+          << x << "] > [" << y
+          << "] instead";
+        throw f;
+    }
+}
+
+template< typename Location, typename X >
+void assert_pred_fn( Location l, X x, bool p )
+{
+    if ( !p ) {
+        AssertFailed f( BRICK_LOCUNWRAP( l ) );
+        f << " for " << x;
+        throw f;
+    }
+}
+
+template< typename Location, typename X, typename Y >
+void assert_neq_fn( Location l, X x, Y y )
+{
+    if ( x != y )
+        return;
+    AssertFailed f( BRICK_LOCUNWRAP( l ) );
+    f << " got ["
+      << x << "] == [" << y << "] instead";
+    throw f;
+}
+
+}
+}
+
+#endif
+
+// vim: syntax=cpp tabstop=4 shiftwidth=4 expandtab

configure.ac

@@ -62,6 +62,8 @@ AM_CONDITIONAL([ENABLE_DOXYGEN], [test "x${enable_doxygen:-no}" = xyes])
 # Activate C11 for gnulib tests
 AX_CHECK_COMPILE_FLAG([-std=c11], [CFLAGS="$CFLAGS -std=c11"])
 
+AX_CHECK_COMPILE_FLAG([-lpthread], [CFLAGS="$CFLAGS -lpthread"])
+
 gl_INIT
 
 # Use -Werror since using -fvisibility under MinGW is only a warning.
@@ -126,6 +128,8 @@ fi
 
 AX_CHECK_BUDDY
 
+AX_CHECK_DIVINE
+
 AC_CHECK_HEADERS([sys/times.h])
 AC_CHECK_FUNCS([times kill alarm sigaction])
 

debian/copyright

@@ -49,6 +49,33 @@ License: BSD-2-Clause
  OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
  MODIFICATIONS.
 
+Files: bricks/*
+Copyright: 2010-2014 Petr Ročkai, Jiří Weiser, Vladimír Štill
+License: BSD-2-Clause
+ Permission is hereby granted, without written agreement and without
+ license or royalty fees, to use, reproduce, prepare derivative
+ works, distribute, and display this software and its documentation
+ for any purpose, provided that (1) the above copyright notice and
+ the following two paragraphs appear in all copies of the source code
+ and (2) redistributions, including without limitation binaries,
+ reproduce these notices in the supporting documentation. Substantial
+ modifications to this software may be copyrighted by their authors
+ and need not follow the licensing terms described here, provided
+ that the new terms are clearly indicated in all files where they apply.
+ .
+ IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+ SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+ INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+ SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+ ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ .
+ JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+ BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+ FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+ OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+ MODIFICATIONS.
+
 Files: utf8/*
 Copyright: 2006 Nemanja Trifunovic
 License: BSL-1.0

debian/libspot-dev.install

 usr/include/spot
+usr/include/bricks
 usr/lib/*-*/libspot.so
 usr/lib/*-*/libspot.a
 usr/lib/*-*/pkgconfig/libspot.pc

m4/bricks.m4

+AC_DEFUN([AX_CHECK_BRICKS], [
+  AC_SUBST([BRICKS_CPPFLAGS], ['-I$(top_srcdir)/bricks'])
+  AC_CONFIG_SUBDIRS([bricks])
+])

tests/Makefile.am

@@ -22,7 +22,7 @@
 
 AUTOMAKE_OPTIONS = subdir-objects
 AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
-              -I$(top_builddir)/lib -I$(top_srcdir)/lib
+              $(BRICKS_CPPFLAGS) -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 LDADD = $(top_builddir)/spot/libspot.la $(top_builddir)/buddy/src/libbddx.la
 
@@ -68,6 +68,7 @@ check_PROGRAMS = \
   core/checkta \
   core/consterm \
   core/cube \
+  core/bricks \
   core/emptchk \
   core/equals \
   core/graph \
@@ -119,6 +120,7 @@ core_taatgba_SOURCES = core/taatgba.cc
 core_tgbagraph_SOURCES = core/twagraph.cc
 core_consterm_SOURCES = core/consterm.cc
 core_cube_SOURCES = core/cube.cc
+core_bricks_SOURCES = core/bricks.cc
 core_equals_SOURCES = core/equalsf.cc
 core_kind_SOURCES = core/kind.cc
 core_length_SOURCES = core/length.cc

tests/core/.gitignore

@@ -12,6 +12,7 @@ cube
 defs
 .deps
 *.dot
+bricks
 eltl2tgba
 emptchk
 defs

tests/core/bricks.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2016 Laboratoire de Recherche et Développement
+// 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/>.
+
+#include <bricks/brick-hashset.h>
+#include <bricks/brick-hash.h>
+
+struct both
+{
+  int x;
+  int y;
+};
+
+template<typename T>
+struct mytest_hasher_both
+{
+  template<typename X>
+  mytest_hasher_both(X&)
+  { }
+
+  mytest_hasher_both() = default;
+
+  brick::hash::hash128_t hash(both t) const
+  {
+    return std::make_pair(t.x*10, t.x);
+  }
+  bool valid(both t) const
+  {
+    return t.x != 0;
+  }
+  bool equal(both a, both b) const
+  {
+    return a.x == b.x;
+  }
+};
+
+int main()
+{
+  // Declare concurrent hash table
+  brick::hashset::FastConcurrent<both , mytest_hasher_both<both>> ht2;
+
+  // Set initial size
+  ht2.setSize(1024);
+
+  // Declare workers and provide them some jobs.
+  std::vector<std::thread> workers;
+  for (int i = 0; i < 6; i++)
+    workers.
+      push_back(std::thread([&ht2](int tid)
+			    {
+			      for (int i = 0; i< 2000; ++i)
+				ht2.insert({i, tid});
+			    }, i));
+
+  // Wait the end of all threads.
+  for (auto& t: workers)
+    t.join();
+
+  // Display the whole table.
+  for (unsigned i = 0; i < ht2.size(); ++ i)
+    if (ht2.valid(i))
+      std::cout << i << ": {"
+		<< ht2[i].x << ',' << ht2[i].y  << "}\n";
+  return 0;
+}