Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase
See merge request simgrid/simgrid!139
# Basic checks on cmake
cmake_minimum_required(VERSION 3.12)
# once we move CMake to >= 3.13, we should use target_link_option in examples/sthread
+# once we move CMake to >= 3.13.1, we could get rid of _Boost_STACKTRACE_BACKTRACE_HEADERS
message(STATUS "Cmake version ${CMAKE_MAJOR_VERSION}.${CMAKE_MINOR_VERSION}.${CMAKE_PATCH_VERSION}")
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} ${CMAKE_HOME_DIRECTORY}/tools/cmake/Modules)
message(STATUS "Disabling model BMF because Eigen3 was not found. If it's installed, use EIGEN3_HINT to hint cmake about the location of Eigen3Config.cmake")
endif()
+# Check for our JSON dependency
+set(SIMGRID_HAVE_JSON 0)
+find_package(nlohmann_json 3.7
+ HINTS ${nlohmann_json_HINT})
+if (nlohmann_json_FOUND)
+ set(SIMGRID_HAVE_JSON 1)
+ if (NOT NLOHMANN_JSON_INCLUDE_DIR)
+ get_target_property(NLOHMANN_JSON_INCLUDE_DIR nlohmann_json::nlohmann_json INTERFACE_INCLUDE_DIRECTORIES)
+ list(REMOVE_DUPLICATES NLOHMANN_JSON_INCLUDE_DIR)
+ else()
+ include_directories(${NLOHMANN_JSON_INCLUDE_DIR})
+ endif()
+ message(STATUS "Found nlohmann_json: ${NLOHMANN_JSON_INCLUDE_DIR}")
+endif()
+
set(HAVE_PAPI 0)
if(enable_smpi_papi)
include(FindPAPI)
else()
message(" Compile Python bindings .....: OFF (disabled, or pybind11 not found)")
endif()
-if(Eigen3_FOUND)
+if(SIMGRID_HAVE_EIGEN3)
message(" Eigen3 library ..............: ${EIGEN3_VERSION_STRING} in ${EIGEN3_INCLUDE_DIR}")
else()
message(" Eigen3 library ..............: not found (EIGEN3_HINT='${EIGEN3_HINT}').")
endif()
+if(SIMGRID_HAVE_JSON)
+ message(" JSON library.................: ${nlohmann_json_VERSION} in ${NLOHMANN_JSON_INCLUDE_DIR}")
+else()
+ message(" JSON library.................: not found (nlohmann_json_HINT='${nlohmann_json_HINT}')")
+endif()
message(" Compile Smpi ................: ${HAVE_SMPI}")
message(" Smpi fortran ..............: ${SMPI_FORTRAN}")
message(" MPICH3 testsuite ..........: ${enable_smpi_MPICH3_testsuite}")
include docs/source/Start_your_own_project.rst
include docs/source/The_XBT_toolbox.rst
include docs/source/Tutorial_Algorithms.rst
+include docs/source/Tutorial_DAG.rst
include docs/source/Tutorial_MPI_Applications.rst
include docs/source/Tutorial_Model-checking.rst
include docs/source/XML_reference.rst
include docs/source/img/zoom_comm.svg
include docs/source/index.rst
include docs/source/intl.rst
+include docs/source/tuto_dag/dag_lab1.cpp
+include docs/source/tuto_dag/dag_lab2-1.cpp
+include docs/source/tuto_dag/dag_lab2-2.cpp
+include docs/source/tuto_dag/dag_lab2-3.cpp
+include docs/source/tuto_dag/img/dag.svg
+include docs/source/tuto_dag/img/dag1.svg
+include docs/source/tuto_dag/img/dag2.svg
+include docs/source/tuto_dag/simple_dax.xml
+include docs/source/tuto_dag/simple_dot.dot
+include docs/source/tuto_dag/simple_json.json
+include docs/source/tuto_dag/small_platform.xml
include docs/source/tuto_disk/CMakeLists.txt
include docs/source/tuto_disk/Dockerfile
include docs/source/tuto_disk/analysis.irst
include src/kernel/xml/simgrid_dtd.c
include src/kernel/xml/simgrid_dtd.h
include src/mc/AddressSpace.hpp
-include src/mc/ModelChecker.cpp
-include src/mc/ModelChecker.hpp
include src/mc/VisitedState.cpp
include src/mc/VisitedState.hpp
include src/mc/api/ActorState.hpp
include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
+include src/mc/api/guide/BasicGuide.hpp
+include src/mc/api/guide/GuidedState.hpp
include src/mc/compare.cpp
include src/mc/datatypes.h
include src/mc/explo/CommunicationDeterminismChecker.cpp
include tools/cmake/Modules/FindNS3.cmake
include tools/cmake/Modules/FindPAPI.cmake
include tools/cmake/Modules/FindValgrind.cmake
+include tools/cmake/Modules/nlohmann_jsonConfig.cmake
include tools/cmake/Modules/pybind11Config.cmake
include tools/cmake/Option.cmake
include tools/cmake/Tests.cmake
- On CentOS / Fedora: ``dnf install eigen3-devel``
- On macOS with homebrew: ``brew install eigen``
- Use EIGEN3_HINT to specify where it's installed if cmake doesn't find it automatically.
+JSON (optional, for the DAG wfcommons loader)
+ - On Debian / Ubuntu: ``apt install nlohmann-json3-dev``
+ - Use nlohmann_json_HINT to specify where it's installed if cmake doesn't find it automatically.
For platform-specific details, please see below.
--- /dev/null
+.. _simdag:
+
+Simulating DAG
+==============
+
+This tutorial presents the basics to understand how DAG are represented in Simgrid and how to simulate their workflow.
+
+Definition of a DAG
+-------------------
+
+Directed Acyclic Graph:
+
+.. math::
+
+ \mathcal{G} = (\mathcal{V},\mathcal{E})
+
+Set of vertices representing :ref:`Activities <API_s4u_Activity>`:
+
+.. math::
+
+ \mathcal{V} = {v_i | i = 1, ..., V}
+
+Set of edges representing precedence constraints between :ref:`Activities <API_s4u_Activity>`:
+
+.. math::
+
+ \mathcal{E} = {e_i,j | (i,j) \in {1, ..., V} x {1, ..., V}}
+
+.. image:: /tuto_dag/img/dag.svg
+ :align: center
+
+Representing Vertices/Activities
+................................
+
+There is two types of :ref:`Activities <API_s4u_Activity>` that can represent Vertices: :ref:`Exec <API_s4u_Exec>` and :ref:`Comm <API_s4u_Comm>`.
+Thoses activities must be initiated and configured to properly describe your worflow.
+
+An Exec represents the execution of an amount of flop on a :ref:`Host <API_s4u_Host>` of your platform.
+
+.. code-block:: cpp
+
+ ExecPtr exec = Exec::init();
+ exec->set_flops_amount(int);
+ exec->set_host(Host*);
+ exec->start();
+
+A Comm represents a data transfer between two :ref:`Hosts <API_s4u_Host>` of your platform.
+
+.. code-block:: cpp
+
+ CommPtr comm = Comm::sendto_init();
+ comm->set_source(Host*);
+ comm->set_destination(Host*);
+ comm->start();
+
+Representing Edges/Dependencies
+...............................
+
+An activity will not start until all of its dependencies have been completed.
+Activities may have any number of successors.
+Dependencies between Activities are created using :cpp:func:`Activity::add_successor(ActivityPtr)`.
+
+.. code-block:: cpp
+
+ exec->add_successor(comm);
+
+The Activity ``comm`` will not start until ``exec`` has been completed.
+
+Lab 1: Basics
+---------------
+
+The goal of this lab is to describe the following DAG:
+
+.. image:: /tuto_dag/img/dag1.svg
+ :align: center
+
+In this DAG we want ``c1`` to compute 1e9 flops, ``c2`` to compute 5e9 flops and ``c3`` to compute 2e9 flops.
+There is also a data transfer of 5e8 bytes between ``c1`` and ``c3``.
+
+First of all, include the Simgrid library and define the log category.
+
+.. code-block:: cpp
+
+ #include "simgrid/s4u.hpp"
+
+ XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u tutorial");
+
+Inside the ``main`` function create an instance of :ref:`Engine <API_s4u_Engine>` and load the platform.
+
+.. code-block:: cpp
+
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+Retrieve pointers to some hosts.
+
+.. code-block:: cpp
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+
+Initiate the activities.
+
+.. code-block:: cpp
+
+ simgrid::s4u::ExecPtr c1 = simgrid::s4u::Exec::init();
+ simgrid::s4u::ExecPtr c2 = simgrid::s4u::Exec::init();
+ simgrid::s4u::ExecPtr c3 = simgrid::s4u::Exec::init();
+ simgrid::s4u::CommPtr t1 = simgrid::s4u::Comm::sendto_init();
+
+Give names to thoses activities.
+
+.. code-block:: cpp
+
+ c1->set_name("c1");
+ c2->set_name("c2");
+ c3->set_name("c3");
+ t1->set_name("t1");
+
+Set the amount of work for each activity.
+
+.. code-block:: cpp
+
+ c1->set_flops_amount(1e9);
+ c2->set_flops_amount(5e9);
+ c3->set_flops_amount(2e9);
+ t1->set_payload_size(5e8);
+
+Define the dependencies between the activities.
+
+.. code-block:: cpp
+
+ c1->add_successor(t1);
+ t1->add_successor(c3);
+ c2->add_successor(c3);
+
+Set the location of each Exec activity and source and destination for the Comm activity.
+
+.. code-block:: cpp
+
+ c1->set_host(tremblay);
+ c2->set_host(jupiter);
+ c3->set_host(jupiter);
+ t1->set_source(tremblay);
+ t1->set_destination(jupiter);
+
+Start the executions of Activities without dependencies.
+
+.. code-block:: cpp
+
+ c1->start();
+ c2->start();
+
+Add a callback to monitor the activities.
+
+.. code-block:: cpp
+
+ Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+Finally, run the simulation.
+
+.. code-block:: cpp
+
+ e.run();
+
+The execution of this code should give you the following output:
+
+.. code-block:: bash
+
+ [10.194200] [main/INFO] Activity 'c1' is complete (start time: 0.000000, finish time: 10.194200)
+ [65.534235] [main/INFO] Activity 'c2' is complete (start time: 0.000000, finish time: 65.534235)
+ [85.283378] [main/INFO] Activity 't1' is complete (start time: 10.194200, finish time: 85.283378)
+ [111.497072] [main/INFO] Activity 'c3' is complete (start time: 85.283378, finish time: 111.497072)
+
+Lab 2: Import a DAG from a file
+---------------
+
+In this lab we present how to import a DAG into you Simgrid simulation, either using a DOT file, a JSON file, or a DAX file.
+
+The files presented in this lab describe the following DAG:
+
+.. image:: /tuto_dag/img/dag2.svg
+ :align: center
+
+From a DOT file
+...............
+
+A DOT file describes a workflow in accordance with the graphviz format.
+
+The following DOT file describes the workflow presented at the beginning of this lab:
+
+.. code-block:: xml
+
+ digraph G {
+ c1 [size="1e9"];
+ c2 [size="5e9"];
+ c3 [size="2e9"];
+
+ root->c1 [size="2e8"];
+ root->c2 [size="1e8"];
+ c1->c3 [size="5e8"];
+ c2->c3 [size="-1"];
+ c3->end [size="2e8"];
+ }
+
+It can be imported as a vector of Activities into Simgrid using :cpp:func:`create_DAG_from_DOT(const std::string& filename)`. Then, you have to assign hosts to your Activities.
+
+.. code-block:: cpp
+
+ #include "simgrid/s4u.hpp"
+
+ XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+ int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_dot(argv[2]);
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+ simgrid::s4u::Host* fafard = e.host_by_name("Fafard");
+
+ dynamic_cast<simgrid::s4u::Exec*>(dag[0].get())->set_host(fafard);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[1].get())->set_host(tremblay);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[2].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[3].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[8].get())->set_host(jupiter);
+
+ for (const auto& a : dag) {
+ if (auto* comm = dynamic_cast<simgrid::s4u::Comm*>(a.get())) {
+ auto pred = dynamic_cast<simgrid::s4u::Exec*>((*comm->get_dependencies().begin()).get());
+ auto succ = dynamic_cast<simgrid::s4u::Exec*>(comm->get_successors().front().get());
+ comm->set_source(pred->get_host())->set_destination(succ->get_host());
+ }
+ }
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+ }
+
+The execution of this code should give you the following output:
+
+.. code-block:: bash
+
+ [0.000000] [main/INFO] Activity 'root' is complete (start time: 0.000000, finish time: 0.000000)
+ [33.394394] [main/INFO] Activity 'root->c2' is complete (start time: 0.000000, finish time: 33.394394)
+ [39.832311] [main/INFO] Activity 'root->c1' is complete (start time: 0.000000, finish time: 39.832311)
+ [50.026511] [main/INFO] Activity 'c1' is complete (start time: 39.832311, finish time: 50.026511)
+ [98.928629] [main/INFO] Activity 'c2' is complete (start time: 33.394394, finish time: 98.928629)
+ [125.115689] [main/INFO] Activity 'c1->c3' is complete (start time: 50.026511, finish time: 125.115689)
+ [151.329383] [main/INFO] Activity 'c3' is complete (start time: 125.115689, finish time: 151.329383)
+ [151.743605] [main/INFO] Activity 'c3->end' is complete (start time: 151.329383, finish time: 151.743605)
+ [151.743605] [main/INFO] Activity 'end' is complete (start time: 151.743605, finish time: 151.743605)
+
+From a JSON file
+................
+
+A JSON file describes a workflow in accordance with the `wfformat <https://github.com/wfcommons/wfformat>`_ .
+
+The following JSON file describes the workflow presented at the beginning of this lab:
+
+.. code-block:: JSON
+
+ {
+ "name": "simple_json",
+ "schemaVersion": "1.0",
+ "workflow": {
+ "makespan": 0,
+ "executedAt": "2023-03-09T00:00:00-00:00",
+ "tasks": [
+ {
+ "name": "c1",
+ "type": "compute",
+ "parents": [],
+ "runtime": 1e9,
+ "machine": "Tremblay"
+ },
+ {
+ "name": "t1",
+ "type": "transfer",
+ "parents": ["c1"],
+ "bytesWritten": 5e8,
+ "machine": "Jupiter"
+ },
+ {
+ "name": "c2",
+ "type": "compute",
+ "parents": [],
+ "runtime": 5e9,
+ "machine": "Jupiter"
+ },
+ {
+ "name": "c3",
+ "type": "compute",
+ "parents": ["t1","c2"],
+ "runtime": 2e9,
+ "machine": "Jupiter"
+ }
+ ],
+ "machines": [
+ {"nodeName": "Tremblay"},
+ {"nodeName": "Jupiter"}
+ ]
+ }
+ }
+
+It can be imported as a vector of Activities into Simgrid using :cpp:func:`create_DAG_from_json(const std::string& filename)`.
+
+.. code-block:: cpp
+
+ #include "simgrid/s4u.hpp"
+
+ XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+ int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_json(argv[2]);
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+ }
+
+The execution of this code should give you the following output:
+
+.. code-block:: bash
+
+ [10.194200] [main/INFO] Activity 'c1' is complete (start time: 0.000000, finish time: 10.194200)
+ [65.534235] [main/INFO] Activity 'c2' is complete (start time: 0.000000, finish time: 65.534235)
+ [85.283378] [main/INFO] Activity 't1' is complete (start time: 10.194200, finish time: 85.283378)
+ [111.497072] [main/INFO] Activity 'c3' is complete (start time: 85.283378, finish time: 111.497072)
+
+From a DAX file [deprecated]
+............................
+
+A DAX file describes a workflow in accordance with the `Pegasus <http://pegasus.isi.edu/>`_ format.
+
+The following DAX file describes the workflow presented at the beginning of this lab:
+
+.. code-block:: xml
+
+ <?xml version="1.0" encoding="UTF-8"?>
+ <adag xmlns="http://pegasus.isi.edu/schema/DAX" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:schemaLocation="http://pegasus.isi.edu/schema/DAX http://pegasus.isi.edu/schema/dax-2.1.xsd"
+ version="2.1">
+ <job id="1" name="c1" runtime="10">
+ <uses file="i1" link="input" register="true" transfer="true" optional="false" type="data" size="2e8"/>
+ <uses file="o1" link="output" register="true" transfer="true" optional="false" type="data" size="5e8"/>
+ </job>
+ <job id="2" name="c2" runtime="50">
+ <uses file="i2" link="input" register="true" transfer="true" optional="false" type="data" size="1e8"/>
+ </job>
+ <job id="3" name="c3" runtime="20">
+ <uses file="o1" link="input" register="true" transfer="true" optional="false" type="data" size="5e8"/>
+ <uses file="o3" link="output" register="true" transfer="true" optional="false" type="data" size="2e8"/>
+ </job>
+ <child ref="3">
+ <parent ref="1"/>
+ <parent ref="2"/>
+ </child>
+ </adag>
+
+It can be imported as a vector of Activities into Simgrid using :cpp:func:`create_DAG_from_DAX(std::string)`.
+
+.. code-block:: cpp
+
+ #include "simgrid/s4u.hpp"
+
+ XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+ int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_DAX(argv[2]);
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+ simgrid::s4u::Host* fafard = e.host_by_name("Fafard");
+
+ dynamic_cast<simgrid::s4u::Exec*>(dag[0].get())->set_host(fafard);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[1].get())->set_host(tremblay);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[2].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[3].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[8].get())->set_host(jupiter);
+
+ for (const auto& a : dag) {
+ if (auto* comm = dynamic_cast<simgrid::s4u::Comm*>(a.get())) {
+ auto pred = dynamic_cast<simgrid::s4u::Exec*>((*comm->get_dependencies().begin()).get());
+ auto succ = dynamic_cast<simgrid::s4u::Exec*>(comm->get_successors().front().get());
+ comm->set_source(pred->get_host())->set_destination(succ->get_host());
+ }
+ }
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+ }
+
Simulating distributed algorithms <Tutorial_Algorithms.rst>
Simulating MPI applications <Tutorial_MPI_Applications.rst>
Model-checking algorithms <Tutorial_Model-checking.rst>
+ Simulating DAG <Tutorial_DAG.rst>
.. toctree::
:hidden:
--- /dev/null
+#include "simgrid/s4u.hpp"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u tutorial");
+
+int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+
+ simgrid::s4u::ExecPtr c1 = simgrid::s4u::Exec::init();
+ simgrid::s4u::ExecPtr c2 = simgrid::s4u::Exec::init();
+ simgrid::s4u::ExecPtr c3 = simgrid::s4u::Exec::init();
+ simgrid::s4u::CommPtr t1 = simgrid::s4u::Comm::sendto_init();
+
+ c1->set_name("c1");
+ c2->set_name("c2");
+ c3->set_name("c3");
+ t1->set_name("t1");
+
+ c1->set_flops_amount(1e9);
+ c2->set_flops_amount(5e9);
+ c3->set_flops_amount(2e9);
+ t1->set_payload_size(5e8);
+
+ c1->add_successor(t1);
+ t1->add_successor(c3);
+ c2->add_successor(c3);
+
+ c1->set_host(tremblay);
+ c2->set_host(jupiter);
+ c3->set_host(jupiter);
+ t1->set_source(tremblay);
+ t1->set_destination(jupiter);
+
+ c1->start();
+ c2->start();
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+}
+
--- /dev/null
+#include "simgrid/s4u.hpp"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_dot(argv[2]);
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+ simgrid::s4u::Host* fafard = e.host_by_name("Fafard");
+
+ dynamic_cast<simgrid::s4u::Exec*>(dag[0].get())->set_host(fafard);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[1].get())->set_host(tremblay);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[2].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[3].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[8].get())->set_host(jupiter);
+
+ for (const auto& a : dag) {
+ if (auto* comm = dynamic_cast<simgrid::s4u::Comm*>(a.get())) {
+ auto pred = dynamic_cast<simgrid::s4u::Exec*>((*comm->get_dependencies().begin()).get());
+ auto succ = dynamic_cast<simgrid::s4u::Exec*>(comm->get_successors().front().get());
+ comm->set_source(pred->get_host())->set_destination(succ->get_host());
+ }
+ }
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+}
+
--- /dev/null
+#include "simgrid/s4u.hpp"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_json(argv[2]);
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+}
+
--- /dev/null
+#include "simgrid/s4u.hpp"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(main, "Messages specific for this s4u example");
+
+int main(int argc, char* argv[]) {
+ simgrid::s4u::Engine e(&argc, argv);
+ e.load_platform(argv[1]);
+
+ std::vector<simgrid::s4u::ActivityPtr> dag = simgrid::s4u::create_DAG_from_DAX(argv[2]);
+
+ simgrid::s4u::Host* tremblay = e.host_by_name("Tremblay");
+ simgrid::s4u::Host* jupiter = e.host_by_name("Jupiter");
+ simgrid::s4u::Host* fafard = e.host_by_name("Fafard");
+
+ dynamic_cast<simgrid::s4u::Exec*>(dag[0].get())->set_host(fafard);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[1].get())->set_host(tremblay);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[2].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[3].get())->set_host(jupiter);
+ dynamic_cast<simgrid::s4u::Exec*>(dag[8].get())->set_host(jupiter);
+
+ for (const auto& a : dag) {
+ if (auto* comm = dynamic_cast<simgrid::s4u::Comm*>(a.get())) {
+ auto pred = dynamic_cast<simgrid::s4u::Exec*>((*comm->get_dependencies().begin()).get());
+ auto succ = dynamic_cast<simgrid::s4u::Exec*>(comm->get_successors().front().get());
+ comm->set_source(pred->get_host())->set_destination(succ->get_host());
+ }
+ }
+
+ simgrid::s4u::Activity::on_completion_cb([](simgrid::s4u::Activity const& activity) {
+ XBT_INFO("Activity '%s' is complete (start time: %f, finish time: %f)", activity.get_cname(), activity.get_start_time(),
+ activity.get_finish_time());
+ });
+
+ e.run();
+ return 0;
+}
+
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+ version="1.1"
+ id="svg2"
+ width="275.83713"
+ height="134.41872"
+ viewBox="0 0 275.83713 134.41872"
+ sodipodi:docname="simdag-101.svg"
+ inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:svg="http://www.w3.org/2000/svg">
+ <defs
+ id="defs6">
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath232">
+ <path
+ d="M 0,0 H 305 V 149 H 0 Z"
+ id="path230" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath320">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2228.77,-1230.227 -84.41,-42.203 17.01,-34.015 84.4,42.203 v 0 l -75.58,-17.004 z"
+ clip-rule="evenodd"
+ id="path318" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath334">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2101.53,-1281.879 91.96,-23.933 10.08,36.531 -92.59,23.937 v 0 l 68.66,-37.793 z"
+ clip-rule="evenodd"
+ id="path332" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath348">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 963.93,-1245.344 -92.598,-23.937 10.078,-36.531 91.965,23.933 v 0 l -77.477,-1.258 z"
+ clip-rule="evenodd"
+ id="path346" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath362">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 829.129,-1264.242 85.035,-42.203 16.379,34.015 -84.406,42.203 v 0 l 59.211,-51.019 z"
+ clip-rule="evenodd"
+ id="path360" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath376">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 221.277,-411.98 31.493,-42.21 30.234,22.68 -31.492,42.2 v 0 l 7.558,-41.57 z"
+ clip-rule="evenodd"
+ id="path374" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath390">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 269.148,-388.68 -28.347,-44.09 32.125,-20.16 28.347,44.09 v 0 l -35.906,-22.04 z"
+ clip-rule="evenodd"
+ id="path388" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath404">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 668.504,-391.83 v -52.91 h 37.793 v 52.91 0 l -18.895,-37.79 z"
+ clip-rule="evenodd"
+ id="path402" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath418">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 1093.69,-391.83 v -52.91 h 37.79 v 52.91 0 l -18.89,-37.79 z"
+ clip-rule="evenodd"
+ id="path416" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath432">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 1498.08,-408.84 28.35,-44.09 32.12,20.16 -28.34,44.09 v 0 l 4.41,-42.2 z"
+ clip-rule="evenodd"
+ id="path430" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath446">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 1544.7,-388.68 -28.35,-44.09 32.13,-20.16 28.34,44.09 v 0 l -35.9,-22.04 z"
+ clip-rule="evenodd"
+ id="path444" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath460">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 1944.05,-391.83 v -52.91 h 37.8 v 52.91 0 l -18.9,-37.79 z"
+ clip-rule="evenodd"
+ id="path458" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath474">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2369.23,-391.83 v -52.91 h 37.8 v 52.91 0 l -18.9,-37.79 z"
+ clip-rule="evenodd"
+ id="path472" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath488">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2772.37,-411.98 31.5,-42.21 30.23,22.68 -31.49,42.2 v 0 l 7.55,-41.57 z"
+ clip-rule="evenodd"
+ id="path486" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath502">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2820.24,-388.68 -28.34,-44.09 32.12,-20.16 28.35,44.09 v 0 l -35.91,-22.04 z"
+ clip-rule="evenodd"
+ id="path500" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath516">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 444.891,647.164 482.055,610 l 26.457,26.453 -37.164,37.164 v 0 l 13.855,-40.312 z"
+ clip-rule="evenodd"
+ id="path514" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath530">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 477.645,673.617 440.48,636.453 466.938,610 l 37.164,37.164 v 0 l -39.684,-13.859 z"
+ clip-rule="evenodd"
+ id="path528" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath544">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 870.074,647.164 907.238,610 l 26.453,26.453 -37.164,37.164 v 0 l 13.86,-40.312 z"
+ clip-rule="evenodd"
+ id="path542" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath558">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 902.828,673.617 865.664,636.453 892.117,610 l 37.168,37.164 v 0 l -39.687,-13.859 z"
+ clip-rule="evenodd"
+ id="path556" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath572">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 1295.25,647.164 1332.42,610 l 26.46,26.453 -37.17,37.164 v 0 l 13.86,-40.312 z"
+ clip-rule="evenodd"
+ id="path570" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath586">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 1328.01,673.617 1290.85,636.453 1317.3,610 l 37.16,37.164 v 0 l -39.68,-13.859 z"
+ clip-rule="evenodd"
+ id="path584" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath600">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 1720.44,647.164 1757.6,610 l 26.46,26.453 -37.17,37.164 v 0 l 13.86,-40.312 z"
+ clip-rule="evenodd"
+ id="path598" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath614">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 1753.19,-816.383 -37.16,-37.164 26.45,-26.453 37.17,37.164 v 0 l -39.69,-13.859 z"
+ clip-rule="evenodd"
+ id="path612" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath628">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 2145.62,647.164 2182.79,610 l 26.45,26.453 -37.17,37.164 v 0 l 13.86,-40.312 z"
+ clip-rule="evenodd"
+ id="path626" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath642">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2178.38,-816.383 -37.17,-37.164 26.46,-26.453 37.16,37.164 v 0 l -39.68,-13.859 z"
+ clip-rule="evenodd"
+ id="path640" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath656">
+ <path
+ d="M 0,1490 V 0 H 3050 V 1490 Z M 2570.8,647.164 2607.97,610 l 26.45,26.453 -37.16,37.164 v 0 l 13.86,-40.312 z"
+ clip-rule="evenodd"
+ id="path654" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath670">
+ <path
+ d="M 0,1490 V 0 h 3050 v 1490 z m 2603.56,-816.383 -37.17,-37.164 26.46,-26.453 37.16,37.164 v 0 l -39.68,-13.859 z"
+ clip-rule="evenodd"
+ id="path668" />
+ </clipPath>
+ </defs>
+ <sodipodi:namedview
+ id="namedview4"
+ pagecolor="#ffffff"
+ bordercolor="#000000"
+ borderopacity="0.25"
+ inkscape:showpageshadow="2"
+ inkscape:pageopacity="0.0"
+ inkscape:pagecheckerboard="0"
+ inkscape:deskcolor="#d1d1d1"
+ showgrid="false"
+ inkscape:zoom="2.4005425"
+ inkscape:cx="138.30207"
+ inkscape:cy="0.83314502"
+ inkscape:window-width="1920"
+ inkscape:window-height="1127"
+ inkscape:window-x="1920"
+ inkscape:window-y="0"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="g8" />
+ <g
+ id="g8"
+ inkscape:groupmode="layer"
+ inkscape:label="simdag-101"
+ transform="matrix(1.3333333,0,0,-1.3333333,-103.81647,182.3422)">
+ <g
+ id="g220"
+ transform="matrix(0.68033,0,0,0.68033,77.66801,35.78601)">
+ <g
+ id="g222">
+ <g
+ id="g224">
+ <g
+ id="g226">
+ <g
+ id="g228"
+ clip-path="url(#clipPath232)">
+ <g
+ id="g234"
+ transform="scale(0.1)">
+ <path
+ d="m 348.516,955.812 c 0,-55.66 -45.125,-100.781 -100.786,-100.781 -55.66,0 -100.781,45.121 -100.781,100.781 0,55.658 45.121,100.788 100.781,100.788 55.661,0 100.786,-45.13 100.786,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path236" />
+ <path
+ d="m 1624.06,955.812 c 0,-55.66 -45.12,-100.781 -100.78,-100.781 -55.66,0 -100.78,45.121 -100.78,100.781 0,55.658 45.12,100.788 100.78,100.788 55.66,0 100.78,-45.13 100.78,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path238" />
+ <path
+ d="m 2049.25,955.812 c 0,-55.66 -45.13,-100.781 -100.79,-100.781 -55.66,0 -100.78,45.121 -100.78,100.781 0,55.658 45.12,100.788 100.78,100.788 55.66,0 100.79,-45.13 100.79,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path240" />
+ <path
+ d="m 2474.43,955.812 c 0,-55.66 -45.13,-100.781 -100.79,-100.781 -55.66,0 -100.78,45.121 -100.78,100.781 0,55.658 45.12,100.788 100.78,100.788 55.66,0 100.79,-45.13 100.79,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path242" />
+ <path
+ d="m 2899.61,955.812 c 0,-55.66 -45.12,-100.781 -100.78,-100.781 -55.66,0 -100.79,45.121 -100.79,100.781 0,55.658 45.13,100.788 100.79,100.788 55.66,0 100.78,-45.13 100.78,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path244" />
+ <path
+ d="m 774.328,955.812 c 0,-55.66 -45.125,-100.781 -100.785,-100.781 -55.66,0 -100.781,45.121 -100.781,100.781 0,55.658 45.121,100.788 100.781,100.788 55.66,0 100.785,-45.13 100.785,-100.788 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path246" />
+ <path
+ d="m 1200.77,954.555 c 0,-55.66 -45.13,-100.785 -100.79,-100.785 -55.66,0 -100.777,45.125 -100.777,100.785 0,55.655 45.117,100.785 100.777,100.785 55.66,0 100.79,-45.13 100.79,-100.785 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path248" />
+ <path
+ d="m 575.281,530.633 c 0,-55.66 -45.125,-100.785 -100.785,-100.785 -55.66,0 -100.785,45.125 -100.785,100.785 0,55.66 45.125,100.781 100.785,100.781 55.66,0 100.785,-45.121 100.785,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path250" />
+ <path
+ d="m 1425.64,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.78,45.125 -100.78,100.785 0,55.66 45.12,100.781 100.78,100.781 55.66,0 100.78,-45.121 100.78,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path252" />
+ <path
+ d="m 1850.83,530.633 c 0,-55.66 -45.13,-100.785 -100.79,-100.785 -55.66,0 -100.78,45.125 -100.78,100.785 0,55.66 45.12,100.781 100.78,100.781 55.66,0 100.79,-45.121 100.79,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path254" />
+ <path
+ d="m 2701.19,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.79,45.125 -100.79,100.785 0,55.66 45.13,100.781 100.79,100.781 55.66,0 100.78,-45.121 100.78,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path256" />
+ <path
+ d="m 1000.46,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.785,45.125 -100.785,100.785 0,55.66 45.125,100.781 100.785,100.781 55.66,0 100.78,-45.121 100.78,-100.781"
+ style="fill:#bfbfbf;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path258" />
+ <path
+ d="m 1000.46,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.785,45.125 -100.785,100.785 0,55.66 45.125,100.781 100.785,100.781 55.66,0 100.78,-45.121 100.78,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path260" />
+ <path
+ d="m 1000.46,105.449 c 0,-55.6599 -45.12,-100.78494 -100.78,-100.78494 -55.66,0 -100.785,45.12504 -100.785,100.78494 0,55.66 45.125,100.785 100.785,100.785 55.66,0 100.78,-45.125 100.78,-100.785"
+ style="fill:#bfbfbf;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path262" />
+ <path
+ d="m 1000.46,105.449 c 0,-55.6599 -45.12,-100.78494 -100.78,-100.78494 -55.66,0 -100.785,45.12504 -100.785,100.78494 0,55.66 45.125,100.785 100.785,100.785 55.66,0 100.78,-45.125 100.78,-100.785 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path264" />
+ <path
+ d="m 2276.01,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.79,45.125 -100.79,100.785 0,55.66 45.13,100.781 100.79,100.781 55.66,0 100.78,-45.121 100.78,-100.781"
+ style="fill:#bfbfbf;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path266" />
+ <path
+ d="m 2276.01,530.633 c 0,-55.66 -45.12,-100.785 -100.78,-100.785 -55.66,0 -100.79,45.125 -100.79,100.785 0,55.66 45.13,100.781 100.79,100.781 55.66,0 100.78,-45.121 100.78,-100.781 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path268" />
+ <path
+ d="m 2276.01,105.449 c 0,-55.6599 -45.12,-100.78494 -100.78,-100.78494 -55.66,0 -100.79,45.12504 -100.79,100.78494 0,55.66 45.13,100.785 100.79,100.785 55.66,0 100.78,-45.125 100.78,-100.785"
+ style="fill:#bfbfbf;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path270" />
+ <path
+ d="m 2276.01,105.449 c 0,-55.6599 -45.12,-100.78494 -100.78,-100.78494 -55.66,0 -100.79,45.12504 -100.79,100.78494 0,55.66 45.13,100.785 100.79,100.785 55.66,0 100.78,-45.125 100.78,-100.785 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path272" />
+ <path
+ d="m 206.789,1381 c 0,-55.66 -45.125,-100.79 -100.785,-100.79 -55.6602,0 -100.78525,45.13 -100.78525,100.79 0,55.66 45.12505,100.78 100.78525,100.78 55.66,0 100.785,-45.12 100.785,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path274" />
+ <path
+ d="m 206.789,1381 c 0,-55.66 -45.125,-100.79 -100.785,-100.79 -55.6602,0 -100.78525,45.13 -100.78525,100.79 0,55.66 45.12505,100.78 100.78525,100.78 55.66,0 100.785,-45.12 100.785,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path276" />
+ <path
+ d="m 490.242,1381 c 0,-55.66 -45.125,-100.79 -100.785,-100.79 -55.66,0 -100.781,45.13 -100.781,100.79 0,55.66 45.121,100.78 100.781,100.78 55.66,0 100.785,-45.12 100.785,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path278" />
+ <path
+ d="m 490.242,1381 c 0,-55.66 -45.125,-100.79 -100.785,-100.79 -55.66,0 -100.781,45.13 -100.781,100.79 0,55.66 45.121,100.78 100.781,100.78 55.66,0 100.785,-45.12 100.785,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path280" />
+ <path
+ d="m 775.586,1379.74 c 0,-55.66 -45.121,-100.79 -100.781,-100.79 -55.66,0 -100.785,45.13 -100.785,100.79 0,55.66 45.125,100.78 100.785,100.78 55.66,0 100.781,-45.12 100.781,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path282" />
+ <path
+ d="m 775.586,1379.74 c 0,-55.66 -45.121,-100.79 -100.781,-100.79 -55.66,0 -100.785,45.13 -100.785,100.79 0,55.66 45.125,100.78 100.785,100.78 55.66,0 100.781,-45.12 100.781,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path284" />
+ <path
+ d="m 1198.88,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.788,45.13 -100.788,100.79 0,55.66 45.128,100.78 100.788,100.78 55.66,0 100.78,-45.12 100.78,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path286" />
+ <path
+ d="m 1198.88,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.788,45.13 -100.788,100.79 0,55.66 45.128,100.78 100.788,100.78 55.66,0 100.78,-45.12 100.78,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path288" />
+ <path
+ d="m 1482.34,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path290" />
+ <path
+ d="m 1482.34,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path292" />
+ <path
+ d="m 1765.79,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.79,45.13 -100.79,100.79 0,55.66 45.13,100.78 100.79,100.78 55.66,0 100.78,-45.12 100.78,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path294" />
+ <path
+ d="m 1765.79,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.79,45.13 -100.79,100.79 0,55.66 45.13,100.78 100.79,100.78 55.66,0 100.78,-45.12 100.78,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path296" />
+ <path
+ d="m 2049.25,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path298" />
+ <path
+ d="m 2049.25,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path300" />
+ <path
+ d="m 2474.43,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path302" />
+ <path
+ d="m 2474.43,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path304" />
+ <path
+ d="m 2757.88,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.78,-45.12 100.78,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path306" />
+ <path
+ d="m 2757.88,1381 c 0,-55.66 -45.12,-100.79 -100.78,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.78,-45.12 100.78,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path308" />
+ <path
+ d="m 3041.34,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78"
+ style="fill:#808080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path310" />
+ <path
+ d="m 3041.34,1381 c 0,-55.66 -45.13,-100.79 -100.79,-100.79 -55.66,0 -100.78,45.13 -100.78,100.79 0,55.66 45.12,100.78 100.78,100.78 55.66,0 100.79,-45.12 100.79,-100.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path312" />
+ <g
+ id="g314">
+ <g
+ id="g316"
+ clip-path="url(#clipPath320)">
+ <path
+ d="M 2614.89,431.105 2161.37,204.344"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path322" />
+ </g>
+ </g>
+ <path
+ d="m 2228.77,259.773 -58.58,-51.019 75.58,17.004 -17,34.015"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path324" />
+ <path
+ d="m 2228.77,259.773 -58.58,-51.019 75.58,17.004 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path326" />
+ <g
+ id="g328">
+ <g
+ id="g330"
+ clip-path="url(#clipPath334)">
+ <path
+ d="M 1339.35,431.105 2189.71,204.344"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path336" />
+ </g>
+ </g>
+ <path
+ d="m 2101.53,208.121 78.11,-1.258 -68.66,37.793 -9.45,-36.535"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path338" />
+ <path
+ d="m 2101.53,208.121 78.11,-1.258 -68.66,37.793 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path340" />
+ <g
+ id="g342">
+ <g
+ id="g344"
+ clip-path="url(#clipPath348)">
+ <path
+ d="M 1736.18,431.105 885.82,204.344"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path350" />
+ </g>
+ </g>
+ <path
+ d="m 963.93,244.656 -68.032,-37.793 77.477,1.258 -9.445,36.535"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path352" />
+ <path
+ d="m 963.93,244.656 -68.032,-37.793 77.477,1.258 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path354" />
+ <g
+ id="g356">
+ <g
+ id="g358"
+ clip-path="url(#clipPath362)">
+ <path
+ d="M 460.637,431.105 914.164,204.344"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path364" />
+ </g>
+ </g>
+ <path
+ d="m 829.129,225.758 76.219,-17.004 -59.211,51.019 -17.008,-34.015"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path366" />
+ <path
+ d="m 829.129,225.758 76.219,-17.004 -59.211,51.019 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path368" />
+ <g
+ id="g370">
+ <g
+ id="g372"
+ clip-path="url(#clipPath376)">
+ <path
+ d="M 92.1445,1281.47 262.219,1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path378" />
+ </g>
+ </g>
+ <path
+ d="m 221.277,1078.02 37.793,-18.9 -7.558,41.57 -30.235,-22.67"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path380" />
+ <path
+ d="m 221.277,1078.02 37.793,-18.9 -7.558,41.57 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path382" />
+ <g
+ id="g384">
+ <g
+ id="g386"
+ clip-path="url(#clipPath390)">
+ <path
+ d="M 403.945,1281.47 262.219,1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path392" />
+ </g>
+ </g>
+ <path
+ d="m 269.148,1101.32 -3.781,-42.2 35.906,22.04 -32.125,20.16"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path394" />
+ <path
+ d="m 269.148,1101.32 -3.781,-42.2 35.906,22.04 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path396" />
+ <g
+ id="g398">
+ <g
+ id="g400"
+ clip-path="url(#clipPath404)">
+ <path
+ d="M 687.402,1281.47 V 1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path406" />
+ </g>
+ </g>
+ <path
+ d="m 668.504,1098.17 18.898,-37.79 18.895,37.79 h -37.793"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path408" />
+ <path
+ d="m 668.504,1098.17 18.898,-37.79 18.895,37.79 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path410" />
+ <g
+ id="g412">
+ <g
+ id="g414"
+ clip-path="url(#clipPath418)">
+ <path
+ d="M 1112.59,1281.47 V 1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path420" />
+ </g>
+ </g>
+ <path
+ d="m 1093.69,1098.17 18.9,-37.79 18.89,37.79 h -37.79"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path422" />
+ <path
+ d="m 1093.69,1098.17 18.9,-37.79 18.89,37.79 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path424" />
+ <g
+ id="g426">
+ <g
+ id="g428"
+ clip-path="url(#clipPath432)">
+ <path
+ d="m 1396.04,1281.47 141.73,-226.76"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path434" />
+ </g>
+ </g>
+ <path
+ d="m 1498.08,1081.16 36.54,-22.04 -4.41,42.2 -32.13,-20.16"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path436" />
+ <path
+ d="m 1498.08,1081.16 36.54,-22.04 -4.41,42.2 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path438" />
+ <g
+ id="g440">
+ <g
+ id="g442"
+ clip-path="url(#clipPath446)">
+ <path
+ d="M 1679.5,1281.47 1537.77,1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path448" />
+ </g>
+ </g>
+ <path
+ d="m 1544.7,1101.32 -3.78,-42.2 35.9,22.04 -32.12,20.16"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path450" />
+ <path
+ d="m 1544.7,1101.32 -3.78,-42.2 35.9,22.04 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path452" />
+ <g
+ id="g454">
+ <g
+ id="g456"
+ clip-path="url(#clipPath460)">
+ <path
+ d="M 1962.95,1281.47 V 1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path462" />
+ </g>
+ </g>
+ <path
+ d="m 1944.05,1098.17 18.9,-37.79 18.9,37.79 h -37.8"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path464" />
+ <path
+ d="m 1944.05,1098.17 18.9,-37.79 18.9,37.79 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path466" />
+ <g
+ id="g468">
+ <g
+ id="g470"
+ clip-path="url(#clipPath474)">
+ <path
+ d="M 2388.13,1281.47 V 1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path476" />
+ </g>
+ </g>
+ <path
+ d="m 2369.23,1098.17 18.9,-37.79 18.9,37.79 h -37.8"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path478" />
+ <path
+ d="m 2369.23,1098.17 18.9,-37.79 18.9,37.79 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path480" />
+ <g
+ id="g482">
+ <g
+ id="g484"
+ clip-path="url(#clipPath488)">
+ <path
+ d="m 2643.24,1281.47 170.07,-226.76"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path490" />
+ </g>
+ </g>
+ <path
+ d="m 2772.37,1078.02 37.79,-18.9 -7.55,41.57 -30.24,-22.67"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path492" />
+ <path
+ d="m 2772.37,1078.02 37.79,-18.9 -7.55,41.57 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path494" />
+ <g
+ id="g496">
+ <g
+ id="g498"
+ clip-path="url(#clipPath502)">
+ <path
+ d="M 2955.04,1281.47 2813.31,1054.71"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path504" />
+ </g>
+ </g>
+ <path
+ d="m 2820.24,1101.32 -3.78,-42.2 35.91,22.04 -32.13,20.16"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path506" />
+ <path
+ d="m 2820.24,1101.32 -3.78,-42.2 35.91,22.04 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path508" />
+ <g
+ id="g510">
+ <g
+ id="g512"
+ clip-path="url(#clipPath516)">
+ <path
+ d="M 262.219,856.289 488.984,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path518" />
+ </g>
+ </g>
+ <path
+ d="m 444.891,647.164 40.312,-13.859 -13.855,40.312 -26.457,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path520" />
+ <path
+ d="m 444.891,647.164 40.312,-13.859 -13.855,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path522" />
+ <g
+ id="g524">
+ <g
+ id="g526"
+ clip-path="url(#clipPath530)">
+ <path
+ d="M 687.402,856.289 460.637,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path532" />
+ </g>
+ </g>
+ <path
+ d="m 477.645,673.617 -13.227,-40.312 39.684,13.859 -26.457,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path534" />
+ <path
+ d="m 477.645,673.617 -13.227,-40.312 39.684,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path536" />
+ <g
+ id="g538">
+ <g
+ id="g540"
+ clip-path="url(#clipPath544)">
+ <path
+ d="M 687.402,856.289 914.164,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path546" />
+ </g>
+ </g>
+ <path
+ d="m 870.074,647.164 40.313,-13.859 -13.86,40.312 -26.453,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path548" />
+ <path
+ d="m 870.074,647.164 40.313,-13.859 -13.86,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path550" />
+ <g
+ id="g552">
+ <g
+ id="g554"
+ clip-path="url(#clipPath558)">
+ <path
+ d="M 1112.59,856.289 885.82,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path560" />
+ </g>
+ </g>
+ <path
+ d="m 902.828,673.617 -13.23,-40.312 39.687,13.859 -26.457,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path562" />
+ <path
+ d="m 902.828,673.617 -13.23,-40.312 39.687,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path564" />
+ <g
+ id="g566">
+ <g
+ id="g568"
+ clip-path="url(#clipPath572)">
+ <path
+ d="M 1112.59,856.289 1339.35,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path574" />
+ </g>
+ </g>
+ <path
+ d="m 1295.25,647.164 40.32,-13.859 -13.86,40.312 -26.46,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path576" />
+ <path
+ d="m 1295.25,647.164 40.32,-13.859 -13.86,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path578" />
+ <g
+ id="g580">
+ <g
+ id="g582"
+ clip-path="url(#clipPath586)">
+ <path
+ d="M 1537.77,856.289 1311,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path588" />
+ </g>
+ </g>
+ <path
+ d="m 1328.01,673.617 -13.23,-40.312 39.68,13.859 -26.45,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path590" />
+ <path
+ d="m 1328.01,673.617 -13.23,-40.312 39.68,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path592" />
+ <g
+ id="g594">
+ <g
+ id="g596"
+ clip-path="url(#clipPath600)">
+ <path
+ d="M 1537.77,856.289 1764.53,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path602" />
+ </g>
+ </g>
+ <path
+ d="m 1720.44,647.164 40.31,-13.859 -13.86,40.312 -26.45,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path604" />
+ <path
+ d="m 1720.44,647.164 40.31,-13.859 -13.86,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path606" />
+ <g
+ id="g608">
+ <g
+ id="g610"
+ clip-path="url(#clipPath614)">
+ <path
+ d="M 1962.95,856.289 1736.18,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path616" />
+ </g>
+ </g>
+ <path
+ d="m 1753.19,673.617 -13.23,-40.312 39.69,13.859 -26.46,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path618" />
+ <path
+ d="m 1753.19,673.617 -13.23,-40.312 39.69,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path620" />
+ <g
+ id="g622">
+ <g
+ id="g624"
+ clip-path="url(#clipPath628)">
+ <path
+ d="M 1962.95,856.289 2189.71,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path630" />
+ </g>
+ </g>
+ <path
+ d="m 2145.62,647.164 40.31,-13.859 -13.86,40.312 -26.45,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path632" />
+ <path
+ d="m 2145.62,647.164 40.31,-13.859 -13.86,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path634" />
+ <g
+ id="g636">
+ <g
+ id="g638"
+ clip-path="url(#clipPath642)">
+ <path
+ d="M 2388.13,856.289 2161.37,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path644" />
+ </g>
+ </g>
+ <path
+ d="m 2178.38,673.617 -13.23,-40.312 39.68,13.859 -26.45,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path646" />
+ <path
+ d="m 2178.38,673.617 -13.23,-40.312 39.68,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path648" />
+ <g
+ id="g650">
+ <g
+ id="g652"
+ clip-path="url(#clipPath656)">
+ <path
+ d="M 2388.13,856.289 2614.89,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path658" />
+ </g>
+ </g>
+ <path
+ d="m 2570.8,647.164 40.32,-13.859 -13.86,40.312 -26.46,-26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path660" />
+ <path
+ d="m 2570.8,647.164 40.32,-13.859 -13.86,40.312 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path662" />
+ <g
+ id="g664">
+ <g
+ id="g666"
+ clip-path="url(#clipPath670)">
+ <path
+ d="M 2813.31,856.289 2586.55,629.527"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path672" />
+ </g>
+ </g>
+ <path
+ d="m 2603.56,673.617 -13.23,-40.312 39.68,13.859 -26.45,26.453"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path674" />
+ <path
+ d="m 2603.56,673.617 -13.23,-40.312 39.68,13.859 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path676" />
+ <g
+ id="g678"
+ transform="scale(10)">
+ <text
+ xml:space="preserve"
+ transform="matrix(1,0,0,-1,9.21445,133.816)"
+ style="font-variant:normal;font-weight:normal;font-size:11.3382px;font-family:Times;-inkscape-font-specification:Times-Roman;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ id="text688"><tspan
+ x="0 28.345726 56.691002 99.209366 127.55509 155.90036 184.24609 226.76401 255.10973 277.78589 283.45499"
+ y="0"
+ sodipodi:role="line"
+ id="tspan680">12345678910</tspan><tspan
+ x="8.5039101 14.17301 51.02182 56.690918 93.540184 99.209282 136.05855 141.72765 178.5769 184.24602 221.09494 226.76404 263.61331 269.28241"
+ y="42.518398"
+ sodipodi:role="line"
+ id="tspan682">11121314151617</tspan><tspan
+ x="31.180111 36.849209 73.698471 79.367577 119.05116 124.72026 161.56952 167.23862 204.08789 209.75699 246.60579 252.2749"
+ y="85.036797"
+ sodipodi:role="line"
+ id="tspan684">181920212223</tspan><tspan
+ x="201.25311 206.92221 73.698112 79.36721"
+ y="127.5548"
+ sodipodi:role="line"
+ id="tspan686">2524</tspan></text>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+</svg>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+ version="1.1"
+ id="svg2"
+ width="63.57653"
+ height="70.614357"
+ viewBox="0 0 63.576531 70.614358"
+ sodipodi:docname="simdag-101.pdf"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:svg="http://www.w3.org/2000/svg">
+ <defs
+ id="defs6">
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath162">
+ <path
+ d="M 0,0 H 130 V 144 H 0 Z"
+ id="path160" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath176">
+ <path
+ d="M 0,1440 V 0 h 1300 v 1440 z m 307.016,-526.48 59.211,-74.329 29.605,23.934 -59.211,74.328 v 0 l 32.754,-71.176 z"
+ clip-rule="evenodd"
+ id="path174" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath190">
+ <path
+ d="M 0,1440 V 0 h 1300 v 1440 z m 558.977,-1097.172 63.617,-71.176 28.347,25.196 -63.621,71.175 v 0 l 36.535,-69.289 z"
+ clip-rule="evenodd"
+ id="path188" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath204">
+ <path
+ d="M 0,1440 V 0 h 1300 v 1440 z m 658.5,-1065.047 -49.133,-81.887 32.754,-19.527 48.504,81.887 v 0 l -54.801,-55.43 z"
+ clip-rule="evenodd"
+ id="path202" />
+ </clipPath>
+ </defs>
+ <sodipodi:namedview
+ id="namedview4"
+ pagecolor="#ffffff"
+ bordercolor="#000000"
+ borderopacity="0.25"
+ inkscape:showpageshadow="2"
+ inkscape:pageopacity="0.0"
+ inkscape:pagecheckerboard="0"
+ inkscape:deskcolor="#d1d1d1"
+ showgrid="false" />
+ <g
+ id="g8"
+ inkscape:groupmode="layer"
+ inkscape:label="simdag-101"
+ transform="matrix(1.3333333,0,0,-1.3333333,-355.80477,212.98189)">
+ <g
+ id="g150"
+ transform="matrix(0.37244,0,0,0.37244,266.67401,106.57601)">
+ <g
+ id="g152">
+ <g
+ id="g154">
+ <g
+ id="g156">
+ <g
+ id="g158"
+ clip-path="url(#clipPath162)">
+ <g
+ id="g164"
+ transform="scale(0.1)">
+ <path
+ d="m 517.402,716.359 c 0,-78.273 -63.453,-141.726 -141.726,-141.726 -78.274,0 -141.731,63.453 -141.731,141.726 0,78.274 63.457,141.727 141.731,141.727 78.273,0 141.726,-63.453 141.726,-141.727"
+ style="fill:#ff8080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path166" />
+ <path
+ d="m 517.402,716.359 c 0,-78.273 -63.453,-141.726 -141.726,-141.726 -78.274,0 -141.731,63.453 -141.731,141.726 0,78.274 63.457,141.727 141.731,141.727 78.273,0 141.726,-63.453 141.726,-141.727 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path168" />
+ <g
+ id="g170">
+ <g
+ id="g172"
+ clip-path="url(#clipPath176)">
+ <path
+ d="M 148.91,1141.54 375.676,858.086"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path178" />
+ </g>
+ </g>
+ <path
+ d="m 307.016,913.52 62.359,-47.243 -32.754,71.176 -29.605,-23.933"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path180" />
+ <path
+ d="m 307.016,913.52 62.359,-47.243 -32.754,71.176 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path182" />
+ <g
+ id="g184">
+ <g
+ id="g186"
+ clip-path="url(#clipPath190)">
+ <path
+ d="M 375.676,574.633 630.785,291.176"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path192" />
+ </g>
+ </g>
+ <path
+ d="m 558.977,342.828 64.878,-44.094 -36.535,69.289 -28.343,-25.195"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path194" />
+ <path
+ d="m 558.977,342.828 64.878,-44.094 -36.535,69.289 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path196" />
+ <g
+ id="g198">
+ <g
+ id="g200"
+ clip-path="url(#clipPath204)">
+ <path
+ d="M 1141,1141.54 630.785,291.176"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path206" />
+ </g>
+ </g>
+ <path
+ d="m 658.5,374.953 -22.676,-74.957 54.801,55.43 -32.125,19.527"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path208" />
+ <path
+ d="m 658.5,374.953 -22.676,-74.957 54.801,55.43 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path210" />
+ <path
+ d="m 7.18359,1141.54 h 283.453 v 283.453 H 7.18359 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path212" />
+ <path
+ d="m 7.18359,1141.54 h 283.453 v 283.453 H 7.18359 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path214" />
+ <path
+ d="m 999.273,1141.54 h 283.457 v 283.453 H 999.273 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path216" />
+ <path
+ d="m 999.273,1141.54 h 283.457 v 283.453 H 999.273 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path218" />
+ <path
+ d="m 489.055,7.72266 h 283.457 v 283.453 H 489.055 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path220" />
+ <path
+ d="m 489.055,7.72266 h 283.457 v 283.453 H 489.055 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path222" />
+ <g
+ id="g224"
+ transform="scale(10)">
+ <text
+ xml:space="preserve"
+ transform="matrix(1,0,0,-1,31.8984,65.9668)"
+ style="font-variant:normal;font-weight:bold;font-size:13.2279px;font-family:Times;-inkscape-font-specification:Times-Bold;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ id="text232"><tspan
+ x="0 4.4048905"
+ y="0"
+ sodipodi:role="line"
+ id="tspan226">t1</tspan><tspan
+ x="-22.6766 -16.803411 76.532784 82.405968"
+ y="-56.691002"
+ sodipodi:role="line"
+ id="tspan228">c1c2</tspan><tspan
+ x="25.5109 31.384089"
+ y="56.691002"
+ sodipodi:role="line"
+ id="tspan230">c3</tspan></text>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+</svg>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+ version="1.1"
+ id="svg2"
+ width="63.701672"
+ height="183.22269"
+ viewBox="0 0 63.701672 183.22269"
+ sodipodi:docname="simdag-101.pdf"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:svg="http://www.w3.org/2000/svg">
+ <defs
+ id="defs6">
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath182">
+ <path
+ d="M 0,0 H 130 V 371 H 0 Z"
+ id="path180" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath196">
+ <path
+ d="M 0,3710 V 0 h 1300 v 3710 z m 307.016,-1662.48 59.211,-74.33 29.605,23.93 -59.211,74.33 v 0 l 32.754,-71.17 z"
+ clip-rule="evenodd"
+ id="path194" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath210">
+ <path
+ d="M 0,3710 V 0 h 1300 v 3710 z m 558.977,-2233.17 63.617,-71.18 28.347,25.2 -63.621,71.17 v 0 l 36.535,-69.29 z"
+ clip-rule="evenodd"
+ id="path208" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath224">
+ <path
+ d="M 0,3710 V 0 h 1300 v 3710 z m 658.5,-2201.05 -49.133,-81.88 32.754,-19.53 48.504,81.89 v 0 L 635.824,1434 Z"
+ clip-rule="evenodd"
+ id="path222" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath272">
+ <path
+ d="M 0,3710 V 0 H 1300 V 3710 Z M 611.887,377.023 V 281.91 h 37.793 v 95.113 0 l -18.895,-75.585 z"
+ clip-rule="evenodd"
+ id="path270" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath286">
+ <path
+ d="M 0,3710 V 0 h 1300 v 3710 z m 1057.23,-557.01 81.88,-47.87 19.53,32.76 -82.52,47.87 v 0 l 56.06,-54.8 z"
+ clip-rule="evenodd"
+ id="path284" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath300">
+ <path
+ d="M 0,3710 V 0 h 1300 v 3710 z m 214.418,-525.51 -83.145,-46.61 18.266,-32.76 83.149,46.61 v 0 l -74.958,-20.78 z"
+ clip-rule="evenodd"
+ id="path298" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath322">
+ <path
+ d="M 0,3710 V 0 H 1300 V 3710 Z M 611.887,943.934 V 848.82 h 37.793 v 95.114 0 l -18.895,-75.586 z"
+ clip-rule="evenodd"
+ id="path320" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath336">
+ <path
+ d="M 0,3710 V 0 H 1300 V 3710 Z M 1122.11,2644.66 v -95.11 h 37.79 v 95.11 0 l -18.9,-75.59 z"
+ clip-rule="evenodd"
+ id="path334" />
+ </clipPath>
+ <clipPath
+ clipPathUnits="userSpaceOnUse"
+ id="clipPath350">
+ <path
+ d="M 0,3710 V 0 H 1300 V 3710 Z M 130.012,2644.66 v -95.11 h 37.797 v 95.11 0 l -18.899,-75.59 z"
+ clip-rule="evenodd"
+ id="path348" />
+ </clipPath>
+ </defs>
+ <sodipodi:namedview
+ id="namedview4"
+ pagecolor="#ffffff"
+ bordercolor="#000000"
+ borderopacity="0.25"
+ inkscape:showpageshadow="2"
+ inkscape:pageopacity="0.0"
+ inkscape:pagecheckerboard="0"
+ inkscape:deskcolor="#d1d1d1"
+ showgrid="false" />
+ <g
+ id="g8"
+ inkscape:groupmode="layer"
+ inkscape:label="simdag-101"
+ transform="matrix(1.3333333,0,0,-1.3333333,-355.80477,267.77649)">
+ <g
+ id="g170"
+ transform="matrix(0.37244,0,0,0.37244,266.67401,63.20901)">
+ <g
+ id="g172">
+ <g
+ id="g174">
+ <g
+ id="g176">
+ <g
+ id="g178"
+ clip-path="url(#clipPath182)">
+ <g
+ id="g184"
+ transform="scale(0.1)">
+ <path
+ d="m 517.402,1850.36 c 0,-78.27 -63.453,-141.73 -141.726,-141.73 -78.274,0 -141.731,63.46 -141.731,141.73 0,78.27 63.457,141.73 141.731,141.73 78.273,0 141.726,-63.46 141.726,-141.73"
+ style="fill:#ff8080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path186" />
+ <path
+ d="m 517.402,1850.36 c 0,-78.27 -63.453,-141.73 -141.726,-141.73 -78.274,0 -141.731,63.46 -141.731,141.73 0,78.27 63.457,141.73 141.731,141.73 78.273,0 141.726,-63.46 141.726,-141.73 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path188" />
+ <g
+ id="g190">
+ <g
+ id="g192"
+ clip-path="url(#clipPath196)">
+ <path
+ d="M 148.91,2275.54 375.676,1992.09"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path198" />
+ </g>
+ </g>
+ <path
+ d="m 307.016,2047.52 62.359,-47.24 -32.754,71.17 -29.605,-23.93"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path200" />
+ <path
+ d="m 307.016,2047.52 62.359,-47.24 -32.754,71.17 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path202" />
+ <g
+ id="g204">
+ <g
+ id="g206"
+ clip-path="url(#clipPath210)">
+ <path
+ d="M 375.676,1708.63 630.785,1425.18"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path212" />
+ </g>
+ </g>
+ <path
+ d="m 558.977,1476.83 64.878,-44.1 -36.535,69.29 -28.343,-25.19"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path214" />
+ <path
+ d="m 558.977,1476.83 64.878,-44.1 -36.535,69.29 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path216" />
+ <g
+ id="g218">
+ <g
+ id="g220"
+ clip-path="url(#clipPath224)">
+ <path
+ d="M 1141,2275.54 630.785,1425.18"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path226" />
+ </g>
+ </g>
+ <path
+ d="m 658.5,1508.95 -22.676,-74.95 54.801,55.43 -32.125,19.52"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path228" />
+ <path
+ d="m 658.5,1508.95 -22.676,-74.95 54.801,55.43 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path230" />
+ <path
+ d="m 7.18359,2275.54 h 283.453 v 283.453 H 7.18359 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path232" />
+ <path
+ d="m 7.18359,2275.54 h 283.453 v 283.453 H 7.18359 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path234" />
+ <path
+ d="m 999.273,2275.54 h 283.457 v 283.453 H 999.273 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path236" />
+ <path
+ d="m 999.273,2275.54 h 283.457 v 283.453 H 999.273 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path238" />
+ <path
+ d="m 489.055,1141.72 h 283.457 v 283.453 H 489.055 Z"
+ style="fill:#8080ff;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path240" />
+ <path
+ d="m 489.055,1141.72 h 283.457 v 283.453 H 489.055 Z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path242" />
+ <g
+ id="g244"
+ transform="scale(10)">
+ <text
+ xml:space="preserve"
+ transform="matrix(1,0,0,-1,31.8984,179.367)"
+ style="font-variant:normal;font-weight:bold;font-size:13.2279px;font-family:Times;-inkscape-font-specification:Times-Bold;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
+ id="text252"><tspan
+ x="0 4.4048905"
+ y="0"
+ sodipodi:role="line"
+ id="tspan246">t1</tspan><tspan
+ x="-22.6766 -16.803411 76.532784 82.405968"
+ y="-56.691002"
+ sodipodi:role="line"
+ id="tspan248">c1c2</tspan><tspan
+ x="25.5109 31.384089"
+ y="56.691002"
+ sodipodi:role="line"
+ id="tspan250">c3</tspan></text>
+ </g>
+ <path
+ d="m 768.73,714.02 c 0,-78.274 -63.453,-141.727 -141.726,-141.727 -78.274,0 -141.727,63.453 -141.727,141.727 0,78.273 63.453,141.726 141.727,141.726 78.273,0 141.726,-63.453 141.726,-141.726"
+ style="fill:#ff8080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path254" />
+ <path
+ d="m 768.73,714.02 c 0,-78.274 -63.453,-141.727 -141.726,-141.727 -78.274,0 -141.727,63.453 -141.727,141.727 0,78.273 63.453,141.726 141.727,141.726 78.273,0 141.726,-63.453 141.726,-141.726 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path256" />
+ <path
+ d="m 1285.25,2983.55 c 0,-78.27 -63.45,-141.73 -141.73,-141.73 -78.27,0 -141.73,63.46 -141.73,141.73 0,78.27 63.46,141.73 141.73,141.73 78.28,0 141.73,-63.46 141.73,-141.73"
+ style="fill:#ff8080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path258" />
+ <path
+ d="m 1285.25,2983.55 c 0,-78.27 -63.45,-141.73 -141.73,-141.73 -78.27,0 -141.73,63.46 -141.73,141.73 0,78.27 63.46,141.73 141.73,141.73 78.28,0 141.73,-63.46 141.73,-141.73 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path260" />
+ <path
+ d="m 290.637,2984.18 c 0,-78.27 -63.453,-141.73 -141.727,-141.73 -78.2733,0 -141.72641,63.46 -141.72641,141.73 0,78.27 63.45311,141.73 141.72641,141.73 78.274,0 141.727,-63.46 141.727,-141.73"
+ style="fill:#ff8080;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path262" />
+ <path
+ d="m 290.637,2984.18 c 0,-78.27 -63.453,-141.73 -141.727,-141.73 -78.2733,0 -141.72641,63.46 -141.72641,141.73 0,78.27 63.45311,141.73 141.72641,141.73 78.274,0 141.727,-63.46 141.727,-141.73 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path264" />
+ <g
+ id="g266">
+ <g
+ id="g268"
+ clip-path="url(#clipPath272)">
+ <path
+ d="M 630.785,574.812 V 291.355"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path274" />
+ </g>
+ </g>
+ <path
+ d="m 611.887,377.023 18.898,-75.585 18.895,75.585 h -37.793"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path276" />
+ <path
+ d="m 611.887,377.023 18.898,-75.585 18.895,75.585 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path278" />
+ <g
+ id="g280">
+ <g
+ id="g282"
+ clip-path="url(#clipPath286)">
+ <path
+ d="M 659.129,3409.36 1141,3125.91"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path288" />
+ </g>
+ </g>
+ <path
+ d="m 1057.23,3152.99 74.95,-22.04 -56.06,54.8 -18.89,-32.76"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path290" />
+ <path
+ d="m 1057.23,3152.99 74.95,-22.04 -56.06,54.8 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path292" />
+ <g
+ id="g294">
+ <g
+ id="g296"
+ clip-path="url(#clipPath300)">
+ <path
+ d="M 659.129,3409.36 148.91,3125.91"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path302" />
+ </g>
+ </g>
+ <path
+ d="m 214.418,3184.49 -56.688,-53.54 74.958,20.78 -18.27,32.76"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path304" />
+ <path
+ d="m 214.418,3184.49 -56.688,-53.54 74.958,20.78 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path306" />
+ <path
+ d="m 498.504,3692.82 v 0 c -36.527,0 -66.141,-29.62 -66.141,-66.14 V 3475.5 c 0,-36.52 29.614,-66.14 66.141,-66.14 h 292.902 c 36.528,0 66.141,29.62 66.141,66.14 v 151.18 c 0,36.52 -29.613,66.14 -66.141,66.14"
+ style="fill:#ffff80;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path308" />
+ <path
+ d="m 498.504,3692.82 v 0 c -36.527,0 -66.141,-29.62 -66.141,-66.14 V 3475.5 c 0,-36.52 29.614,-66.14 66.141,-66.14 h 292.902 c 36.528,0 66.141,29.62 66.141,66.14 v 151.18 c 0,36.52 -29.613,66.14 -66.141,66.14 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path310" />
+ <path
+ d="m 498.504,291.355 v 0 c -36.527,0 -66.141,-29.613 -66.141,-66.136 V 74.043 c 0,-36.5274 29.614,-66.14066 66.141,-66.14066 h 292.902 c 36.528,0 66.141,29.61326 66.141,66.14066 v 151.176 c 0,36.523 -29.613,66.136 -66.141,66.136"
+ style="fill:#ffff80;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path312" />
+ <path
+ d="m 498.504,291.355 v 0 c -36.527,0 -66.141,-29.613 -66.141,-66.136 V 74.043 c 0,-36.5274 29.614,-66.14066 66.141,-66.14066 h 292.902 c 36.528,0 66.141,29.61326 66.141,66.14066 v 151.176 c 0,36.523 -29.613,66.136 -66.141,66.136 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path314" />
+ <g
+ id="g316">
+ <g
+ id="g318"
+ clip-path="url(#clipPath322)">
+ <path
+ d="M 630.785,1141.72 V 858.266"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path324" />
+ </g>
+ </g>
+ <path
+ d="m 611.887,943.934 18.898,-75.586 18.895,75.586 h -37.793"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path326" />
+ <path
+ d="m 611.887,943.934 18.898,-75.586 18.895,75.586 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path328" />
+ <g
+ id="g330">
+ <g
+ id="g332"
+ clip-path="url(#clipPath336)">
+ <path
+ d="M 1141,2842.45 V 2559"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path338" />
+ </g>
+ </g>
+ <path
+ d="m 1122.11,2644.66 18.89,-75.59 18.9,75.59 h -37.79"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path340" />
+ <path
+ d="m 1122.11,2644.66 18.89,-75.59 18.9,75.59 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path342" />
+ <g
+ id="g344">
+ <g
+ id="g346"
+ clip-path="url(#clipPath350)">
+ <path
+ d="M 148.91,2842.45 V 2559"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path352" />
+ </g>
+ </g>
+ <path
+ d="m 130.012,2644.66 18.898,-75.59 18.899,75.59 h -37.797"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:none"
+ id="path354" />
+ <path
+ d="m 130.012,2644.66 18.898,-75.59 18.899,75.59 z"
+ style="fill:none;stroke:#000000;stroke-width:4.72425;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
+ id="path356" />
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+ </g>
+</svg>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<adag xmlns="http://pegasus.isi.edu/schema/DAX" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:schemaLocation="http://pegasus.isi.edu/schema/DAX http://pegasus.isi.edu/schema/dax-2.1.xsd"
+ version="2.1">
+ <job id="1" name="c1" runtime="10">
+ <uses file="i1" link="input" register="true" transfer="true" optional="false" type="data" size="2e8"/>
+ <uses file="o1" link="output" register="true" transfer="true" optional="false" type="data" size="5e8"/>
+ </job>
+ <job id="2" name="c2" runtime="50">
+ <uses file="i2" link="input" register="true" transfer="true" optional="false" type="data" size="1e8"/>
+ </job>
+ <job id="3" name="c3" runtime="20">
+ <uses file="o1" link="input" register="true" transfer="true" optional="false" type="data" size="5e8"/>
+ <uses file="o3" link="output" register="true" transfer="true" optional="false" type="data" size="2e8"/>
+ </job>
+ <child ref="3">
+ <parent ref="1"/>
+ <parent ref="2"/>
+ </child>
+</adag>
--- /dev/null
+digraph G {
+ c1 [size="1e9"];
+ c2 [size="5e9"];
+ c3 [size="2e9"];
+ root->c1 [size="2e8"];
+ root->c2 [size="1e8"];
+ c1->c3 [size="5e8"];
+ c2->c3 [size="-1."];
+ c3->end [size="2e8"];
+}
--- /dev/null
+{
+ "name": "simple_json",
+ "schemaVersion": "1.0",
+ "workflow": {
+ "makespan": 0,
+ "executedAt": "2023-03-09T00:00:00-00:00",
+ "tasks": [
+ {
+ "name": "c1",
+ "type": "compute",
+ "parents": [],
+ "runtime": 1e9,
+ "machine": "Tremblay"
+ },
+ {
+ "name": "t1",
+ "type": "transfer",
+ "parents": ["c1"],
+ "bytesWritten": 5e8,
+ "machine": "Jupiter"
+ },
+ {
+ "name": "c2",
+ "type": "compute",
+ "parents": [],
+ "runtime": 5e9,
+ "machine": "Jupiter"
+ },
+ {
+ "name": "c3",
+ "type": "compute",
+ "parents": ["t1","c2"],
+ "runtime": 2e9,
+ "machine": "Jupiter"
+ }
+ ],
+ "machines": [
+ {"nodeName": "Tremblay"},
+ {"nodeName": "Jupiter"}
+ ]
+ }
+}
\ No newline at end of file
--- /dev/null
+<?xml version='1.0'?>
+<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
+<platform version="4.1">
+ <zone id="zone0" routing="Full">
+ <host id="Tremblay" speed="98.095Mf"/>
+ <host id="Jupiter" speed="76.296Mf"/>
+ <host id="Fafard" speed="76.296Mf"/>
+ <host id="Ginette" speed="48.492Mf"/>
+ <host id="Bourassa" speed="48.492Mf"/>
+ <host id="Jacquelin" speed="137.333Mf"/>
+ <host id="Boivin" speed="98.095Mf"/>
+
+ <link id="6" bandwidth="41.279125MBps" latency="59.904us"/>
+ <link id="3" bandwidth="34.285625MBps" latency="514.433us"/>
+ <link id="7" bandwidth="11.618875MBps" latency="189.98us"/>
+ <link id="9" bandwidth="7.20975MBps" latency="1.461517ms"/>
+ <link id="2" bandwidth="118.6825MBps" latency="136.931us"/>
+ <link id="8" bandwidth="8.158MBps" latency="270.544us"/>
+ <link id="1" bandwidth="34.285625MBps" latency="514.433us"/>
+ <link id="4" bandwidth="10.099625MBps" latency="479.78us"/>
+ <link id="0" bandwidth="41.279125MBps" latency="59.904us"/>
+ <link id="5" bandwidth="27.94625MBps" latency="278.066us"/>
+ <link id="145" bandwidth="2.583375MBps" latency="410.463us"/>
+ <link id="10" bandwidth="34.285625MBps" latency="514.433us"/>
+ <link id="11" bandwidth="118.6825MBps" latency="136.931us"/>
+ <link id="16" bandwidth="34.285625MBps" latency="514.433us"/>
+ <link id="17" bandwidth="118.6825MBps" latency="136.931us"/>
+ <link id="44" bandwidth="10.314625MBps" latency="6.932556ms"/>
+ <link id="47" bandwidth="10.314625MBps" latency="6.932556ms"/>
+ <link id="54" bandwidth="15.376875MBps" latency="35.083019ms"/>
+ <link id="56" bandwidth="21.41475MBps" latency="29.5890617ms"/>
+ <link id="59" bandwidth="11.845375MBps" latency="370.788us"/>
+ <link id="78" bandwidth="27.94625MBps" latency="278.066us"/>
+ <link id="79" bandwidth="8.42725MBps" latency="156.056us"/>
+ <link id="80" bandwidth="15.376875MBps" latency="35.083019ms"/>
+ <link id="loopback" bandwidth="498MBps" latency="15us" sharing_policy="FATPIPE"/>
+
+ <route src="Tremblay" dst="Tremblay">
+ <link_ctn id="loopback"/>
+ </route>
+ <route src="Jupiter" dst="Jupiter">
+ <link_ctn id="loopback"/>
+ </route>
+ <route src="Fafard" dst="Fafard">
+ <link_ctn id="loopback"/>
+ </route>
+ <route src="Ginette" dst="Ginette">
+ <link_ctn id="loopback"/>
+ </route>
+ <route src="Bourassa" dst="Bourassa">
+ <link_ctn id="loopback"/>
+ </route>
+ <route src="Tremblay" dst="Jupiter">
+ <link_ctn id="9"/>
+ </route>
+ <route src="Tremblay" dst="Fafard">
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="2"/>
+ <link_ctn id="0"/>
+ <link_ctn id="1"/>
+ <link_ctn id="8"/>
+ </route>
+ <route src="Tremblay" dst="Ginette">
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="5"/>
+ </route>
+ <route src="Tremblay" dst="Bourassa">
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="2"/>
+ <link_ctn id="0"/>
+ <link_ctn id="1"/>
+ <link_ctn id="6"/>
+ <link_ctn id="7"/>
+ </route>
+ <route src="Jupiter" dst="Fafard">
+ <link_ctn id="9"/>
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="2"/>
+ <link_ctn id="0"/>
+ <link_ctn id="1"/>
+ <link_ctn id="8"/>
+ </route>
+ <route src="Jupiter" dst="Bourassa">
+ <link_ctn id="9"/>
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="2"/>
+ <link_ctn id="0"/>
+ <link_ctn id="1"/>
+ <link_ctn id="6"/>
+ <link_ctn id="7"/>
+ </route>
+ <route src="Fafard" dst="Ginette">
+ <link_ctn id="8"/>
+ <link_ctn id="1"/>
+ <link_ctn id="0"/>
+ <link_ctn id="2"/>
+ <link_ctn id="5"/>
+ </route>
+ <route src="Jupiter" dst="Jacquelin">
+ <link_ctn id="145"/>
+ </route>
+ <route src="Jupiter" dst="Boivin">
+ <link_ctn id="47"/>
+ </route>
+ <route src="Jupiter" dst="Ginette">
+ <link_ctn id="9"/>
+ <link_ctn id="4"/>
+ <link_ctn id="3"/>
+ <link_ctn id="5"/>
+ </route>
+ <route src="Fafard" dst="Bourassa">
+ <link_ctn id="8"/>
+ <link_ctn id="6"/>
+ <link_ctn id="7"/>
+ </route>
+ <route src="Ginette" dst="Bourassa">
+ <link_ctn id="5"/>
+ <link_ctn id="2"/>
+ <link_ctn id="0"/>
+ <link_ctn id="1"/>
+ <link_ctn id="6"/>
+ <link_ctn id="7"/>
+ </route>
+ <route src="Ginette" dst="Jacquelin">
+ <link_ctn id="145"/>
+ </route>
+ <route src="Ginette" dst="Boivin">
+ <link_ctn id="47"/>
+ </route>
+ <route src="Bourassa" dst="Jacquelin">
+ <link_ctn id="145"/>
+ </route>
+ <route src="Bourassa" dst="Boivin">
+ <link_ctn id="47"/>
+ </route>
+ <route src="Jacquelin" dst="Boivin">
+ <link_ctn id="145"/>
+ <link_ctn id="59"/>
+ <link_ctn id="56"/>
+ <link_ctn id="54"/>
+ <link_ctn id="17"/>
+ <link_ctn id="16"/>
+ <link_ctn id="10"/>
+ <link_ctn id="11"/>
+ <link_ctn id="44"/>
+ <link_ctn id="47"/>
+ </route>
+ <route src="Jacquelin" dst="Fafard">
+ <link_ctn id="145"/>
+ <link_ctn id="59"/>
+ <link_ctn id="56"/>
+ <link_ctn id="54"/>
+ <link_ctn id="17"/>
+ <link_ctn id="16"/>
+ <link_ctn id="10"/>
+ <link_ctn id="6"/>
+ <link_ctn id="9"/>
+ <link_ctn id="79"/>
+ <link_ctn id="78"/>
+ </route>
+ <route src="Jacquelin" dst="Tremblay">
+ <link_ctn id="145"/>
+ <link_ctn id="59"/>
+ <link_ctn id="56"/>
+ <link_ctn id="54"/>
+ <link_ctn id="2"/>
+ <link_ctn id="3"/>
+ </route>
+ <route src="Boivin" dst="Tremblay">
+ <link_ctn id="47"/>
+ <link_ctn id="44"/>
+ <link_ctn id="11"/>
+ <link_ctn id="10"/>
+ <link_ctn id="16"/>
+ <link_ctn id="0"/>
+ <link_ctn id="3"/>
+ </route>
+ <route src="Boivin" dst="Fafard">
+ <link_ctn id="47"/>
+ <link_ctn id="44"/>
+ <link_ctn id="11"/>
+ <link_ctn id="6"/>
+ <link_ctn id="9"/>
+ <link_ctn id="79"/>
+ <link_ctn id="78"/>
+ <link_ctn id="80"/>
+ </route>
+ </zone>
+</platform>
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
-> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
-> [Checker] Backtracking from 1;2;1;2;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=3)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] Execution came to an end at 1;2;1;2;0 (state: 5, depth: 5)
+> [Checker] Backtracking from 1;2;1;2;0
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 7, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
-> [Checker] Backtracking from 2;1;1;2;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
> [Checker] BARRIER_WAIT(barrier: 0) (state=8)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=7)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
+> [Checker] Execution came to an end at 2;1;1;2;0 (state: 9, depth: 5)
+> [Checker] Backtracking from 2;1;1;2;0
> [Checker] DFS exploration ended. 9 unique states visited; 2 backtracks (10 transition replays, 0 states visited overall)
$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker] Dependent Transitions:
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
-> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;2;3;1;2;3;0
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=6)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=5)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=4)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] Execution came to an end at 1;2;3;1;2;3;0 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;2;3;1;2;3;0
+> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 8, 0 interleaves)
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves)
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves)
-> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves)
-> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
-> [Checker] Backtracking from 1;3;2;1;2;3;0
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
+> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] Dependent Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=10)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=9)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] Dependent Transitions:
> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker] BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] BARRIER_WAIT(barrier: 0) (state=11)
+> [Checker] Execution came to an end at 1;3;2;1;2;3;0 (state: 12, depth: 7)
+> [Checker] Backtracking from 1;3;2;1;2;3;0
> [Checker] DFS exploration ended. 12 unique states visited; 2 backtracks (14 transition replays, 1 states visited overall)
\ No newline at end of file
> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
-> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
-> [Checker] Backtracking from 1;1;1;2;2;2;0
-> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
-> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
> [Checker] INDEPENDENT Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
-> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves)
-> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7)
-> [Checker] Backtracking from 1;1;2;1;2;2;0
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
+> [Checker] Execution came to an end at 1;1;1;2;2;2;0 (state: 7, depth: 7)
+> [Checker] Backtracking from 1;1;1;2;2;2;0
+> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=9)
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10)
+> [Checker] Execution came to an end at 1;1;2;1;2;2;0 (state: 11, depth: 7)
+> [Checker] Backtracking from 1;1;2;1;2;2;0
> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 12, 0 interleaves)
+> [Checker] Dependent Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 13, 0 interleaves)
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
+> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13)
> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 14, 0 interleaves)
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
-> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7)
-> [Checker] Backtracking from 2;1;2;2;1;1;0
-> [Checker] Dependent Transitions:
+> [Checker] INDEPENDENT Transitions:
+> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
+> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
> [Checker] MUTEX_WAIT(mutex: 0, owner: 1) (state=15)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] INDEPENDENT Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] MUTEX_WAIT(mutex: 0, owner: 2) (state=13)
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
> [Checker] Dependent Transitions:
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
-> [Checker] MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
+> [Checker] MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
+> [Checker] Execution came to an end at 2;1;2;2;1;1;0 (state: 17, depth: 7)
+> [Checker] Backtracking from 2;1;2;2;1;1;0
> [Checker] DFS exploration ended. 17 unique states visited; 3 backtracks (21 transition replays, 2 states visited overall)
$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
#cmakedefine NS3_MINOR_VERSION @NS3_MINOR_VERSION@
/* Was the Eigen3 support compiled in? */
#cmakedefine01 SIMGRID_HAVE_EIGEN3
+/* Was the JSON support compiled in? */
+#cmakedefine01 SIMGRID_HAVE_JSON
#endif /* SIMGRID_PUBLIC_CONFIG_H */
} // namespace kernel
namespace mc {
class State;
+class RemoteApp;
}
} // namespace simgrid
friend kernel::activity::ActivityImpl;
friend std::vector<ActivityPtr> create_DAG_from_dot(const std::string& filename);
friend std::vector<ActivityPtr> create_DAG_from_DAX(const std::string& filename);
+ friend std::vector<ActivityPtr> create_DAG_from_json(const std::string& filename);
#endif
public:
std::vector<ActivityPtr> create_DAG_from_dot(const std::string& filename);
std::vector<ActivityPtr> create_DAG_from_DAX(const std::string& filename);
+std::vector<ActivityPtr> create_DAG_from_json(const std::string& filename);
#ifndef DOXYGEN /* Internal use only, no need to expose it */
template <class T>
-/* Copyright (c) 2009-2023. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2009-2023. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/internal_config.h"
#include <algorithm>
#include <map>
+#include <fstream>
+#include <simgrid/s4u/Host.hpp>
#include <simgrid/s4u/Comm.hpp>
#include <simgrid/s4u/Engine.hpp>
#include <simgrid/s4u/Exec.hpp>
#include "dax_dtd.h"
#include "dax_dtd.c"
+#if SIMGRID_HAVE_JSON
+#include <nlohmann/json.hpp>
+#include <sstream>
+#endif
+
#if HAVE_GRAPHVIZ
#include <graphviz/cgraph.h>
#endif
static std::map<std::string, Comm*, std::less<>> files;
static ExecPtr current_job;
+/** @brief loads a JSON file describing a DAG
+ *
+ * See https://github.com/wfcommons/wfformat for more details.
+ */
+std::vector<ActivityPtr> create_DAG_from_json(const std::string& filename)
+{
+#if SIMGRID_HAVE_JSON
+ std::ifstream f(filename);
+ auto data = nlohmann::json::parse(f);
+ std::vector<ActivityPtr> dag = {};
+ std::map<std::string, std::vector<ActivityPtr>> successors = {};
+ std::map<ActivityPtr, Host*> comms_destinations = {};
+ ActivityPtr current;
+
+ for (auto const& task: data["workflow"]["tasks"]) {
+ if (task["type"] == "compute") {
+ current = Exec::init()->set_name(task["name"])->set_flops_amount(task["runtime"]);
+ if (task.contains("machine"))
+ dynamic_cast<Exec*>(current.get())->set_host(simgrid::s4u::Engine::get_instance()->host_by_name(task["machine"]));
+ }
+ else if (task["type"] == "transfer"){
+ current = Comm::sendto_init()->set_name(task["name"])->set_payload_size(task["bytesWritten"]);
+ if (task.contains("machine"))
+ comms_destinations[current] = simgrid::s4u::Engine::get_instance()->host_by_name(task["machine"]);
+ if (task["parents"].size() == 1) {
+ ActivityPtr parent_activity;
+ for (auto const& activity: dag) {
+ if (activity->get_name() == task["parents"][0]) {
+ parent_activity = activity;
+ break;
+ }
+ }
+ if (dynamic_cast<Exec*>(parent_activity.get()) != nullptr)
+ dynamic_cast<Comm*>(current.get())->set_source(dynamic_cast<Exec*>(parent_activity.get())->get_host());
+ else if (dynamic_cast<Comm*>(parent_activity.get()) != nullptr)
+ dynamic_cast<Comm*>(current.get())->set_source(dynamic_cast<Comm*>(parent_activity.get())->get_destination());
+ }
+ } else if (XBT_LOG_ISENABLED(dag_parsing, xbt_log_priority_debug)) {
+ std::stringstream ss;
+ ss << task["type"];
+ XBT_DEBUG("Task type \"%s\" not supported.", ss.str().c_str());
+ }
+
+ dag.push_back(current);
+ for (auto const& parent: task["parents"]) {
+ auto it = successors.find(parent);
+ if (it == successors.end())
+ successors[parent] = {};
+ successors[parent].push_back(current);
+ }
+ }
+ // Assign successors
+ for (auto const& [parent, successors_list] : successors)
+ for (auto const& activity: dag)
+ if (activity->get_name() == parent) {
+ for (auto const& successor: successors_list)
+ activity->add_successor(successor);
+ break;
+ }
+ // Assign destinations of Comms (if done before successors are assigned there is a bug)
+ for (auto const& [comm, destination]: comms_destinations)
+ dynamic_cast<Comm*>(comm.get())->set_destination(destination);
+
+ // Start only Activities with dependencies solved
+ for (auto const& activity: dag) {
+ if (dynamic_cast<Exec*>(activity.get()) != nullptr and activity->dependencies_solved())
+ activity->start();
+ }
+ return dag;
+#else
+ xbt_die("JSON support was not compiled in, probably because nlohmann/json was not found. Please install "
+ "nlohmann-json3-dev and recompile SimGrid to use this feature.");
+#endif
+}
/** @brief loads a DAX file describing a DAG
*
* See https://confluence.pegasus.isi.edu/display/pegasus/WorkflowGenerator for more details.
* * the current state of an existing process;
*
* * a snapshot.
- *
- * In order to support SMPI privatization, the can read the memory from the
- * context of a given SMPI process: if specified, the code reads data from the
- * correct SMPI privatization VMA.
*/
class AddressSpace {
private:
+++ /dev/null
-/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "src/mc/ModelChecker.hpp"
-#include "src/mc/explo/Exploration.hpp"
-#include "src/mc/explo/LivenessChecker.hpp"
-#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_exit.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/sosp/RemoteProcessMemory.hpp"
-#include "src/mc/transition/TransitionComm.hpp"
-#include "xbt/automaton.hpp"
-#include "xbt/system_error.hpp"
-
-#include <array>
-#include <csignal>
-#include <sys/ptrace.h>
-#include <sys/wait.h>
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
-
-::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
-
-#ifdef __linux__
-# define WAITPID_CHECKED_FLAGS __WALL
-#else
-# define WAITPID_CHECKED_FLAGS 0
-#endif
-
-namespace simgrid::mc {
-
-ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory, int sockfd)
- : checker_side_(sockfd), remote_process_memory_(std::move(remote_memory))
-{
-}
-
-void ModelChecker::start()
-{
- checker_side_.start(
- [](evutil_socket_t sig, short events, void* arg) {
- auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
- if (events == EV_READ) {
- std::array<char, MC_MESSAGE_LENGTH> buffer;
- ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false);
- if (size == -1 && errno != EAGAIN)
- throw simgrid::xbt::errno_error();
-
- if (not mc->handle_message(buffer.data(), size))
- mc->checker_side_.break_loop();
- } else if (events == EV_SIGNAL) {
- if (sig == SIGCHLD)
- mc->handle_waitpid();
- else
- xbt_die("Unexpected signal: %d", sig);
- } else {
- xbt_die("Unexpected event");
- }
- },
- this);
-
- XBT_DEBUG("Waiting for the model-checked process");
- int status;
-
- // The model-checked process SIGSTOP itself to signal it's ready:
- const pid_t pid = remote_process_memory_->pid();
-
- xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
- "Could not wait model-checked process");
-
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
- ptrace(PTRACE_CONT, pid, 0, 0);
-#elif defined BSD
- ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
-#else
-# error "no ptrace equivalent coded for this platform"
-#endif
- xbt_assert(errno == 0,
- "Ptrace does not seem to be usable in your setup (errno: %d). "
- "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
- "If it does not help, please report this bug.",
- errno);
-}
-
-bool ModelChecker::handle_message(const char* buffer, ssize_t size)
-{
- s_mc_message_t base_message;
- xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
- memcpy(&base_message, buffer, sizeof(base_message));
-
- switch(base_message.type) {
- case MessageType::INITIAL_ADDRESSES: {
- s_mc_message_initial_addresses_t message;
- xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
- memcpy(&message, buffer, sizeof(message));
-
- get_remote_process_memory().init(message.mmalloc_default_mdp);
- break;
- }
-
- case MessageType::IGNORE_HEAP: {
- s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
-
- IgnoredHeapRegion region;
- region.block = message.block;
- region.fragment = message.fragment;
- region.address = message.address;
- region.size = message.size;
- get_remote_process_memory().ignore_heap(region);
- break;
- }
-
- case MessageType::UNIGNORE_HEAP: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_process_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
- break;
- }
-
- case MessageType::IGNORE_MEMORY: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_process_memory().ignore_region(message.addr, message.size);
- break;
- }
-
- case MessageType::STACK_REGION: {
- s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_process_memory().stack_areas().push_back(message.stack_region);
- } break;
-
- case MessageType::REGISTER_SYMBOL: {
- s_mc_message_register_symbol_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
- XBT_DEBUG("Received symbol: %s", message.name.data());
-
- LivenessChecker::automaton_register_symbol(get_remote_process_memory(), message.name.data(),
- remote((int*)message.data));
- break;
- }
-
- case MessageType::WAITING:
- return false;
-
- case MessageType::ASSERTION_FAILED:
- exploration_->report_assertion_failure();
- break;
-
- default:
- xbt_die("Unexpected message from model-checked application");
- }
- return true;
-}
-
-void ModelChecker::handle_waitpid()
-{
- XBT_DEBUG("Check for wait event");
- int status;
- pid_t pid;
- while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
- if (pid == -1) {
- if (errno == ECHILD) {
- // No more children:
- xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state");
- break;
- } else {
- XBT_ERROR("Could not wait for pid");
- throw simgrid::xbt::errno_error();
- }
- }
-
- if (pid == this->get_remote_process_memory().pid()) {
- // From PTRACE_O_TRACEEXIT:
-#ifdef __linux__
- if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- unsigned long eventmsg;
- xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
- "Could not get exit status");
- status = static_cast<int>(eventmsg);
- if (WIFSIGNALED(status))
- exploration_->report_crash(status);
- }
-#endif
-
- // We don't care about non-lethal signals, just reinject them:
- if (WIFSTOPPED(status)) {
- XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_CONT, get_remote_process_memory().pid(), 0, WSTOPSIG(status));
-#elif defined BSD
- ptrace(PT_CONTINUE, get_remote_process_memory().pid(), (caddr_t)1, WSTOPSIG(status));
-#endif
- xbt_assert(errno == 0, "Could not PTRACE_CONT");
- }
-
- else if (WIFSIGNALED(status)) {
- exploration_->report_crash(status);
- } else if (WIFEXITED(status)) {
- XBT_DEBUG("Child process is over");
- this->get_remote_process_memory().terminate();
- }
- }
- }
-}
-
-Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
-{
- s_mc_message_simcall_execute_t m = {};
- m.type = MessageType::SIMCALL_EXECUTE;
- m.aid_ = aid;
- m.times_considered_ = times_considered;
- checker_side_.get_channel().send(m);
-
- this->remote_process_memory_->clear_cache();
- if (this->remote_process_memory_->running())
- checker_side_.dispatch(); // The app may send messages while processing the transition
-
- s_mc_message_simcall_execute_answer_t answer;
- ssize_t s = checker_side_.get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
- xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
- "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
- to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
-
- if (new_transition) {
- std::stringstream stream(answer.buffer.data());
- return deserialize_transition(aid, times_considered, stream);
- } else
- return nullptr;
-}
-
-} // namespace simgrid::mc
+++ /dev/null
-/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_MODEL_CHECKER_HPP
-#define SIMGRID_MC_MODEL_CHECKER_HPP
-
-#include "src/mc/remote/CheckerSide.hpp"
-#include "src/mc/remote/RemotePtr.hpp"
-#include "src/mc/sosp/PageStore.hpp"
-#include "xbt/base.h"
-
-#include <memory>
-
-namespace simgrid::mc {
-
-/** State of the model-checker (global variables for the model checker)
- */
-class ModelChecker {
- CheckerSide checker_side_;
- std::unique_ptr<RemoteProcessMemory> remote_process_memory_;
- Exploration* exploration_ = nullptr;
-
-public:
- ModelChecker(ModelChecker const&) = delete;
- ModelChecker& operator=(ModelChecker const&) = delete;
- explicit ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_simulation, int sockfd);
-
- RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; }
- Channel& get_channel() { return checker_side_.get_channel(); }
- void channel_handle_events() { checker_side_.dispatch(); }
-
- void start();
-
- /** Let the application take a transition. A new Transition is created iff the last parameter is true */
- Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
-
- Exploration* get_exploration() const { return exploration_; }
- void set_exploration(Exploration* exploration) { exploration_ = exploration; }
-
-private:
- bool handle_message(const char* buffer, ssize_t size);
- void handle_waitpid();
-};
-
-} // namespace simgrid::mc
-
-#endif
/** @brief Save the current state */
VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app)
- : heap_bytes_used_(remote_app.get_remote_process_memory().get_remote_heap_bytes())
+ : heap_bytes_used_(remote_app.get_remote_process_memory()->get_remote_heap_bytes())
, actor_count_(actor_count)
, num_(state_number)
{
this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
void VisitedStates::prune()
for (auto i = range_begin; i != range_end; ++i) {
auto& visited_state = *i;
- if (*visited_state->system_state_.get() == *new_state->system_state_.get()) {
+ if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
+ *remote_app.get_remote_process_memory())) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/api/RemoteApp.hpp"
-#include "src/internal_config.h" // HAVE_SMPI
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
#include "xbt/asserts.h"
-#if HAVE_SMPI
-#include "smpi/smpi.h"
-#include "src/smpi/include/private.hpp"
-#endif
#include "src/mc/api/State.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include <algorithm>
#include <array>
-#include <boost/tokenizer.hpp>
#include <memory>
#include <numeric>
#include <string>
-#include <fcntl.h>
-#ifdef __linux__
-#include <sys/prctl.h>
-#endif
+#include <sys/ptrace.h>
+#include <sys/wait.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
XBT_LOG_EXTERNAL_CATEGORY(mc_global);
-static simgrid::config::Flag<std::string> _sg_mc_setenv{
- "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
- [](std::string_view value) {
- xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
- "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
- }};
-
namespace simgrid::mc {
-XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<char*>& args)
-{
- /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
- * env variable is set. If so, MC mode is assumed, and the client is setup from its side
- */
-
-#ifdef __linux__
- // Make sure we do not outlive our parent
- sigset_t mask;
- sigemptyset(&mask);
- xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
- xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
-#endif
-
- // Remove CLOEXEC to pass the socket to the application
- int fdflags = fcntl(socket, F_GETFD, 0);
- xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
- "Could not remove CLOEXEC for socket");
-
- setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
-
- /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
- using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
- boost::char_separator<char> semicol_sep(";");
- boost::char_separator<char> equal_sep("=");
- Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
- for (const auto& token : token_vars) {
- std::vector<std::string> kv;
- Tokenizer token_kv(token, equal_sep);
- for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
- kv.push_back(t);
- xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
- token.c_str());
- XBT_INFO("setenv '%s'='%s'", kv[0].c_str(), kv[1].c_str());
- setenv(kv[0].c_str(), kv[1].c_str(), 1);
- }
-
- /* And now, exec the child process */
- int i = 1;
- while (args[i] != nullptr && args[i][0] == '-')
- i++;
-
- xbt_assert(args[i] != nullptr,
- "Unable to find a binary to exec on the command line. Did you only pass config flags?");
-
- execvp(args[i], args.data() + i);
- XBT_CRITICAL("The model-checked process failed to exec(%s): %s.\n"
- " Make sure that your binary exists on disk and is executable.",
- args[i], strerror(errno));
- if (strchr(args[i], '=') != nullptr)
- XBT_CRITICAL("If you want to pass environment variables to the application, please use --cfg=model-check/setenv:%s",
- args[i]);
-
- xbt_die("Aborting now.");
-}
-
-RemoteApp::RemoteApp(const std::vector<char*>& args)
+RemoteApp::RemoteApp(const std::vector<char*>& args, bool need_memory_introspection)
{
-#if HAVE_SMPI
- smpi_init_options(); // only performed once
- xbt_assert(smpi_cfg_privatization() != SmpiPrivStrategies::MMAP,
- "Please use the dlopen privatization schema when model-checking SMPI code");
-#endif
-
- // Create an AF_LOCAL socketpair used for exchanging messages
- // between the model-checker process (ourselves) and the model-checked
- // process:
- int sockets[2];
- xbt_assert(socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets) != -1, "Could not create socketpair");
-
- pid_t pid = fork();
- xbt_assert(pid >= 0, "Could not fork model-checked process");
-
- if (pid == 0) { // Child
- ::close(sockets[1]);
- run_child_process(sockets[0], args);
- DIE_IMPOSSIBLE;
- }
-
- // Parent (model-checker):
- ::close(sockets[0]);
-
- xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
+ for (auto* arg : args)
+ app_args_.push_back(arg);
- auto process = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid);
- model_checker_ = std::make_unique<simgrid::mc::ModelChecker>(std::move(process), sockets[1]);
+ checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_, need_memory_introspection);
- mc_model_checker = model_checker_.get();
- model_checker_->start();
-
- /* Take the initial snapshot */
- wait_for_requests();
- initial_snapshot_ =
- std::make_shared<simgrid::mc::Snapshot>(0, page_store_, model_checker_->get_remote_process_memory());
+ if (need_memory_introspection)
+ initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, *checker_side_->get_remote_memory());
}
RemoteApp::~RemoteApp()
{
initial_snapshot_ = nullptr;
- if (model_checker_) {
- shutdown();
- model_checker_ = nullptr;
- mc_model_checker = nullptr;
- }
+ checker_side_ = nullptr;
}
-void RemoteApp::restore_initial_state() const
+void RemoteApp::restore_initial_state()
{
- this->initial_snapshot_->restore(model_checker_->get_remote_process_memory());
+ if (initial_snapshot_ == nullptr) { // No memory introspection
+ // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy
+ checker_side_.reset(nullptr);
+ checker_side_.reset(new simgrid::mc::CheckerSide(app_args_, true));
+ } else
+ initial_snapshot_->restore(*checker_side_->get_remote_memory());
}
unsigned long RemoteApp::get_maxpid() const
// note: we could maybe cache it and count the actor creation on checker side too.
// But counting correctly accross state checkpoint/restore would be annoying.
- model_checker_->get_channel().send(MessageType::ACTORS_MAXPID);
+ checker_side_->get_channel().send(MessageType::ACTORS_MAXPID);
s_mc_message_int_t answer;
- ssize_t answer_size = model_checker_->get_channel().receive(answer);
+ ssize_t answer_size = checker_side_->get_channel().receive(answer);
xbt_assert(answer_size != -1, "Could not receive message");
xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
xbt_assert(answer.type == MessageType::ACTORS_MAXPID_REPLY,
// <----- send ACTORS_STATUS_REPLY
// <----- send `N` `s_mc_message_actors_status_one_t` structs
// <----- send `M` `s_mc_message_simcall_probe_one_t` structs
- model_checker_->get_channel().send(MessageType::ACTORS_STATUS);
+ checker_side_->get_channel().send(MessageType::ACTORS_STATUS);
s_mc_message_actors_status_answer_t answer;
- ssize_t answer_size = model_checker_->get_channel().receive(answer);
+ ssize_t answer_size = checker_side_->get_channel().receive(answer);
xbt_assert(answer_size != -1, "Could not receive message");
xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
xbt_assert(answer.type == MessageType::ACTORS_STATUS_REPLY,
std::vector<s_mc_message_actors_status_one_t> status(answer.count);
if (answer.count > 0) {
size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
- ssize_t received = model_checker_->get_channel().receive(status.data(), size);
+ ssize_t received = checker_side_->get_channel().receive(status.data(), size);
xbt_assert(static_cast<size_t>(received) == size);
}
std::vector<s_mc_message_simcall_probe_one_t> probes(answer.transition_count);
if (answer.transition_count > 0) {
for (auto& probe : probes) {
- ssize_t received = model_checker_->get_channel().receive(probe);
+ ssize_t received = checker_side_->get_channel().receive(probe);
xbt_assert(received >= 0, "Could not receive response to ACTORS_PROBE message (%s)", strerror(errno));
xbt_assert(static_cast<size_t>(received) == sizeof probe,
"Could not receive response to ACTORS_PROBE message (%zd bytes received != %zu bytes expected",
void RemoteApp::check_deadlock() const
{
- xbt_assert(model_checker_->get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
+ xbt_assert(checker_side_->get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
s_mc_message_int_t message;
- ssize_t received = model_checker_->get_channel().receive(message);
+ ssize_t received = checker_side_->get_channel().receive(message);
xbt_assert(received != -1, "Could not receive message");
xbt_assert(received == sizeof message, "Broken message (size=%zd; expected %zu)", received, sizeof message);
xbt_assert(message.type == MessageType::DEADLOCK_CHECK_REPLY,
to_c_str(message.type), (int)message.type, (int)MessageType::DEADLOCK_CHECK_REPLY);
if (message.value != 0) {
+ auto* explo = Exploration::get_instance();
XBT_CINFO(mc_global, "Counter-example execution trace:");
- for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
+ for (auto const& frame : explo->get_textual_trace())
XBT_CINFO(mc_global, " %s", frame.c_str());
XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
"--cfg=model-check/replay:'%s'",
- model_checker_->get_exploration()->get_record_trace().to_string().c_str());
- model_checker_->get_exploration()->log_state();
+ explo->get_record_trace().to_string().c_str());
+ explo->log_state();
throw DeadlockError();
}
}
void RemoteApp::wait_for_requests()
{
- /* Resume the application */
- if (model_checker_->get_channel().send(MessageType::CONTINUE) != 0)
- throw xbt::errno_error();
- get_remote_process_memory().clear_cache();
-
- if (this->get_remote_process_memory().running())
- model_checker_->channel_handle_events();
+ checker_side_->wait_for_requests();
}
-void RemoteApp::shutdown()
+Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_transition)
{
- XBT_DEBUG("Shutting down model-checker");
-
- RemoteProcessMemory& process = get_remote_process_memory();
- if (process.running()) {
- XBT_DEBUG("Killing process");
- finalize_app(true);
- kill(process.pid(), SIGKILL);
- process.terminate();
- }
+ s_mc_message_simcall_execute_t m = {};
+ m.type = MessageType::SIMCALL_EXECUTE;
+ m.aid_ = aid;
+ m.times_considered_ = times_considered;
+ checker_side_->get_channel().send(m);
+
+ auto* memory = get_remote_process_memory();
+ if (memory != nullptr)
+ memory->clear_cache();
+ if (checker_side_->running())
+ checker_side_->dispatch_events(); // The app may send messages while processing the transition
+
+ s_mc_message_simcall_execute_answer_t answer;
+ ssize_t s = checker_side_->get_channel().receive(answer);
+ xbt_assert(s != -1, "Could not receive message");
+ xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+ xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
+ "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
+ to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
+
+ if (new_transition) {
+ std::stringstream stream(answer.buffer.data());
+ return deserialize_transition(aid, times_considered, stream);
+ } else
+ return nullptr;
}
void RemoteApp::finalize_app(bool terminate_asap)
{
- s_mc_message_int_t m = {};
- m.type = MessageType::FINALIZE;
- m.value = terminate_asap;
- xbt_assert(model_checker_->get_channel().send(m) == 0, "Could not ask the app to finalize on need");
-
- s_mc_message_t answer;
- ssize_t s = model_checker_->get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive answer to FINALIZE");
- xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
- xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
- "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
- (int)answer.type, (int)MessageType::FINALIZE_REPLY);
+ checker_side_->finalize(terminate_asap);
}
} // namespace simgrid::mc
#define SIMGRID_MC_REMOTE_APP_HPP
#include "simgrid/forward.h"
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/ActorState.hpp"
+#include "src/mc/remote/CheckerSide.hpp"
#include "src/mc/remote/RemotePtr.hpp"
+#include "src/mc/sosp/PageStore.hpp"
#include <functional>
/** High-level view of the verified application, from the model-checker POV
*
- * This is expected to become the interface used by model-checking
- * algorithms to control the execution of the model-checked process
- * and the exploration of the execution graph. Model-checking
- * algorithms should be able to be written in high-level languages
- * (e.g. Python) using bindings on this interface.
+ * This is expected to become the interface used by model-checking algorithms to control the execution of
+ * the application process during the exploration of the execution graph.
+ *
+ * One day, this will allow parallel exploration, ie, the handling of several application processes (each encapsulated
+ * in a separate CheckerSide objects) that explore several parts of the exploration graph.
*/
class XBT_PUBLIC RemoteApp {
private:
- std::unique_ptr<ModelChecker> model_checker_;
+ std::unique_ptr<CheckerSide> checker_side_;
PageStore page_store_{500};
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
+ std::vector<char*> app_args_;
+
// No copy:
RemoteApp(RemoteApp const&) = delete;
RemoteApp& operator=(RemoteApp const&) = delete;
*
* The code is expected to `exec` the model-checked application.
*/
- explicit RemoteApp(const std::vector<char*>& args);
+ explicit RemoteApp(const std::vector<char*>& args, bool need_memory_introspection);
~RemoteApp();
- void restore_initial_state() const;
+ void restore_initial_state();
void wait_for_requests();
/** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
/** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
void finalize_app(bool terminate_asap = false);
- /** Forcefully kill the application (after running post-mortem analysis)*/
- void shutdown();
/** Retrieve the max PID of the running actors */
unsigned long get_maxpid() const;
/* Get the list of actors that are ready to run at that step. Usually shorter than maxpid */
void get_actors_status(std::map<aid_t, simgrid::mc::ActorState>& whereto) const;
+ /** Take a transition. A new Transition is created iff the last parameter is true */
+ Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
+
/* Get the memory of the remote process */
- RemoteProcessMemory& get_remote_process_memory() { return model_checker_->get_remote_process_memory(); }
+ RemoteProcessMemory* get_remote_process_memory() { return checker_side_->get_remote_memory(); }
PageStore& get_page_store() { return page_store_; }
};
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/api/State.hpp"
+#include "src/mc/api/guide/BasicGuide.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
long State::expended_states_ = 0;
-State::State(RemoteApp& remote_app) : num_(++expended_states_)
+State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_unique<BasicGuide>())
{
- remote_app.get_actors_status(actors_to_run_);
+ remote_app.get_actors_status(guide->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
-State::State(RemoteApp& remote_app, const State* previous_state)
- : default_transition_(std::make_unique<Transition>()), num_(++expended_states_)
+State::State(RemoteApp& remote_app, const State* parent_state)
+ : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
{
- remote_app.get_actors_status(actors_to_run_);
-
- transition_ = default_transition_.get();
+ remote_app.get_actors_status(guide->actors_to_run_);
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
-
- /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
- * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
- * it is not explored*/
- for (auto& [aid, transition] : previous_state->get_sleep_set()) {
-
- if (not previous_state->get_transition()->depends(&transition)) {
-
- sleep_set_.emplace(aid, transition);
- if (actors_to_run_.count(aid) != 0) {
- XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
-
- actors_to_run_.at(aid).mark_done();
- }
- } else
- XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
- transition.to_string().c_str(), previous_state->get_transition()->to_string().c_str());
+ *remote_app.get_remote_process_memory());
+
+ /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
+ if (_sg_mc_sleep_set) {
+ /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
+ * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
+ * it is not explored*/
+ for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
+
+ if (not parent_state_->get_transition()->depends(&transition)) {
+
+ sleep_set_.emplace(aid, transition);
+ if (guide->actors_to_run_.count(aid) != 0) {
+ XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
+
+ guide->actors_to_run_.at(aid).mark_done();
+ }
+ } else
+ XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
+ transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str());
+ }
}
}
std::size_t State::count_todo() const
{
- return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
-}
-
-void State::mark_all_enabled_todo()
-{
- for (auto const& [aid, _] : this->get_actors_list()) {
- if (this->is_actor_enabled(aid) and not is_actor_done(aid)) {
- this->mark_todo(aid);
- }
- }
+ return boost::range::count_if(this->guide->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
}
Transition* State::get_transition() const
aid_t State::next_transition() const
{
- XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size());
- for (auto const& [aid, actor] : actors_to_run_) {
+ XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide->actors_to_run_.size());
+ for (auto const& [aid, actor] : guide->actors_to_run_) {
/* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
return -1;
}
-void State::execute_next(aid_t next)
+std::pair<aid_t, double> State::next_transition_guided() const
+{
+ return guide->next_transition();
+}
+
+// This should be done in GuidedState, or at least interact with it
+void State::execute_next(aid_t next, RemoteApp& app)
{
// This actor is ready to be executed. Execution involves three phases:
// 1. Identify the appropriate ActorState to prepare for execution
// when simcall_handle will be called on it
- auto& actor_state = actors_to_run_.at(next);
+ auto& actor_state = guide->actors_to_run_.at(next);
const unsigned times_considered = actor_state.do_consider();
const auto* expected_executed_transition = actor_state.get_transition(times_considered);
xbt_assert(expected_executed_transition != nullptr,
// 2. Execute the actor according to the preparation above
Transition::executed_transitions_++;
- auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true);
+ auto* just_executed = app.handle_simcall(next, times_considered, true);
xbt_assert(just_executed->type_ == expected_executed_transition->type_,
"The transition that was just executed by actor %ld, viz:\n"
"%s\n"
auto executed_transition = std::unique_ptr<Transition>(just_executed);
actor_state.set_transition(std::move(executed_transition), times_considered);
- mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
+ app.wait_for_requests();
}
} // namespace simgrid::mc
#include "src/mc/api/ActorState.hpp"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/api/guide/GuidedState.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "src/mc/transition/Transition.hpp"
/** Sequential state ID (used for debugging) */
long num_ = 0;
- /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
- * state */
- std::map<aid_t, ActorState> actors_to_run_;
-
/** Snapshot of system state (if needed) */
std::shared_ptr<Snapshot> system_state_;
+ /** Unique parent of this state. Required both for sleep set computation
+ and for guided model-checking */
+ const State* parent_state_;
+
+ std::unique_ptr<GuidedState> guide;
+
/* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
* set. With this information, it is check whether it should be removed from it or not when exploring a new
* transition */
std::map<aid_t, Transition> sleep_set_;
-
+
public:
explicit State(RemoteApp& remote_app);
- explicit State(RemoteApp& remote_app, const State* previous_state);
+ explicit State(RemoteApp& remote_app, const State* parent_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
- aid_t next_transition() const;
+ aid_t next_transition() const; // this function should disapear as it is redundant with the next one
- /* Explore a new path; the parameter must be the result of a previous call to next_transition() */
- void execute_next(aid_t next);
+ /* Same as next_transition, but choice is now guided, and a double corresponding to the
+ internal cost of the transition is returned */
+ std::pair<aid_t, double> next_transition_guided() const;
+
+ /* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
+ * next_transition() */
+ void execute_next(aid_t next, RemoteApp& app);
long get_num() const { return num_; }
std::size_t count_todo() const;
- void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
- void mark_all_enabled_todo();
- bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
+
+ void consider_one(aid_t aid) { guide->consider_one(aid); }
+ void consider_best() { guide->consider_best(); }
+ void consider_all() { guide->consider_all(); }
+
+ bool is_actor_done(aid_t actor) const { return guide->actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
- std::map<aid_t, ActorState> const& get_actors_list() const { return actors_to_run_; }
+ std::map<aid_t, ActorState> const& get_actors_list() const { return guide->actors_to_run_; }
- unsigned long get_actor_count() const { return actors_to_run_.size(); }
- bool is_actor_enabled(aid_t actor) { return actors_to_run_.at(actor).is_enabled(); }
+ unsigned long get_actor_count() const { return guide->actors_to_run_.size(); }
+ bool is_actor_enabled(aid_t actor) { return guide->actors_to_run_.at(actor).is_enabled(); }
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
- void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
-
+ void add_sleep_set(Transition* t)
+ {
+ sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
+ }
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_BASICGUIDE_HPP
+#define SIMGRID_MC_BASICGUIDE_HPP
+
+namespace simgrid::mc {
+
+/** Basic MC guiding class which corresponds to no guide at all (random choice) */
+// Not Yet fully implemented
+class BasicGuide : public GuidedState {
+public:
+ std::pair<aid_t, double> next_transition() const override
+ {
+
+ for (auto const& [aid, actor] : actors_to_run_) {
+ /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
+ continue;
+ }
+
+ return std::make_pair(aid, 1.0);
+ }
+ return std::make_pair(-1, 0.0);
+ }
+ void execute_next(aid_t aid, RemoteApp& app) override { return; }
+
+ void consider_best() override
+ {
+ for (auto& [_, actor] : actors_to_run_) {
+ if (actor.is_todo())
+ return;
+ if (actor.is_enabled() and not actor.is_done()) {
+ actor.mark_todo();
+ return;
+ }
+ }
+ }
+};
+
+} // namespace simgrid::mc
+
+#endif
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "xbt/asserts.h"
+
+#ifndef SIMGRID_MC_GUIDEDSTATE_HPP
+#define SIMGRID_MC_GUIDEDSTATE_HPP
+
+namespace simgrid::mc {
+
+class GuidedState {
+protected:
+ /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this
+ * state */
+ std::map<aid_t, ActorState> actors_to_run_;
+
+public:
+ virtual ~GuidedState() = default;
+ virtual std::pair<aid_t, double> next_transition() const = 0;
+ virtual void execute_next(aid_t aid, RemoteApp& app) = 0;
+ virtual void consider_best() = 0;
+
+ // Mark the first enabled and not yet done transition as todo
+ // If there's already a transition marked as todo, does nothing
+ void consider_one(aid_t aid)
+ {
+ xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(),
+ "Tried to mark as TODO actor %ld but it is either not enabled or already done", aid);
+ actors_to_run_.at(aid).mark_todo();
+ }
+ // Matk as todo all actors enabled that are not done yet
+ void consider_all()
+ {
+ for (auto& [_, actor] : actors_to_run_)
+ if (actor.is_enabled() and not actor.is_done())
+ actor.mark_todo();
+ }
+
+ friend class State;
+};
+
+} // namespace simgrid::mc
+
+#endif
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
+#include "src/mc/sosp/RemoteProcessMemory.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/ex.h"
compared_pointers.clear();
}
- int initHeapInformation(const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
+ int initHeapInformation(RemoteProcessMemory& appli, const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
const std::vector<IgnoredHeapRegion>& i1, const std::vector<IgnoredHeapRegion>& i2);
template <int rank> HeapArea& equals_to_(std::size_t i, std::size_t j)
this->types.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, nullptr);
}
-int StateComparator::initHeapInformation(const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
- const std::vector<IgnoredHeapRegion>& i1,
+int StateComparator::initHeapInformation(simgrid::mc::RemoteProcessMemory& memory, const s_xbt_mheap_t* heap1,
+ const s_xbt_mheap_t* heap2, const std::vector<IgnoredHeapRegion>& i1,
const std::vector<IgnoredHeapRegion>& i2)
{
if ((heap1->heaplimit != heap2->heaplimit) || (heap1->heapsize != heap2->heapsize))
return -1;
this->heaplimit = heap1->heaplimit;
- this->std_heap_copy = *mc_model_checker->get_remote_process_memory().get_heap();
+ this->std_heap_copy = *memory.get_heap();
this->processStates[0].initHeapInformation(heap1, i1);
this->processStates[1].initHeapInformation(heap2, i2);
return 0;
}
namespace simgrid::mc {
-
-bool Snapshot::operator==(const Snapshot& other)
+bool Snapshot::equals_to(const Snapshot& other, RemoteProcessMemory& memory)
{
- // TODO, make this a field of ModelChecker or something similar
- static StateComparator state_comparator;
+ /* TODO: the memory parameter should be eventually removed. It seems to be there because each snapshot lacks some sort
+ of metadata. That's OK for now (letting appart the fact that we cannot have a nice operator== because we need that
+ extra parameter), but it will fall short when we want to have parallel explorations, with more than one
+ RemoteProcess. At the very least, snapshots will need to know the remote process they are corresponding to, and more
+ probably they will need to embeed all their metadata to let the remoteprocesses die before the end of the
+ exploration. */
+
+ /* TODO: This method should moved to Snapshot.cpp, but it needs the StateComparator that is declared locally to this
+ * file only. */
- const RemoteProcessMemory& process = mc_model_checker->get_remote_process_memory();
+ static StateComparator state_comparator; // TODO, make this a field of a persistant state object
if (hash_ != other.hash_) {
XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_,
}
/* Init heap information used in heap comparison algorithm */
- const s_xbt_mheap_t* heap1 = static_cast<xbt_mheap_t>(this->read_bytes(
- alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
- const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(other.read_bytes(
- alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
- if (state_comparator.initHeapInformation(heap1, heap2, this->to_ignore_, other.to_ignore_) == -1) {
+ const s_xbt_mheap_t* heap1 = static_cast<xbt_mheap_t>(
+ this->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), memory.heap_address, ReadOptions::lazy()));
+ const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(
+ other.read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), memory.heap_address, ReadOptions::lazy()));
+ if (state_comparator.initHeapInformation(memory, heap1, heap2, this->to_ignore_, other.to_ignore_) == -1) {
XBT_VERB("(%ld - %ld) Different heap information", this->num_state_, other.num_state_);
return false;
}
const_mc_snapshot_stack_t stack1 = &this->stacks_[cursor];
const_mc_snapshot_stack_t stack2 = &other.stacks_[cursor];
- if (local_variables_differ(process, state_comparator, *this, other, stack1, stack2)) {
+ if (local_variables_differ(memory, state_comparator, *this, other, stack1, stack2)) {
XBT_VERB("(%ld - %ld) Different local variables between stacks %u", this->num_state_, other.num_state_,
cursor + 1);
return false;
xbt_assert(region1->object_info());
/* Compare global variables */
- if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *this, other)) {
+ if (global_variables_differ(memory, state_comparator, region1->object_info(), region1, region2, *this, other)) {
std::string const& name = region1->object_info()->file_name;
XBT_VERB("(%ld - %ld) Different global variables in %s", this->num_state_, other.num_state_, name.c_str());
return false;
XBT_VERB(" Compare heap...");
/* Compare heap */
- if (mmalloc_heap_differ(process, state_comparator, *this, other)) {
+ if (mmalloc_heap_differ(memory, state_comparator, *this, other)) {
XBT_VERB("(%ld - %ld) Different heap (mmalloc_heap_differ)", this->num_state_, other.num_state_);
return false;
}
void DFSExplorer::check_non_termination(const State* current_state)
{
for (auto const& state : stack_) {
- if (*state->get_system_state() == *current_state->get_system_state()) {
+ if (state->get_system_state()->equals_to(*current_state->get_system_state(),
+ *get_remote_app().get_remote_process_memory())) {
XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
continue;
}
- // Backtrack if we are revisiting a state we saw previously
+ // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction
if (visited_state_ != nullptr) {
XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
}
// Search for the next transition
- aid_t next = state->next_transition();
+ // next_transition returns a pair<aid_t, double> in case we want to consider multiple state
+ auto [next, _] = state->next_transition_guided();
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
-
+
if (state->get_actor_count() == 0) {
get_remote_app().finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
-
}
-
+
this->backtrack();
continue;
}
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- state->execute_next(next);
+ state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
/* Create the new expanded state (copy the state of MCed into our MCer data) */
std::unique_ptr<State> next_state;
- /* If we want sleep set reduction, pass the old state to the new state so it can
- * both copy the sleep set and eventually removes things from it locally */
- if (_sg_mc_sleep_set)
- next_state = std::make_unique<State>(get_remote_app(), state);
- else
- next_state = std::make_unique<State>(get_remote_app());
-
+ next_state = std::make_unique<State>(get_remote_app(), state);
on_state_creation_signal(next_state.get(), get_remote_app());
-
+ /* Sleep set procedure:
+ * adding the taken transition to the sleep set of the original state.
+ * <!> Since the parent sleep set is used to compute the child sleep set, this need to be
+ * done after next_state creation */
+ XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
+ state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+ state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
+
+ /* DPOR persistent set procedure:
+ * for each new transition considered, check if it depends on any other previous transition executed before it
+ * on another process. If there exists one, find the more recent, and add its process to the interleave set.
+ * If the process is not enabled at this point, then add every enabled process to the interleave */
+ if (reduction_mode_ == ReductionMode::dpor) {
+ aid_t issuer_id = state->get_transition()->aid_;
+ for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
+ State* prev_state = i->get();
+ if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
+ XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
+ prev_state->get_transition()->to_string().c_str(), issuer_id);
+ continue;
+ } else if (prev_state->get_transition()->depends(state->get_transition())) {
+ XBT_VERB("Dependent Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+
+ if (prev_state->is_actor_enabled(issuer_id)) {
+ if (not prev_state->is_actor_done(issuer_id))
+ prev_state->consider_one(issuer_id);
+ else
+ XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
+ } else {
+ XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
+ "transition as todo",
+ issuer_id);
+ prev_state->consider_all();
+ }
+ break;
+ } else {
+ XBT_VERB("INDEPENDENT Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+ }
+ }
+ }
+
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto const& [aid, _] : next_state->get_actors_list()) {
- if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) {
- next_state->mark_todo(aid);
- if (reduction_mode_ == ReductionMode::dpor)
- break; // With DPOR, we take the first enabled transition
- }
- }
+ if (reduction_mode_ == ReductionMode::dpor)
+ next_state->consider_best(); // Take only one transition if DPOR: others may be considered later if required
+ else
+ next_state->consider_all();
dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
state->get_transition()->dot_string().c_str());
/* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
* In the first case, we need to remove the last transition corresponding to the Finalize */
if (stack_.back()->get_transition()->aid_ == 0)
- stack_.pop_back();
-
+ stack_.pop_back();
+
/* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
- * have it empty in the way. For each deleted state, check if the request that has generated it (from its
- * predecessor state) depends on any other previous request executed before it on another process. If there exists one,
- * find the more recent, and add its process to the interleave set. If the process is not enabled at this point,
- * then add every enabled process to the interleave */
+ * have it empty in the way. */
bool found_backtracking_point = false;
while (not stack_.empty() && not found_backtracking_point) {
std::unique_ptr<State> state = std::move(stack_.back());
stack_.pop_back();
- XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
- state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
- state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
-
- if (reduction_mode_ == ReductionMode::dpor) {
- aid_t issuer_id = state->get_transition()->aid_;
- for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
- State* prev_state = i->get();
- if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
- XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
- prev_state->get_transition()->to_string().c_str(), issuer_id);
- continue;
- } else if (prev_state->get_transition()->depends(state->get_transition())) {
- XBT_VERB("Dependent Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
-
- if (prev_state->is_actor_enabled(issuer_id)) {
- if (not prev_state->is_actor_done(issuer_id))
- prev_state->mark_todo(issuer_id);
- else
- XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
- } else {
- XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
- "transition as todo",
- issuer_id);
- prev_state->mark_all_enabled_todo();
- }
- break;
- } else {
- XBT_VERB("INDEPENDENT Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
- }
- }
- }
if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over
XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
} else {
XBT_DEBUG("Back-tracking to state %ld at depth %zu: %lu transitions left to be explored", state->get_num(),
stack_.size() + 1, state->count_todo());
- stack_.push_back(std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
+ stack_.push_back(
+ std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
found_backtracking_point = true;
}
}
/* If asked to rollback on a state that has a snapshot, restore it */
State* last_state = stack_.back().get();
if (const auto* system_state = last_state->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
on_restore_system_state_signal(last_state, get_remote_app());
return;
}
for (std::unique_ptr<State> const& state : stack_) {
if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
break;
- state->get_transition()->replay();
+ state->get_transition()->replay(get_remote_app());
on_transition_replay_signal(state->get_transition(), get_remote_app());
visited_states_count_++;
}
} // If no backtracing point, then the stack is empty and the exploration is over
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args)
+//DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, _sg_mc_termination) // UNCOMMENT TO ACTIVATE REFORKS
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, true) // This version does not use reforks as it breaks
{
if (with_dpor)
reduction_mode_ = ReductionMode::dpor;
/* Get an enabled actor and insert it in the interleave set of the initial state */
XBT_DEBUG("Initial state. %lu actors to consider", initial_state->get_actor_count());
- for (auto const& [aid, _] : initial_state->get_actors_list()) {
- if (initial_state->is_actor_enabled(aid)) {
- initial_state->mark_todo(aid);
- if (reduction_mode_ == ReductionMode::dpor) {
- XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid);
- break;
- }
- XBT_DEBUG("Actor %ld is TODO", aid);
- }
- }
+ if (reduction_mode_ == ReductionMode::dpor)
+ initial_state->consider_best();
+ else
+ initial_state->consider_all();
stack_.push_back(std::move(initial_state));
}
static simgrid::config::Flag<std::string> cfg_dot_output_file{
"model-check/dot-output", "Name of dot output file corresponding to graph state", ""};
-Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
+Exploration* Exploration::instance_ = nullptr; // singleton instance
+
+Exploration::Exploration(const std::vector<char*>& args, bool need_memory_introspection)
+ : remote_app_(std::make_unique<RemoteApp>(args, need_memory_introspection))
{
- mc_model_checker->set_exploration(this);
+ xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
+ instance_ = this;
if (not cfg_dot_output_file.get().empty()) {
dot_output_ = fopen(cfg_dot_output_file.get().c_str(), "w");
{
if (dot_output_ != nullptr)
fclose(dot_output_);
+ instance_ = nullptr;
}
void Exploration::dot_output(const char* fmt, ...)
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
- XBT_INFO("Stack trace:");
- get_remote_app().get_remote_process_memory().dump_stack();
+ auto* memory = get_remote_app().get_remote_process_memory();
+ if (memory) {
+ XBT_INFO("Stack trace:");
+ memory->dump_stack();
+ } else {
+ XBT_INFO("Stack trace not shown because there is no memory introspection.");
+ }
}
- get_remote_app().get_remote_process_memory().terminate();
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
void Exploration::report_assertion_failure()
void Exploration::system_exit(int status)
{
- get_remote_app().shutdown();
::exit(status);
}
// abstract
class Exploration : public xbt::Extendable<Exploration> {
std::unique_ptr<RemoteApp> remote_app_;
+ static Exploration* instance_;
FILE* dot_output_ = nullptr;
public:
- explicit Exploration(const std::vector<char*>& args);
+ explicit Exploration(const std::vector<char*>& args, bool need_memory_introspection);
virtual ~Exploration();
+ static Exploration* get_instance() { return instance_; }
// No copy:
Exploration(Exploration const&) = delete;
Exploration& operator=(Exploration const&) = delete;
RemoteApp& remote_app)
: num(pair_num), prop_state_(prop_state)
{
- auto& memory = mc_model_checker->get_remote_process_memory();
+ auto* memory = remote_app.get_remote_process_memory();
this->app_state_ = std::move(app_state);
if (not this->app_state_->get_system_state())
- this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), memory));
- this->heap_bytes_used = memory.get_remote_heap_bytes();
+ this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), *memory));
+ this->heap_bytes_used = memory->get_remote_heap_bytes();
this->actor_count_ = app_state_->get_actor_count();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
- (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state()))
+ (not pair_test->app_state_->get_system_state()->equals_to(*new_pair->app_state_->get_system_state(),
+ *get_remote_app().get_remote_process_memory())))
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
exploration_stack_.pop_back();
if (_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
if (const auto* system_state = pair->app_state_->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
return;
}
}
std::shared_ptr<State> state = pair->app_state_;
if (pair->exploration_started) {
- state->get_transition()->replay();
+ state->get_transition()->replay(get_remote_app());
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
}
const VisitedPair* pair_test = i->get();
if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
- (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state()))
+ (not pair_test->app_state_->get_system_state()->equals_to(*visited_pair->app_state_->get_system_state(),
+ *get_remote_app().get_remote_process_memory())))
continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
}
}
-LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args) {}
+LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args, true) {}
LivenessChecker::~LivenessChecker()
{
xbt_automaton_free(property_automaton_);
/* Add all enabled actors to the interleave set of the initial state */
for (auto const& [aid, _] : next_pair->app_state_->get_actors_list())
if (next_pair->app_state_->is_actor_enabled(aid))
- next_pair->app_state_->mark_todo(aid);
+ next_pair->app_state_->consider_one(aid);
next_pair->requests = next_pair->app_state_->count_todo();
/* FIXME : get search_cycle value for each accepting state */
}
}
- current_pair->app_state_->execute_next(current_pair->app_state_->next_transition());
+ current_pair->app_state_->execute_next(current_pair->app_state_->next_transition(), get_remote_app());
XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str());
/* Update the dot output */
namespace simgrid::mc::udpor {
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
{
// Initialize the map
}
"one transition of the state of an visited event is enabled, yet no\n"
"state was actually enabled. Please report this as a bug.\n"
"*********************************\n\n");
- state.execute_next(next_actor);
+ state.execute_next(next_actor, get_remote_app());
}
void UdporChecker::restore_program_state_to(const State& stateC)
auto next_state = this->get_current_state();
// In UDPOR, we care about all enabled transitions in a given state
- next_state->mark_all_enabled_todo();
+ next_state->consider_all();
return next_state;
}
xbt_assert(argc >= 2, "Missing arguments");
// Currently, we need this before sg_config_init:
- simgrid::mc::cfg_do_model_check = true;
+ simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::CHECKER_SIDE;
// The initialization function can touch argv.
// We make a copy of argv before modifying it in order to pass the original value to the model-checked application:
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
#include "src/mc/mc.h"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/remote/AppSide.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
bool actor_is_enabled(kernel::actor::ActorImpl* actor)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
#endif
// Now, we are in the client app, no need for remote memory reading.
bool request_is_visible(const kernel::actor::Simcall* req)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
#endif
if (req->observer_ == nullptr)
return false;
int MC_random(int min, int max)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
#endif
if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
static simgrid::xbt::random::XbtRandom prng;
{
// Cannot used xbt_assert here, or it would be an infinite recursion.
#if SIMGRID_HAVE_MC
- if (mc_model_checker != nullptr)
- xbt_die("This should be called from the client side");
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
if (not prop) {
if (MC_is_active())
simgrid::mc::AppSide::get()->report_assertion_failure();
int MC_is_active()
{
- return simgrid::mc::cfg_do_model_check;
+ return simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::APP_SIDE ||
+ simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::CHECKER_SIDE;
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
simgrid::mc::AppSide::get()->declare_symbol(name, value);
#endif
}
void MC_ignore(void* addr, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_memory(addr, size);
#endif
}
void MC_ignore_heap(void *address, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
simgrid::mc::AppSide::get()->ignore_heap(address, size);
#endif
}
void MC_unignore_heap(void* address, size_t size)
{
#if SIMGRID_HAVE_MC
- xbt_assert(mc_model_checker == nullptr);
+ xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+ "This should be called from the client side");
simgrid::mc::AppSide::get()->unignore_heap(address, size);
#endif
}
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg);
-bool simgrid::mc::cfg_do_model_check = false;
+simgrid::mc::ModelCheckingMode simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::NONE;
static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
{
/* Replay (this part is enabled even if MC it disabled) */
simgrid::config::Flag<std::string> _sg_mc_record_path{
"model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "",
- [](std::string_view value) { MC_record_path() = value; }};
+ [](std::string_view value) {
+ xbt_assert(simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::NONE ||
+ simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::REPLAY,
+ "Specifying a MC replay path is not allowed when running the model-checker in mode %s. "
+ "Either remove the model-check/replay parameter, or execute your code out of simgrid-mc.",
+ to_c_str(simgrid::mc::model_checking_mode));
+ simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::REPLAY;
+ MC_record_path() = value;
+ }};
#if SIMGRID_HAVE_MC
simgrid::config::Flag<bool> _sg_mc_timeout{
/********************************** Configuration of MC **************************************/
namespace simgrid::mc {
bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
-extern XBT_PUBLIC bool cfg_do_model_check;
+XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
+extern XBT_PUBLIC ModelCheckingMode model_checking_mode;
};
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
class PageStore;
class ChunkedData;
-class ModelChecker;
class AddressSpace;
class RemoteProcessMemory;
class Snapshot;
class Variable;
class Transition;
class Frame;
-class ActorInformation;
class Session;
class Exploration;
} // namespace simgrid::mc
-// TODO, try to get rid of the global ModelChecker variable
-extern simgrid::mc::ModelChecker* mc_model_checker;
-
#endif
if (instance_)
return instance_.get();
- simgrid::mc::cfg_do_model_check = true;
+ simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE;
setvbuf(stdout, nullptr, _IOLBF, 0);
xbt_assert(errno == 0 && raise(SIGSTOP) == 0, "Could not wait for the model-checker (errno = %d: %s)", errno,
strerror(errno));
- s_mc_message_initial_addresses_t message = {};
- message.type = MessageType::INITIAL_ADDRESSES;
- message.mmalloc_default_mdp = mmalloc_get_current_heap();
- xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
-
instance_->handle_messages();
return instance_.get();
}
if (terminate_asap)
::_Exit(0);
}
+void AppSide::handle_initial_addresses()
+{
+ this->need_memory_info_ = true;
+ s_mc_message_initial_addresses_reply_t answer = {};
+ answer.type = MessageType::INITIAL_ADDRESSES_REPLY;
+ answer.mmalloc_default_mdp = mmalloc_get_current_heap();
+ xbt_assert(channel_.send(answer) == 0, "Could not send response with initial addresses.");
+}
void AppSide::handle_actors_status() const
{
auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \
sizeof(_type_))
-void AppSide::handle_messages() const
+void AppSide::handle_messages()
{
while (true) { // Until we get a CONTINUE message
XBT_DEBUG("Waiting messages from model-checker");
handle_finalize((s_mc_message_int_t*)message_buffer.data());
break;
+ case MessageType::INITIAL_ADDRESSES:
+ assert_msg_size("INITIAL_ADDRESSES", s_mc_message_t);
+ handle_initial_addresses();
+ break;
+
case MessageType::ACTORS_STATUS:
assert_msg_size("ACTORS_STATUS", s_mc_message_t);
handle_actors_status();
}
}
-void AppSide::main_loop() const
+void AppSide::main_loop()
{
simgrid::mc::processes_time.resize(simgrid::kernel::actor::ActorImpl::get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
}
}
-void AppSide::report_assertion_failure() const
+void AppSide::report_assertion_failure()
{
xbt_assert(channel_.send(MessageType::ASSERTION_FAILED) == 0, "Could not send assertion to model-checker");
this->handle_messages();
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::ignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
void AppSide::unignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::declare_symbol(const char* name, int* value) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_) {
+ XBT_CRITICAL("Ignore AppSide::declare_symbol(%s)", name);
return;
+ }
s_mc_message_register_symbol_t message = {};
message.type = MessageType::REGISTER_SYMBOL;
*/
void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
private:
Channel channel_;
static std::unique_ptr<AppSide> instance_;
+ bool need_memory_info_ = false; /* by default we don't send memory info, unless we got a INITIAL_ADDRESSES */
public:
AppSide();
explicit AppSide(int fd) : channel_(fd) {}
- void handle_messages() const;
+ void handle_messages();
private:
void handle_deadlock_check(const s_mc_message_t* msg) const;
void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const;
void handle_finalize(const s_mc_message_int_t* msg) const;
+ void handle_initial_addresses();
void handle_actors_status() const;
void handle_actors_maxpid() const;
public:
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
- XBT_ATTRIB_NORETURN void main_loop() const;
- void report_assertion_failure() const;
+ XBT_ATTRIB_NORETURN void main_loop();
+ void report_assertion_failure();
void ignore_memory(void* addr, std::size_t size) const;
void ignore_heap(void* addr, std::size_t size) const;
void unignore_heap(void* addr, std::size_t size) const;
return 0;
}
-ssize_t Channel::receive(void* message, size_t size, bool block) const
+ssize_t Channel::receive(void* message, size_t size) const
{
- ssize_t res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
+ ssize_t res = recv(this->socket_, message, size, 0);
if (res != -1) {
if (is_valid_MessageType(*static_cast<int*>(message))) {
XBT_DEBUG("Receive %s (requested %zu; received %zd)", to_c_str(*static_cast<MessageType*>(message)), size, res);
template <class M> static constexpr bool messageType() { return std::is_class_v<M> && std::is_trivial_v<M>; }
public:
+ Channel() = default;
explicit Channel(int sock) : socket_(sock) {}
~Channel();
}
// Receive
- ssize_t receive(void* message, size_t size, bool block = true) const;
+ ssize_t receive(void* message, size_t size) const;
template <class M> typename std::enable_if_t<messageType<M>(), ssize_t> receive(M& m) const
{
return this->receive(&m, sizeof(M));
}
int get_socket() const { return socket_; }
+ void reset_socket(int socket) { socket_ = socket; }
};
} // namespace simgrid::mc
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/remote/CheckerSide.hpp"
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
+#include "src/mc/sosp/RemoteProcessMemory.hpp"
+#include "xbt/system_error.hpp"
+
+#ifdef __linux__
+#include <sys/personality.h>
+#include <sys/prctl.h>
+#endif
+
+#include <boost/tokenizer.hpp>
#include <csignal>
+#include <fcntl.h>
+#include <sys/ptrace.h>
#include <sys/wait.h>
+#ifdef __linux__
+#define WAITPID_CHECKED_FLAGS __WALL
+#else
+#define WAITPID_CHECKED_FLAGS 0
+#endif
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkerside, mc, "MC communication with the application");
+
+static simgrid::config::Flag<std::string> _sg_mc_setenv{
+ "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
+ [](std::string_view value) {
+ xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
+ "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
+ }};
+
namespace simgrid::mc {
-void CheckerSide::start(void (*handler)(int, short, void*), ModelChecker* mc)
+XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<char*>& args)
+{
+ /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
+ * env variable is set. If so, MC mode is assumed, and the client is setup from its side
+ */
+
+#ifdef __linux__
+ // Make sure we do not outlive our parent
+ sigset_t mask;
+ sigemptyset(&mask);
+ xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
+ xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
+
+ // Make sure that the application process layout is not randomized, so that the info we gather is stable over re-execs
+ if (personality(ADDR_NO_RANDOMIZE) == -1) {
+ XBT_ERROR("Could not set the NO_RANDOMIZE personality");
+ throw xbt::errno_error();
+ }
+#endif
+
+ // Remove CLOEXEC to pass the socket to the application
+ int fdflags = fcntl(socket, F_GETFD, 0);
+ xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
+ "Could not remove CLOEXEC for socket");
+
+ setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
+
+ /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
+ using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
+ boost::char_separator<char> semicol_sep(";");
+ boost::char_separator<char> equal_sep("=");
+ Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
+ for (const auto& token : token_vars) {
+ std::vector<std::string> kv;
+ Tokenizer token_kv(token, equal_sep);
+ for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
+ kv.push_back(t);
+ xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
+ token.c_str());
+ XBT_INFO("setenv '%s'='%s'", kv[0].c_str(), kv[1].c_str());
+ setenv(kv[0].c_str(), kv[1].c_str(), 1);
+ }
+
+ /* And now, exec the child process */
+ int i = 1;
+ while (args[i] != nullptr && args[i][0] == '-')
+ i++;
+
+ xbt_assert(args[i] != nullptr,
+ "Unable to find a binary to exec on the command line. Did you only pass config flags?");
+
+ execvp(args[i], args.data() + i);
+ XBT_CRITICAL("The model-checked process failed to exec(%s): %s.\n"
+ " Make sure that your binary exists on disk and is executable.",
+ args[i], strerror(errno));
+ if (strchr(args[i], '=') != nullptr)
+ XBT_CRITICAL("If you want to pass environment variables to the application, please use --cfg=model-check/setenv:%s",
+ args[i]);
+
+ xbt_die("Aborting now.");
+}
+
+static void wait_application_process(pid_t pid)
{
+ XBT_DEBUG("Waiting for the model-checked process");
+ int status;
+
+ // The model-checked process SIGSTOP itself to signal it's ready:
+ xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
+ "Could not wait model-checked process");
+
+ errno = 0;
+#ifdef __linux__
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
+#elif defined BSD
+ ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
+#else
+#error "no ptrace equivalent coded for this platform"
+#endif
+ xbt_assert(errno == 0,
+ "Ptrace does not seem to be usable in your setup (errno: %d). "
+ "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
+ "If it does not help, please report this bug.",
+ errno);
+}
+
+void CheckerSide::setup_events()
+{
+ if (base_ != nullptr)
+ event_base_free(base_.get());
auto* base = event_base_new();
base_.reset(base);
- auto* socket_event = event_new(base, get_channel().get_socket(), EV_READ | EV_PERSIST, handler, mc);
- event_add(socket_event, nullptr);
- socket_event_.reset(socket_event);
+ socket_event_ = event_new(
+ base, get_channel().get_socket(), EV_READ | EV_PERSIST,
+ [](evutil_socket_t sig, short events, void* arg) {
+ auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
+ if (events == EV_READ) {
+ std::array<char, MC_MESSAGE_LENGTH> buffer;
+ ssize_t size = recv(checker->get_channel().get_socket(), buffer.data(), buffer.size(), MSG_DONTWAIT);
+ if (size == -1) {
+ XBT_ERROR("Channel::receive failure: %s", strerror(errno));
+ if (errno != EAGAIN)
+ throw simgrid::xbt::errno_error();
+ }
- auto* signal_event = event_new(base, SIGCHLD, EV_SIGNAL | EV_PERSIST, handler, mc);
- event_add(signal_event, nullptr);
- signal_event_.reset(signal_event);
+ if (not checker->handle_message(buffer.data(), size))
+ checker->break_loop();
+ } else {
+ xbt_die("Unexpected event");
+ }
+ },
+ this);
+ event_add(socket_event_, nullptr);
+
+ signal_event_ = event_new(
+ base, SIGCHLD, EV_SIGNAL | EV_PERSIST,
+ [](evutil_socket_t sig, short events, void* arg) {
+ auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
+ if (events == EV_SIGNAL) {
+ if (sig == SIGCHLD)
+ checker->handle_waitpid();
+ else
+ xbt_die("Unexpected signal: %d", sig);
+ } else {
+ xbt_die("Unexpected event");
+ }
+ },
+ this);
+ event_add(signal_event_, nullptr);
}
-void CheckerSide::dispatch() const
+CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_introspection) : running_(true)
+{
+ // Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
+ // and the application process (child)
+ int sockets[2];
+ xbt_assert(socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets) != -1, "Could not create socketpair");
+
+ pid_ = fork();
+ xbt_assert(pid_ >= 0, "Could not fork model-checked process");
+
+ if (pid_ == 0) { // Child
+ ::close(sockets[1]);
+ run_child_process(sockets[0], args);
+ DIE_IMPOSSIBLE;
+ }
+
+ // Parent (model-checker):
+ ::close(sockets[0]);
+ channel_.reset_socket(sockets[1]);
+
+ setup_events();
+ wait_application_process(pid_);
+
+ // Request the initial memory on need
+ if (need_memory_introspection) {
+ channel_.send(MessageType::INITIAL_ADDRESSES);
+ s_mc_message_initial_addresses_reply_t answer;
+ ssize_t answer_size = channel_.receive(answer);
+ xbt_assert(answer_size != -1, "Could not receive message");
+ xbt_assert(answer.type == MessageType::INITIAL_ADDRESSES_REPLY,
+ "The received message is not the INITIAL_ADDRESS_REPLY I was expecting but of type %s",
+ to_c_str(answer.type));
+ xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
+
+ /* We now have enough info to create the memory address space */
+ remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, answer.mmalloc_default_mdp);
+ }
+
+ wait_for_requests();
+}
+
+CheckerSide::~CheckerSide()
+{
+ event_del(socket_event_);
+ event_free(socket_event_);
+ event_del(signal_event_);
+ event_free(signal_event_);
+
+ if (running()) {
+ XBT_DEBUG("Killing process");
+ finalize(true);
+ kill(get_pid(), SIGKILL);
+ terminate();
+ handle_waitpid();
+ }
+}
+
+void CheckerSide::finalize(bool terminate_asap)
+{
+ s_mc_message_int_t m = {};
+ m.type = MessageType::FINALIZE;
+ m.value = terminate_asap;
+ xbt_assert(get_channel().send(m) == 0, "Could not ask the app to finalize on need");
+
+ s_mc_message_t answer;
+ ssize_t s = get_channel().receive(answer);
+ xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+ xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+ xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
+ "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
+ (int)answer.type, (int)MessageType::FINALIZE_REPLY);
+}
+
+void CheckerSide::dispatch_events() const
{
event_base_dispatch(base_.get());
}
event_base_loopbreak(base_.get());
}
+bool CheckerSide::handle_message(const char* buffer, ssize_t size)
+{
+ s_mc_message_t base_message;
+ xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
+ memcpy(&base_message, buffer, sizeof(base_message));
+
+ switch (base_message.type) {
+ case MessageType::IGNORE_HEAP: {
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_heap_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ get_remote_memory()->ignore_heap(region);
+ } else {
+ XBT_INFO("Ignoring a IGNORE_HEAP message because we don't need to introspect memory.");
+ }
+ break;
+ }
+
+ case MessageType::UNIGNORE_HEAP: {
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an UNIGNORE_HEAP message because we don't need to introspect memory.");
+ }
+ break;
+ }
+
+ case MessageType::IGNORE_MEMORY: {
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->ignore_region(message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an IGNORE_MEMORY message because we don't need to introspect memory.");
+ }
+ break;
+ }
+
+ case MessageType::STACK_REGION: {
+ if (remote_memory_ != nullptr) {
+ s_mc_message_stack_region_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->stack_areas().push_back(message.stack_region);
+ } else {
+ XBT_INFO("Ignoring an STACK_REGION message because we don't need to introspect memory.");
+ }
+ break;
+ }
+
+ case MessageType::REGISTER_SYMBOL: {
+ s_mc_message_register_symbol_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
+ XBT_DEBUG("Received symbol: %s", message.name.data());
+
+ LivenessChecker::automaton_register_symbol(*get_remote_memory(), message.name.data(), remote((int*)message.data));
+ break;
+ }
+
+ case MessageType::WAITING:
+ return false;
+
+ case MessageType::ASSERTION_FAILED:
+ Exploration::get_instance()->report_assertion_failure();
+ break;
+
+ default:
+ xbt_die("Unexpected message from model-checked application");
+ }
+ return true;
+}
+
+void CheckerSide::wait_for_requests()
+{
+ /* Resume the application */
+ if (get_channel().send(MessageType::CONTINUE) != 0)
+ throw xbt::errno_error();
+ clear_memory_cache();
+
+ if (running())
+ dispatch_events();
+}
+
+void CheckerSide::clear_memory_cache()
+{
+ if (remote_memory_)
+ remote_memory_->clear_cache();
+}
+
+void CheckerSide::handle_waitpid()
+{
+ XBT_DEBUG("Check for wait event");
+ int status;
+ pid_t pid;
+ while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
+ if (pid == -1) {
+ if (errno == ECHILD) { // No more children:
+ xbt_assert(not this->running(), "Inconsistent state");
+ break;
+ } else {
+ XBT_ERROR("Could not wait for pid");
+ throw simgrid::xbt::errno_error();
+ }
+ }
+
+ if (pid == get_pid()) {
+ // From PTRACE_O_TRACEEXIT:
+#ifdef __linux__
+ if (status >> 8 == (SIGTRAP | (PTRACE_EVENT_EXIT << 8))) {
+ unsigned long eventmsg;
+ xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid, 0, &eventmsg) != -1, "Could not get exit status");
+ status = static_cast<int>(eventmsg);
+ if (WIFSIGNALED(status)) {
+ this->terminate();
+ Exploration::get_instance()->report_crash(status);
+ }
+ }
+#endif
+
+ // We don't care about non-lethal signals, just reinject them:
+ if (WIFSTOPPED(status)) {
+ XBT_DEBUG("Stopped with signal %i", (int)WSTOPSIG(status));
+ errno = 0;
+#ifdef __linux__
+ ptrace(PTRACE_CONT, pid, 0, WSTOPSIG(status));
+#elif defined BSD
+ ptrace(PT_CONTINUE, pid, (caddr_t)1, WSTOPSIG(status));
+#endif
+ xbt_assert(errno == 0, "Could not PTRACE_CONT");
+ }
+
+ else if (WIFSIGNALED(status)) {
+ this->terminate();
+ Exploration::get_instance()->report_crash(status);
+ } else if (WIFEXITED(status)) {
+ XBT_DEBUG("Child process is over");
+ this->terminate();
+ }
+ }
+ }
+}
+
} // namespace simgrid::mc
namespace simgrid::mc {
+/* CheckerSide: All what the checker needs to interact with a given application process */
+
class CheckerSide {
+ event* socket_event_;
+ event* signal_event_;
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
- std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
- std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, &event_free};
+ std::unique_ptr<RemoteProcessMemory> remote_memory_;
Channel channel_;
+ bool running_ = false;
+ pid_t pid_;
+
+ void setup_events(); // Part of the initialization
+ void clear_memory_cache();
+ void handle_waitpid();
public:
- explicit CheckerSide(int sockfd) : channel_(sockfd) {}
+ explicit CheckerSide(const std::vector<char*>& args, bool need_memory_introspection);
+ ~CheckerSide();
// No copy:
CheckerSide(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide&&) = delete;
+ /* Communicating with the application */
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
- void start(void (*handler)(int, short, void*), ModelChecker* mc);
- void dispatch() const;
+ bool handle_message(const char* buffer, ssize_t size);
+ void dispatch_events() const;
void break_loop() const;
+ void wait_for_requests();
+
+ /** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
+ void finalize(bool terminate_asap = false);
+
+ /* Interacting with the application process */
+ pid_t get_pid() const { return pid_; }
+ bool running() const { return running_; }
+ void terminate() { running_ = false; }
+ RemoteProcessMemory* get_remote_memory() { return remote_memory_.get(); }
};
} // namespace simgrid::mc
// ***** Messages
namespace simgrid::mc {
-XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
- STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
- SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID,
- ACTORS_MAXPID_REPLY, FINALIZE, FINALIZE_REPLY);
+XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, INITIAL_ADDRESSES_REPLY, CONTINUE, IGNORE_HEAP,
+ UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK,
+ DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE, SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED,
+ ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID, ACTORS_MAXPID_REPLY, FINALIZE,
+ FINALIZE_REPLY);
} // namespace simgrid::mc
constexpr unsigned MC_MESSAGE_LENGTH = 512;
};
/* Client->Server */
-struct s_mc_message_initial_addresses_t {
- simgrid::mc::MessageType type;
- xbt_mheap_t mmalloc_default_mdp;
-};
-
struct s_mc_message_ignore_heap_t {
simgrid::mc::MessageType type;
int block;
};
/* Server -> client */
+struct s_mc_message_initial_addresses_reply_t {
+ simgrid::mc::MessageType type;
+ xbt_mheap_t mmalloc_default_mdp;
+};
+
struct s_mc_message_simcall_execute_t {
simgrid::mc::MessageType type;
aid_t aid_;
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/sosp/Region.hpp"
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_forward.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
namespace simgrid::mc {
-Region::Region(PageStore& store, RegionType region_type, void* start_addr, size_t size)
+Region::Region(PageStore& store, RemoteProcessMemory& memory, RegionType region_type, void* start_addr, size_t size)
: region_type_(region_type), start_addr_(start_addr), size_(size)
{
xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize - 1)) == 0, "Start address not at the beginning of a page");
- chunks_ = ChunkedData(store, mc_model_checker->get_remote_process_memory(), RemotePtr<void>(start_addr),
- mmu::chunk_count(size));
+ chunks_ = ChunkedData(store, memory, RemotePtr<void>(start_addr), mmu::chunk_count(size));
}
/** @brief Restore a region from a snapshot
*
* @param region Target region
*/
-void Region::restore() const
+void Region::restore(RemoteProcessMemory& memory) const
{
xbt_assert(((start().address()) & (xbt_pagesize - 1)) == 0, "Not at the beginning of a page");
xbt_assert(simgrid::mc::mmu::chunk_count(size()) == get_chunks().page_count());
for (size_t i = 0; i != get_chunks().page_count(); ++i) {
auto* target_page = (void*)simgrid::mc::mmu::join(i, (std::uintptr_t)(void*)start().address());
const void* source_page = get_chunks().page(i);
- mc_model_checker->get_remote_process_memory().write_bytes(source_page, xbt_pagesize, remote(target_page));
+ memory.write_bytes(source_page, xbt_pagesize, remote(target_page));
}
}
ChunkedData chunks_;
public:
- Region(PageStore& store, RegionType type, void* start_addr, size_t size);
+ Region(PageStore& store, RemoteProcessMemory& memory, RegionType type, void* start_addr, size_t size);
Region(Region const&) = delete;
Region& operator=(Region const&) = delete;
Region(Region&& that) = delete;
bool contain(RemotePtr<void> p) const { return p >= start() && p < end(); }
/** @brief Restore a region from a snapshot */
- void restore() const;
+ void restore(RemoteProcessMemory& memory) const;
/** @brief Read memory that was snapshotted in this region
*
#include "src/mc/sosp/RemoteProcessMemory.hpp"
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/file.hpp"
#include "xbt/log.h"
+#include "xbt/system_error.hpp"
#include <fcntl.h>
#include <libunwind-ptrace.h>
// ***** RemoteProcessMemory
-RemoteProcessMemory::RemoteProcessMemory(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
-
-void RemoteProcessMemory::init(xbt_mheap_t mmalloc_default_mdp)
+RemoteProcessMemory::RemoteProcessMemory(pid_t pid, xbt_mheap_t mmalloc_default_mdp) : AddressSpace(this), pid_(pid)
{
this->heap_address = remote(mmalloc_default_mdp);
_UPT_destroy(context);
unw_destroy_addr_space(as);
}
+
} // namespace simgrid::mc
namespace simgrid::mc {
-class ActorInformation {
-public:
- /** MCed address of the process */
- RemotePtr<kernel::actor::ActorImpl> address{nullptr};
- Remote<kernel::actor::ActorImpl> copy;
-
- /** Hostname (owned by `mc_model_checker->hostnames_`) */
- const std::string* hostname = nullptr;
- std::string name;
-
- void clear()
- {
- name.clear();
- address = nullptr;
- hostname = nullptr;
- }
-};
-
struct IgnoredRegion {
std::uint64_t addr;
std::size_t size;
std::size_t size;
};
-/** The Application's process memory, seen from the Checker perspective
- *
- * Responsibilities:
+/** The Application's process memory, seen from the Checker perspective. This class is not needed if you don't need to
+ * introspect the application process.
*
- * - reading from the process memory (`AddressSpace`);
- * - accessing the system state of the process (heap, …);
- * - privatization;
- * - stack unwinding;
- * - etc.
+ * Responsabilities:
+ * - reading from the process memory (`AddressSpace`);
+ * - accessing the system state of the process (heap, …);
+ * - stack unwinding;
+ * - etc.
*/
class RemoteProcessMemory final : public AddressSpace {
private:
static constexpr int cache_malloc = 2;
public:
- explicit RemoteProcessMemory(pid_t pid);
+ explicit RemoteProcessMemory(pid_t pid, xbt_mheap_t mmalloc_default_mdp);
~RemoteProcessMemory() override;
- void init(xbt_mheap_t mmalloc_default_mdp);
RemoteProcessMemory(RemoteProcessMemory const&) = delete;
RemoteProcessMemory(RemoteProcessMemory&&) = delete;
// Heap access:
xbt_mheap_t get_heap()
{
- if (not(this->cache_flags_ & RemoteProcessMemory::cache_heap))
- this->refresh_heap();
+ if (not(cache_flags_ & RemoteProcessMemory::cache_heap))
+ refresh_heap();
return this->heap.get();
}
const malloc_info* get_malloc_info()
std::vector<IgnoredRegion> const& ignored_regions() const { return ignored_regions_; }
void ignore_region(std::uint64_t address, std::size_t size);
- pid_t pid() const { return pid_; }
-
bool in_maestro_stack(RemotePtr<void> p) const
{
return p >= this->maestro_stack_start_ && p < this->maestro_stack_end_;
}
- bool running() const { return running_; }
-
- void terminate() { running_ = false; }
-
void ignore_global_variable(const char* name) const
{
for (std::shared_ptr<ObjectInformation> const& info : this->object_infos)
void refresh_heap();
void refresh_malloc_info();
- pid_t pid_ = -1;
- bool running_ = false;
+ pid_t pid_ = -1;
std::vector<xbt::VmMap> memory_map_;
RemotePtr<void> maestro_stack_start_;
RemotePtr<void> maestro_stack_end_;
/************************************* Take Snapshot ************************************/
/****************************************************************************************/
-void Snapshot::snapshot_regions(RemoteProcessMemory& process_memory)
+void Snapshot::snapshot_regions(RemoteProcessMemory& memory)
{
snapshot_regions_.clear();
- for (auto const& object_info : process_memory.object_infos)
- add_region(RegionType::Data, object_info.get(), object_info->start_rw, object_info->end_rw - object_info->start_rw);
+ for (auto const& object_info : memory.object_infos)
+ add_region(RegionType::Data, memory, object_info.get(), object_info->start_rw,
+ object_info->end_rw - object_info->start_rw);
- const s_xbt_mheap_t* heap = process_memory.get_heap();
+ const s_xbt_mheap_t* heap = memory.get_heap();
void* start_heap = heap->base;
void* end_heap = heap->breakval;
- add_region(RegionType::Heap, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
- heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process_memory.get_malloc_info());
+ add_region(RegionType::Heap, memory, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
+ heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, memory.get_malloc_info());
}
/** @brief Checks whether the variable is in scope for a given IP.
}
static void fill_local_variables_values(mc_stack_frame_t stack_frame, Frame* scope,
- std::vector<s_local_variable_t>& result)
+ std::vector<s_local_variable_t>& result, AddressSpace* memory)
{
if (not scope || not scope->range.contain(stack_frame->ip))
return;
if (current_variable.address != nullptr)
new_var.address = current_variable.address;
else if (not current_variable.location_list.empty()) {
- dwarf::Location location = simgrid::dwarf::resolve(current_variable.location_list, current_variable.object_info,
- &(stack_frame->unw_cursor), (void*)stack_frame->frame_base,
- &mc_model_checker->get_remote_process_memory());
+ dwarf::Location location =
+ simgrid::dwarf::resolve(current_variable.location_list, current_variable.object_info,
+ &(stack_frame->unw_cursor), (void*)stack_frame->frame_base, memory);
xbt_assert(location.in_memory(), "Cannot handle non-address variable");
new_var.address = location.address();
// Recursive processing of nested scopes:
for (Frame& nested_scope : scope->scopes)
- fill_local_variables_values(stack_frame, &nested_scope, result);
+ fill_local_variables_values(stack_frame, &nested_scope, result, memory);
}
-static std::vector<s_local_variable_t> get_local_variables_values(std::vector<s_mc_stack_frame_t>& stack_frames)
+static std::vector<s_local_variable_t> get_local_variables_values(std::vector<s_mc_stack_frame_t>& stack_frames,
+ AddressSpace* memory)
{
std::vector<s_local_variable_t> variables;
for (s_mc_stack_frame_t& stack_frame : stack_frames)
- fill_local_variables_values(&stack_frame, stack_frame.frame, variables);
+ fill_local_variables_values(&stack_frame, stack_frame.frame, variables, memory);
return variables;
}
-static std::vector<s_mc_stack_frame_t> unwind_stack_frames(UnwindContext* stack_context)
+static std::vector<s_mc_stack_frame_t> unwind_stack_frames(UnwindContext* stack_context,
+ const RemoteProcessMemory* process_memory)
{
- const RemoteProcessMemory* process_memory = &mc_model_checker->get_remote_process_memory();
std::vector<s_mc_stack_frame_t> result;
unw_cursor_t c = stack_context->cursor();
st.context.initialize(process_memory, &context);
- st.stack_frames = unwind_stack_frames(&st.context);
- st.local_variables = get_local_variables_values(st.stack_frames);
+ st.stack_frames = unwind_stack_frames(&st.context, &process_memory);
+ st.local_variables = get_local_variables_values(st.stack_frames, &process_memory);
unw_word_t sp = st.stack_frames[0].sp;
s_mc_snapshot_ignored_data_t ignored_data;
ignored_data.start = (void*)region.addr;
ignored_data.data.resize(region.size);
- // TODO, we should do this once per privatization segment:
get_remote_process_memory()->read_bytes(ignored_data.data.data(), region.size, remote(region.addr));
ignored_data_.push_back(std::move(ignored_data));
}
ignore_restore();
}
-void Snapshot::add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size)
+void Snapshot::add_region(RegionType type, RemoteProcessMemory& memory, ObjectInformation* object_info,
+ void* start_addr, std::size_t size)
{
if (type == RegionType::Data)
xbt_assert(object_info, "Missing object info for object.");
else if (type == RegionType::Heap)
xbt_assert(not object_info, "Unexpected object info for heap region.");
- auto* region = new Region(page_store_, type, start_addr, size);
+ auto* region = new Region(page_store_, memory, type, start_addr, size);
region->object_info(object_info);
snapshot_regions_.push_back(std::unique_ptr<Region>(region));
}
// Restore regions
for (std::unique_ptr<Region> const& region : snapshot_regions_) {
- if (region) // privatized variables are not snapshotted
- region.get()->restore();
+ region->restore(memory);
}
ignore_restore();
#ifndef SIMGRID_MC_SNAPSHOT_HPP
#define SIMGRID_MC_SNAPSHOT_HPP
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/sosp/Region.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
Region* get_region(const void* addr, Region* hinted_region) const;
void restore(RemoteProcessMemory& memory) const;
- bool operator==(const Snapshot& other);
- bool operator!=(const Snapshot& other) { return not(*this == other); }
+ bool equals_to(const Snapshot& other, RemoteProcessMemory& memory);
// To be private
long num_state_;
std::vector<s_mc_snapshot_ignored_data_t> ignored_data_;
private:
- void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size);
- void snapshot_regions(RemoteProcessMemory& process_memory);
- void snapshot_stacks(RemoteProcessMemory& process_memory);
+ void add_region(RegionType type, RemoteProcessMemory& memory, ObjectInformation* object_info, void* start_addr,
+ std::size_t size);
+ void snapshot_regions(RemoteProcessMemory& memory);
+ void snapshot_stacks(RemoteProcessMemory& memory);
void handle_ignore();
void ignore_restore() const;
hash_type do_hash() const;
using simgrid::mc::Region;
class snap_test_helper {
static simgrid::mc::PageStore page_store_;
+ static std::unique_ptr<simgrid::mc::RemoteProcessMemory> memory_;
public:
static void init_memory(void* mem, size_t size);
static void compare_region_parts();
static void read_pointer();
- static void cleanup()
- {
- delete mc_model_checker;
- mc_model_checker = nullptr;
- }
-
- static std::unique_ptr<simgrid::mc::RemoteProcessMemory> process;
+ static void cleanup() { memory_ = nullptr; }
};
// static member variables init.
-std::unique_ptr<simgrid::mc::RemoteProcessMemory> snap_test_helper::process = nullptr;
simgrid::mc::PageStore snap_test_helper::page_store_(500);
+std::unique_ptr<simgrid::mc::RemoteProcessMemory> snap_test_helper::memory_ = nullptr;
void snap_test_helper::init_memory(void* mem, size_t size)
{
REQUIRE(xbt_pagesize == getpagesize());
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
- process = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid());
- process->init(nullptr);
- mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
+ memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid(), nullptr);
}
snap_test_helper::prologue_return snap_test_helper::prologue(int n)
// Init memory and take snapshots:
init_memory(source, byte_size);
- auto* region0 = new simgrid::mc::Region(page_store_, simgrid::mc::RegionType::Data, source, byte_size);
+ auto* region0 =
+ new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
for (int i = 0; i < n; i += 2) {
init_memory((char*)source + i * xbt_pagesize, xbt_pagesize);
}
- auto* region = new simgrid::mc::Region(page_store_, simgrid::mc::RegionType::Data, source, byte_size);
+ auto* region = new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
void* destination = mmap(nullptr, byte_size, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
INFO("Could not allocate destination memory");
}
}
+int some_global_variable = 42;
+void* some_global_pointer = &some_global_variable;
void snap_test_helper::read_pointer()
{
prologue_return ret = prologue(1);
- memcpy(ret.src, &mc_model_checker, sizeof(void*));
- const simgrid::mc::Region region2(page_store_, simgrid::mc::RegionType::Data, ret.src, ret.size);
+ memcpy(ret.src, &some_global_pointer, sizeof(void*));
+ const simgrid::mc::Region region2(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, ret.src, ret.size);
INFO("Mismtach in MC_region_read_pointer()");
- REQUIRE(MC_region_read_pointer(®ion2, ret.src) == mc_model_checker);
+ REQUIRE(MC_region_read_pointer(®ion2, ret.src) == some_global_pointer);
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
#include <simgrid/config.h>
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/transition/TransitionActorJoin.hpp"
#include "src/mc/transition/TransitionAny.hpp"
return xbt::string_printf("label = \"[(%ld)] %s\", color = %s, fontcolor = %s", aid_, Transition::to_c_str(type_),
color, color);
}
-void Transition::replay() const
+void Transition::replay(RemoteApp& app) const
{
replayed_transitions_++;
#if SIMGRID_HAVE_MC
- mc_model_checker->handle_simcall(aid_, times_considered_, false);
- mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
+ app.handle_simcall(aid_, times_considered_, false);
+ app.wait_for_requests();
#endif
}
virtual std::string dot_string() const;
/* Moves the application toward a path that was already explored, but don't change the current transition */
- void replay() const;
+ void replay(RemoteApp& app) const;
virtual bool depends(const Transition* other) const { return true; }
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#if SIMGRID_HAVE_MC
#include "src/mc/mc_config.hpp"
+#include "src/mc/mc_replay.hpp"
#endif
#if defined(__APPLE__)
void smpi_check_options()
{
#if SIMGRID_HAVE_MC
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
if (_sg_mc_buffering == "zero")
simgrid::config::set_value<int>("smpi/send-is-detached-thresh", 0);
else if (_sg_mc_buffering == "infty")
engine.load_platform(argv[1]);
engine.set_default_comm_data_copy_callback(smpi_comm_copy_buffer_callback);
+ xbt_assert(not MC_is_active() || smpi_cfg_privatization() != SmpiPrivStrategies::MMAP,
+ "Please use the dlopen privatization schema when model-checking SMPI code");
+
if (smpi_cfg_privatization() == SmpiPrivStrategies::DLOPEN)
smpi_init_privatization_dlopen(executable);
else
Datatype::Datatype(int size, MPI_Aint lb, MPI_Aint ub, int flags) : size_(size), lb_(lb), ub_(ub), flags_(flags)
{
this->add_f();
-#if SIMGRID_HAVE_MC
- if(MC_is_active())
- MC_ignore(&refcount_, sizeof refcount_);
-#endif
+ MC_ignore(&refcount_, sizeof refcount_);
}
// for predefined types, so refcount_ = 0.
: name_(name), id(std::to_string(ident)), size_(size), lb_(lb), ub_(ub), flags_(flags), refcount_(0)
{
id2type_lookup.try_emplace(id, this);
-#if SIMGRID_HAVE_MC
- if(MC_is_active())
- MC_ignore(&refcount_, sizeof refcount_);
-#endif
+ MC_ignore(&refcount_, sizeof refcount_);
}
Datatype::Datatype(Datatype* datatype, int* ret)
void Datatype::ref()
{
refcount_++;
-
-#if SIMGRID_HAVE_MC
- if(MC_is_active())
- MC_ignore(&refcount_, sizeof refcount_);
-#endif
+ MC_ignore(&refcount_, sizeof refcount_);
}
void Datatype::unref(MPI_Datatype datatype)
{
if (datatype->refcount_ > 0)
datatype->refcount_--;
-
-#if SIMGRID_HAVE_MC
- if(MC_is_active())
- MC_ignore(&datatype->refcount_, sizeof datatype->refcount_);
-#endif
+ MC_ignore(&datatype->refcount_, sizeof datatype->refcount_);
if (datatype->refcount_ == 0 && not(datatype->flags_ & DT_FLAG_PREDEFINED))
delete datatype;
int main()
{
- auto* process = new simgrid::mc::RemoteProcessMemory(getpid());
- process->init(nullptr);
+ auto* process = new simgrid::mc::RemoteProcessMemory(getpid(), nullptr);
simgrid::dwarf::ExpressionContext state;
state.address_space = (simgrid::mc::AddressSpace*) process;
const simgrid::mc::Variable* var;
simgrid::mc::Type* type;
- simgrid::mc::RemoteProcessMemory process(getpid());
- process.init(nullptr);
+ simgrid::mc::RemoteProcessMemory process(getpid(), nullptr);
test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));
src/mc/transition/TransitionSynchro.cpp
src/mc/transition/TransitionSynchro.hpp
- src/mc/AddressSpace.hpp
- src/mc/ModelChecker.cpp
- src/mc/ModelChecker.hpp
- src/mc/VisitedState.cpp
- src/mc/VisitedState.hpp
+ src/mc/api/guide/BasicGuide.hpp
+ src/mc/api/guide/GuidedState.hpp
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
+
+ src/mc/AddressSpace.hpp
+ src/mc/VisitedState.cpp
+ src/mc/VisitedState.hpp
src/mc/compare.cpp
src/mc/mc_exit.hpp
src/mc/mc_forward.hpp
docs/source/tuto_s4u/master-workers-lab3.cpp
docs/source/tuto_s4u/master-workers-lab4.cpp
+ docs/source/Tutorial_DAG.rst
+ docs/source/tuto_dag/dag_lab1.cpp
+ docs/source/tuto_dag/dag_lab2-1.cpp
+ docs/source/tuto_dag/dag_lab2-2.cpp
+ docs/source/tuto_dag/dag_lab2-3.cpp
+ docs/source/tuto_dag/img/dag1.svg
+ docs/source/tuto_dag/img/dag2.svg
+ docs/source/tuto_dag/img/dag.svg
+ docs/source/tuto_dag/simple_dax.xml
+ docs/source/tuto_dag/simple_dot.dot
+ docs/source/tuto_dag/simple_json.json
+ docs/source/tuto_dag/small_platform.xml
+
docs/source/Tutorial_MPI_Applications.rst
docs/source/tuto_smpi/3hosts.png
docs/source/tuto_smpi/3hosts.xml
tools/cmake/Modules/FindNS3.cmake
tools/cmake/Modules/FindPAPI.cmake
tools/cmake/Modules/FindValgrind.cmake
+ tools/cmake/Modules/nlohmann_jsonConfig.cmake
tools/cmake/Modules/pybind11Config.cmake
tools/cmake/Option.cmake
tools/cmake/Tests.cmake
endif()
endif()
+if(SIMGRID_HAVE_JSON)
+ target_link_libraries(simgrid nlohmann_json::nlohmann_json)
+endif()
+
if(NOT ${DL_LIBRARY} STREQUAL "")
SET(SIMGRID_DEP "${SIMGRID_DEP} ${DL_LIBRARY}")
endif()
--- /dev/null
+include(FindPackageHandleStandardArgs)
+set(${CMAKE_FIND_PACKAGE_NAME}_CONFIG ${CMAKE_CURRENT_LIST_FILE})
+find_package_handle_standard_args(nlohmann_json CONFIG_MODE)
+
+if(NOT TARGET nlohmann_json::nlohmann_json)
+ include("${CMAKE_CURRENT_LIST_DIR}/nlohmann_jsonTargets.cmake")
+ if((NOT TARGET nlohmann_json) AND
+ (NOT nlohmann_json_FIND_VERSION OR
+ nlohmann_json_FIND_VERSION VERSION_LESS 3.2.0))
+ add_library(nlohmann_json INTERFACE IMPORTED)
+ set_target_properties(nlohmann_json PROPERTIES
+ INTERFACE_LINK_LIBRARIES nlohmann_json::nlohmann_json
+ )
+ endif()
+endif()
if [ "$runtests" = "ON" ]; then
# exclude tests known to fail with _GLIBCXX_DEBUG
- ctest -j$NUMPROC -E '^[ps]thread-|mc-bugged1-liveness'
+ ctest -j$NUMPROC -E '^[ps]thread-|mc-bugged1-liveness' --output-on-failure
fi
cd ..
sed -n 's/.* Eigen3 library \.\+: \([^ ]*\) in .*/\1/p;T;q' ./consoleText
}
+get_json(){
+ sed -n 's/.* JSON library \.\+: \([^ ]*\) in .*/\1/p;T;q' ./consoleText
+}
+
get_ns3(){
sed -n 's/.*-- ns-3 found (v\(3[-.0-9a-z]\+\); minor:.*/\1/p;T;q' ./consoleText
}
<td class=matrix-header style=min-width:75px onclick="sortTable($((++col)),'version');">Boost</td>
<td class=matrix-header style=min-width:75px onclick="sortTable($((++col)),'version');">Cmake</td>
<td class=matrix-header style=min-width:50px onclick="sortTable($((++col)),'version');">Eigen3</td>
+ <td class=matrix-header style=min-width:50px onclick="sortTable($((++col)),'version');">JSON</td>
<td class=matrix-header style=min-width:50px onclick="sortTable($((++col)),'version');">ns-3</td>
<td class=matrix-header style=min-width:50px onclick="sortTable($((++col)),'version');">Python</td>
</tr>
compiler=$(get_compiler)
cmake=$(get_cmake)
eigen3=$(get_eigen3)
+ json=$(get_json)
ns3=$(get_ns3)
py=$(get_python)
os=$(grep -m 1 "OS Version" ./consoleText| sed "s/OS Version : \(.*\)/\1/g")
<td class="matrix-cell" style="text-align:left">$boost</td>
<td class="matrix-cell" style="text-align:left">$cmake</td>
<td class="matrix-cell" style="text-align:center">$eigen3</td>
+ <td class="matrix-cell" style="text-align:center">$json</td>
<td class="matrix-cell" style="text-align:left">$ns3</td>
<td class="matrix-cell" style="text-align:left">$py</td>
</tr>
