From 23908f3d2f2854872c7f80053e3961a52d8a60f2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Jun 2022 23:43:50 +0200 Subject: [PATCH] Add a --enable-pthread option to activate experimental threading code * NEWS, README, doc/org/compile.org: Mention the option and its effect on compilation requirements. * configure.ac: Add the --enable-pthread option, and ENABLE_PTHREAD macro. * doc/org/g++wrap.in, spot/Makefile.am, spot/libspot.pc.in: Compile with -pthread conditionally. * spot/graph/graph.hh, spot/twa/twagraph.cc: Adjust the code to not use thread-local variables, and let the pthread code be optional. * .gitlab-ci.yml: Activate --enable-pthread in two configurations. --- .gitlab-ci.yml | 8 ++++---- NEWS | 12 ++++++++++++ README | 6 ++++++ configure.ac | 11 ++++++++++- doc/org/compile.org | 5 ++++- doc/org/g++wrap.in | 4 ++-- spot/Makefile.am | 4 ++-- spot/graph/graph.hh | 13 +++++++++---- spot/libspot.pc.in | 2 +- spot/twa/twagraph.cc | 46 ++++++++++++++++++++++++++++---------------- 10 files changed, 79 insertions(+), 32 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3c66af0b7..a1bb0ca9a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -22,9 +22,9 @@ debian-stable-gcc: image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian:stable script: - autoreconf -vfi - - ./configure --enable-max-accsets=256 + - ./configure --enable-max-accsets=256 --enable-pthread - make - - make distcheck + - make distcheck DISTCHECK_CONFIGURE_FLAGS='--enable-max-accsets=256 --enable-pthread' artifacts: when: always paths: @@ -89,7 +89,7 @@ debian-gcc-snapshot: - autoreconf -vfi - ./configure --with-included-ltdl CXX='g++' - make - - make distcheck DISTCHECK_CONFIGURE_FLAGS='--with-included-ltdl' + - make distcheck DISTCHECK_CONFIGURE_FLAGS='--with-included-ltdl' allow_failure: true artifacts: when: always @@ -111,7 +111,7 @@ alpine-gcc: - autoreconf -vfi - ./configure - make - - make distcheck || { chmod -R u+w ./spot-*; false; } + - make distcheck DISTCHECK_CONFIGURE_FLAGS='--enable-pthread' || { chmod -R u+w ./spot-*; false; } artifacts: when: always paths: diff --git a/NEWS b/NEWS index 33b74132c..b8067d47a 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,17 @@ New in spot 2.10.6.dev (not yet released) + Build: + + - A new configure option --enable-pthread enable the compilation of + Spot with -pthread, and activate the parallel version of some + algorithms. If Spot is compiled with -pthread enabled, any user + linking with Spot should also link with the pthread library. In + order to not break existing build setups using Spot, this option + is currently disabled by default in this release. We plan to turn + it on by default in some future release. Third-party project + using Spot may want to start linking with -pthread in prevision + for this change. + Command-line tools: - autfilt has a new options --aliases=drop|keep to specify diff --git a/README b/README index 836bc51b0..7581df4ad 100644 --- a/README +++ b/README @@ -173,6 +173,12 @@ flags specific to Spot: client code should be compiled with -D_GLIBCXX_DEBUG as well. This options should normally only be useful to run Spot's test-suite. + --enable-pthread + Build and link with the -pthread option, and activate a few + parallel variants of the algorithms. This is currently disabled + by default, as it require all third-party tools using Spot to + build with -pthread as well. + --enable-c++20 Build everything in C++20 mode. We use that in our build farm to ensure that Spot can be used in C++20 projects as well. diff --git a/configure.ac b/configure.ac index 2ac9ff616..7c0ff62ae 100644 --- a/configure.ac +++ b/configure.ac @@ -53,6 +53,15 @@ AC_ARG_ENABLE([c++20], [Compile in C++20 mode.])], [enable_20=$enableval], [enable_20=no]) +AC_ARG_ENABLE([pthread], + [AS_HELP_STRING([--enable-pthread], + [Allow libspot to use POSIX threads.])], + [enable_pthread=$enableval], [enable_pthread=no]) +if test "$enable_pthread" = yes; then + AC_DEFINE([ENABLE_PTHREAD], [1], [Whether Spot is compiled with -pthread.]) + AC_SUBST([LIBSPOT_PTHREAD], [-pthread]) +fi + AC_ARG_ENABLE([doxygen], [AS_HELP_STRING([--enable-doxygen], [enable generation of Doxygen documentation (requires Doxygen)])], @@ -150,7 +159,7 @@ AX_CHECK_BUDDY AC_CHECK_FUNCS([times kill alarm sigaction sched_getcpu]) oLIBS=$LIBS -LIBS="$LIBS -lpthread" +LIBS="$LIBS -pthread" AC_CHECK_FUNCS([pthread_setaffinity_np]) LIBS=$oLIBS diff --git a/doc/org/compile.org b/doc/org/compile.org index 8d4a3b1ca..6c2f8e6c6 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -210,11 +210,14 @@ one library requiring another, you will need to link with the =bddx= library. This should be as simple as adding =-lbddx= after =-lspot= in the first three cases. +Similarly, if Spot has been configured with =--enable-pthread=, you +will need to add =-pthread= to the compiler flags. + In the fourth case where =libtool= is used to link against =libspot.la= linking against =libbddx.la= should not be necessary because Libtool already handles such dependencies. However the version of =libtool= distributed with Debian is patched to ignore those dependencies, so in this -case you 2 +case you have to list all dependencies. * Additional suggestions diff --git a/doc/org/g++wrap.in b/doc/org/g++wrap.in index c4a61a39c..b176af28b 100755 --- a/doc/org/g++wrap.in +++ b/doc/org/g++wrap.in @@ -1,6 +1,6 @@ #!/bin/sh # This is a wrapper around the compiler, to ensure that the code -# example run from the org-mode file are all linked with Spot. +# examples run from org-mode files are all linked with Spot. # # Also we save errors to org.errors, so that we can detect issues # after org-mode has exported everything. Otherwise these errors @@ -8,7 +8,7 @@ @top_builddir@/libtool link @CXX@ @CXXFLAGS@ @CPPFLAGS@ -Wall -Werror \ -I@abs_top_builddir@ -I@abs_top_srcdir@ -I@abs_top_srcdir@/buddy/src \ "$@" @abs_top_builddir@/spot/libspot.la \ - @abs_top_builddir@/buddy/src/libbddx.la 2> errors.$$ + @abs_top_builddir@/buddy/src/libbddx.la @LIBSPOT_PTHREAD@ 2> errors.$$ code=$? if test $code -ne 0 && test -s errors.$$; then cat errors.$$ >>org.errors diff --git a/spot/Makefile.am b/spot/Makefile.am index c7bebfe6a..72cbef22d 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016, 2017, 2020 +## Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016, 2017, 2020, 2022 ## Laboratoire de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -35,7 +35,7 @@ SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \ lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = -libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined -pthread $(SYMBOLIC_LDFLAGS) +libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined @LIBSPOT_PTHREAD@ $(SYMBOLIC_LDFLAGS) libspot_la_LIBADD = \ kripke/libkripke.la \ misc/libmisc.la \ diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index dc7ffc6ae..6419fc27a 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -20,6 +20,7 @@ #pragma once #include +#include #include #include #include @@ -28,7 +29,9 @@ #include #include #include -#include +#ifdef SPOT_ENABLE_PTHREAD +# include +#endif // SPOT_ENABLE_PTHREAD namespace spot { @@ -1242,8 +1245,6 @@ namespace spot //std::cerr << "\nbefore\n"; //dump_storage(std::cerr); const auto N = num_states(); - // Read threads once - const unsigned nthreads = get_nthreads(); auto idx_list = std::vector(N+1); auto new_edges = edge_vector_t(); @@ -1265,13 +1266,17 @@ namespace spot // If we have few edge or only one threads // Benchmark few? auto bne = new_edges.begin(); +#ifdef SPOT_ENABLE_PTHREAD + const unsigned nthreads = get_nthreads(); if (nthreads == 1 || edges_.size() < 1000) +#endif { for (auto s = 0u; s < N; ++s) std::stable_sort(bne + idx_list[s], bne + idx_list[s+1], p); } +#ifdef SPOT_ENABLE_PTHREAD else { static auto tv = std::vector(); @@ -1291,7 +1296,7 @@ namespace spot t.join(); tv.clear(); } - // Done +#endif std::swap(edges_, new_edges); // Like after normal sort_edges, they need to be chained before usage } diff --git a/spot/libspot.pc.in b/spot/libspot.pc.in index 2dac1de5d..9cb877b34 100644 --- a/spot/libspot.pc.in +++ b/spot/libspot.pc.in @@ -8,5 +8,5 @@ Description: A library of LTL and omega-automata algorithms for model checking URL: https://spot.lrde.epita.fr/ Version: @PACKAGE_VERSION@ Cflags: -I${includedir} -Libs: -L${libdir} -lspot +Libs: -L${libdir} -lspot @LIBSPOT_PTHREAD@ Requires: libbddx diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 2fd2eb070..5b4da10a3 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -372,7 +372,11 @@ namespace spot throw std::runtime_error( "twa_graph::merge_states() does not work on alternating automata"); +#ifdef ENABLE_PTHREAD const unsigned nthreads = get_nthreads(); +#else + constexpr unsigned nthreads = 1; +#endif typedef graph_t::edge_storage_t tr_t; g_.sort_edges_srcfirst_([](const tr_t& lhs, const tr_t& rhs) @@ -511,9 +515,12 @@ namespace spot // << ((env_map.size()+player_map.size())/((float)n_states)) // << '\n'; + // Check whether we can merge two states // and takes into account the self-loops - auto state_equal = [&](unsigned s1, unsigned s2) + auto state_equal = [&e_vec, &e_chain, &e_idx](unsigned s1, unsigned s2, + std::vector& checked1, + std::vector& checked2) { auto edge_data_comp = [](const auto& lhs, const auto& rhs) @@ -528,10 +535,6 @@ namespace spot return false; }; - - thread_local auto checked1 = std::vector(); - thread_local auto checked2 = std::vector(); - auto [i1, nsl1, sl1, e1] = e_idx[s1]; auto [i2, nsl2, sl2, e2] = e_idx[s2]; @@ -612,10 +615,10 @@ namespace spot std::vector remap(nb_states, -1U); // Check each hash - auto check_ix = [&](unsigned ix) + auto check_ix = [&](unsigned ix, std::vector& v, + std::vector& checked1, + std::vector& checked2) { - // Reduce cache miss - thread_local auto v = std::vector(); v.clear(); for (auto i = ix; i != -1U; i = hash_linked_list[i]) v.push_back(i); @@ -627,7 +630,7 @@ namespace spot for (unsigned jdx = 0; jdx < idx; ++jdx) { auto j = v[jdx]; - if (state_equal(j, i)) + if (state_equal(j, i, checked1, checked2)) { remap[i] = (remap[j] != -1U) ? remap[j] : j; @@ -675,13 +678,19 @@ namespace spot auto worker = [&upd, check_ix, nthreads](unsigned pid, auto begp, auto endp, auto bege, auto ende) - { - upd(begp, endp, pid); - upd(bege, ende, pid); - for (; begp != endp; upd(begp, endp, nthreads)) - check_ix(begp->second.first); - for (; bege != ende; upd(bege, ende, nthreads)) - check_ix(bege->second.first); + { + // Temporary storage for list of edges to reduce cache misses + std::vector v; + // Vector reused by all invocations of state_equal to mark edges + // that have been matched already. + std::vector checked1; + std::vector checked2; + upd(begp, endp, pid); + upd(bege, ende, pid); + for (; begp != endp; upd(begp, endp, nthreads)) + check_ix(begp->second.first, v, checked1, checked2); + for (; bege != ende; upd(bege, ende, nthreads)) + check_ix(bege->second.first, v, checked1, checked2); }; { @@ -690,10 +699,12 @@ namespace spot auto bege = env_map.begin(); auto ende = env_map.end(); - +#ifdef ENABLE_PTHREAD if ((nthreads == 1) & (num_states() > 1000)) // Bound? { +#endif // ENABLE_PTHREAD worker(0, begp, endp, bege, ende); +#ifdef ENABLE_PTHREAD } else { @@ -711,6 +722,7 @@ namespace spot t.join(); tv.clear(); } +#endif // ENABLE_PTHREAD } for (auto& e: edges())