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

@@ -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:
@@ -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:

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

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.

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
 

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
 

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

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 \

spot/graph/graph.hh

@@ -20,6 +20,7 @@
 #pragma once
 
 #include <spot/misc/common.hh>
+#include <spot/misc/_config.h>
 #include <vector>
 #include <type_traits>
 #include <tuple>
@@ -28,7 +29,9 @@
 #include <algorithm>
 #include <map>
 #include <iostream>
+#ifdef SPOT_ENABLE_PTHREAD
 #  include <thread>
+#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<unsigned>(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<std::thread>();
@@ -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
     }

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

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<char>& checked1,
+                                                  std::vector<char>& 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<char>();
-        thread_local auto checked2 = std::vector<char>();
-
         auto [i1, nsl1, sl1, e1] = e_idx[s1];
         auto [i2, nsl2, sl2, e2] = e_idx[s2];
 
@@ -612,10 +615,10 @@ namespace spot
     std::vector<unsigned> remap(nb_states, -1U);
 
     // Check each hash
-    auto check_ix = [&](unsigned ix)
+    auto check_ix = [&](unsigned ix, std::vector<unsigned>& v,
+                        std::vector<char>& checked1,
+                        std::vector<char>& checked2)
       {
-        // Reduce cache miss
-        thread_local auto v = std::vector<unsigned>();
         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;
 
@@ -676,12 +679,18 @@ namespace spot
     auto worker = [&upd, check_ix, nthreads](unsigned pid, auto begp, auto endp,
                                              auto bege, auto ende)
     {
+      // Temporary storage for list of edges to reduce cache misses
+      std::vector<unsigned> v;
+      // Vector reused by all invocations of state_equal to mark edges
+      // that have been matched already.
+      std::vector<char> checked1;
+      std::vector<char> checked2;
       upd(begp, endp, pid);
       upd(bege, ende, pid);
       for (; begp != endp; upd(begp, endp, nthreads))
-          check_ix(begp->second.first);
+        check_ix(begp->second.first, v, checked1, checked2);
       for (; bege != ende; upd(bege, ende, nthreads))
-          check_ix(bege->second.first);
+        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())