diff --git a/benchmarks/CMakeLists.txt b/benchmarks/CMakeLists.txt index 1de03ec834..0e8174ebe7 100644 --- a/benchmarks/CMakeLists.txt +++ b/benchmarks/CMakeLists.txt @@ -15,7 +15,10 @@ function(add_tool_benchmark NAME TOOL INPUT OUTPUT) ) add_test(NAME ${TEST} - COMMAND ${CMAKE_COMMAND} "--build" ${CMAKE_BINARY_DIR} "--target" "${TARGET}") + COMMAND ${CMAKE_COMMAND} + "--build" ${CMAKE_BINARY_DIR} + "--target" "${TARGET}") + set_property(TEST ${TEST} PROPERTY LABELS "benchmark_tool") endfunction() @@ -137,5 +140,15 @@ if (MCRL2_ENABLE_DEVELOPER) "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" "-rjitty") + + add_tool_benchmark("${NAME}_jittyc" mcrl2rewrite + "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" + "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" + "-rjittyc") + + add_tool_benchmark("${NAME}_innermost" mcrl2rewrite + "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" + "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" + "-rinnermost") endforeach() endif() diff --git a/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h b/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h index b5e57e0f14..f8921e1c25 100644 --- a/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h +++ b/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h @@ -24,7 +24,7 @@ constexpr static bool EnableGarbageCollection = true; constexpr static bool EnableBlockAllocator = false; /// \brief Enable to print garbage collection statistics. -constexpr static bool EnableGarbageCollectionMetrics = true; +constexpr static bool EnableGarbageCollectionMetrics = false; /// Performs garbage collection intensively for testing purposes. constexpr static bool EnableAggressiveGarbageCollection = false; diff --git a/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h b/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h index a5ca980904..e6ec617182 100644 --- a/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h +++ b/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h @@ -43,7 +43,7 @@ class InnermostRewriter final : public Rewriter rewrite_strategy getStrategy() override { return innermost; } - std::shared_ptr clone() + std::shared_ptr clone() override { return std::shared_ptr(new InnermostRewriter(*this)); } diff --git a/libraries/lps/include/mcrl2/lps/lpsreach.h b/libraries/lps/include/mcrl2/lps/lpsreach.h index 99fb5d4000..0a731fd80c 100644 --- a/libraries/lps/include/mcrl2/lps/lpsreach.h +++ b/libraries/lps/include/mcrl2/lps/lpsreach.h @@ -281,7 +281,7 @@ class lpsreach_algorithm while (todo != empty_set() && (m_options.max_iterations == 0 || iteration_count < m_options.max_iterations)) { - stopwatch loop_start; + mcrl2::utilities::stopwatch loop_start; iteration_count++; mCRL2log(log::debug1) << "--- iteration " << iteration_count << " ---" << std::endl; mCRL2log(log::debug1) << "todo = " << print_states(m_lts.data_index, todo) << std::endl; diff --git a/libraries/pbes/include/mcrl2/pbes/pbesreach.h b/libraries/pbes/include/mcrl2/pbes/pbesreach.h index 696e53ef6a..3eb9df33a3 100644 --- a/libraries/pbes/include/mcrl2/pbes/pbesreach.h +++ b/libraries/pbes/include/mcrl2/pbes/pbesreach.h @@ -450,7 +450,7 @@ class pbesreach_algorithm mCRL2log(log::debug1) << "initial state = " << core::detail::print_list(m_initial_state) << std::endl; - stopwatch timer; + mcrl2::utilities::stopwatch timer; m_initial_vertex = initial_state(); m_visited = empty_set(); m_todo = m_initial_vertex; @@ -458,7 +458,7 @@ class pbesreach_algorithm while (m_todo != empty_set() && !solution_found() && (m_options.max_iterations == 0 || iteration_count < m_options.max_iterations)) { - stopwatch loop_start; + mcrl2::utilities::stopwatch loop_start; iteration_count++; mCRL2log(log::debug1) << "--- iteration " << iteration_count << " ---" << std::endl; mCRL2log(log::debug1) << "todo = " << print_states(m_data_index, m_todo) << std::endl; diff --git a/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h b/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h index d2d7743792..1041bd1cc7 100644 --- a/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h +++ b/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h @@ -322,7 +322,7 @@ class symbolic_parity_game const ldd& I = sylvan::ldds::empty_set(), const ldd& T = sylvan::ldds::empty_set()) const { - stopwatch attractor_watch; + mcrl2::utilities::stopwatch attractor_watch; mCRL2log(log::debug) << "start attractor set computation\n"; using namespace sylvan::ldds; @@ -342,7 +342,7 @@ class symbolic_parity_game mCRL2log(log::debug1) << "todo = " << print_nodes(todo) << std::endl; mCRL2log(log::debug1) << "Zoutside = " << print_nodes(Zoutside) << std::endl; - stopwatch iter_start; + mcrl2::utilities::stopwatch iter_start; todo = minus(safe_control_predecessors_impl(alpha, todo, Zoutside, Zoutside, V, Vplayer, I), Z); Z = union_(Z, todo); @@ -372,7 +372,7 @@ class symbolic_parity_game { using namespace sylvan::ldds; - stopwatch attractor_watch; + mcrl2::utilities::stopwatch attractor_watch; mCRL2log(log::debug) << "start monotone attractor set computation\n"; using namespace sylvan::ldds; @@ -403,7 +403,7 @@ class symbolic_parity_game mCRL2log(log::debug1) << "todo = " << print_nodes(todo) << std::endl; mCRL2log(log::debug1) << "Zoutside = " << print_nodes(Zoutside) << std::endl; - stopwatch iter_start; + mcrl2::utilities::stopwatch iter_start; todo = intersect(Vc, minus(safe_control_predecessors_impl(alpha, union_(todo, U), V, minus(Zoutside, U), Vc, Vplayer, I), Z)); Z = union_(Z, todo); @@ -519,7 +519,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; result = union_(result, predecessors(U, V, group)); mCRL2log(log::debug1) << "added predecessors for group " << i << " out of " << m_summand_groups.size() << " (time = " << std::setprecision(2) << std::fixed << watch.seconds() << "s)\n"; @@ -566,7 +566,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; ldd todo1 = predecessors(U, todo, group); mCRL2log(log::debug1) << "added predecessors for group " << i << " out of " << m_summand_groups.size() << " (time = " << std::setprecision(2) << std::fixed << watch.seconds() << "s)\n"; @@ -598,7 +598,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; Pforced = minus(Pforced, predecessors(Pforced, outside, group)); mCRL2log(log::debug1) << "removed 1 - alpha predecessors for group " << i << " out of " << m_summand_groups.size() diff --git a/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h b/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h index 23be915b44..f8acfefdfa 100644 --- a/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h +++ b/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h @@ -39,7 +39,7 @@ class symbolic_pbessolve_algorithm return { empty_set(), empty_set() }; } - stopwatch timer; + mcrl2::utilities::stopwatch timer; mCRL2log(log::debug) << "start zielonka recursion\n"; auto [m, U] = m_G.get_min_rank(V); @@ -90,7 +90,7 @@ class symbolic_pbessolve_algorithm const ldd& W1 = sylvan::ldds::empty_set()) { using namespace sylvan::ldds; - stopwatch timer; + mcrl2::utilities::stopwatch timer; std::array winning = { W0, W1 }; ldd Vtotal = m_G.compute_total_graph(V, empty_set(), Vsinks, winning); @@ -207,7 +207,7 @@ class symbolic_pbessolve_algorithm std::size_t iter = 0; while (U != Unext) { - stopwatch timer; + mcrl2::utilities::stopwatch timer; U = Unext; Unext = m_G.predecessors(U, U); @@ -287,7 +287,7 @@ class symbolic_pbessolve_algorithm std::size_t iter = 0; while (U != Unext) { - stopwatch timer; + mcrl2::utilities::stopwatch timer; U = Unext; if (safe_variant) { @@ -331,7 +331,7 @@ class symbolic_pbessolve_algorithm const ldd& W1 = sylvan::ldds::empty_set()) { using namespace sylvan::ldds; - stopwatch timer; + mcrl2::utilities::stopwatch timer; std::array winning = { W0, W1 }; ldd Vtotal = m_G.compute_total_graph(V, I, Vsinks, winning); diff --git a/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h b/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h index 2974970825..2fd8356768 100644 --- a/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h +++ b/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h @@ -137,7 +137,7 @@ void learn_successors_callback(WorkerP*, Task*, std::uint32_t* x, std::size_t, v // add the assignments corresponding to x to sigma // add x to the transition xy - stopwatch learn_start; + mcrl2::utilities::stopwatch learn_start; for (std::size_t j = 0; j < x_size; j++) { sigma[group.read_parameters[j]] = data_index[group.read[j]][x[j]]; diff --git a/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp b/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp index 0d411a65f4..4cc7d7cec0 100644 --- a/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp +++ b/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp @@ -48,7 +48,7 @@ class pbesreach_algorithm_partial : public pbes_system::pbesreach_algorithm if (time_solving * 10 < (time_solving + time_exploring) || m_options.aggressive) { mCRL2log(log::verbose) << "start partial solving\n"; - stopwatch timer; + mcrl2::utilities::stopwatch timer; // Store the set of won states to keep track of whether new states have been solved. std::array Vwon = m_Vwon; @@ -127,7 +127,7 @@ class pbesreach_algorithm_partial : public pbes_system::pbesreach_algorithm double time_solving = 0.0; double time_exploring = 0.0; - stopwatch explore_timer; + mcrl2::utilities::stopwatch explore_timer; }; } // namespace mcrl2::pbes_system