sthread:
- Implement pthread_join in MC mode.
- Implement semaphore functions in sthread.
+ - Add an intricated way to verify the access to non-reentrant data structures
+ It requires code annotation, as shown in examples/sthread/stdobject/stdobject.cpp
Model checking:
- Synchronize the MBI tests with upstream.
include examples/sthread/pthread-mutex-simpledeadlock.c
include examples/sthread/pthread-producer-consumer.c
include examples/sthread/pthread-producer-consumer.tesh
+include examples/sthread/stdobject/stdobject.cpp
+include examples/sthread/stdobject/stdobject.tesh
include examples/sthread/sthread-mutex-simple.c
include examples/sthread/sthread-mutex-simple.tesh
include teshsuite/catch_simgrid.hpp
include src/mc/transition/TransitionAny.hpp
include src/mc/transition/TransitionComm.cpp
include src/mc/transition/TransitionComm.hpp
+include src/mc/transition/TransitionObjectAccess.cpp
+include src/mc/transition/TransitionObjectAccess.hpp
include src/mc/transition/TransitionRandom.cpp
include src/mc/transition/TransitionRandom.hpp
include src/mc/transition/TransitionSynchro.cpp
include src/smpi/smpiff.in
include src/smpi/smpirun.in
include src/smpi/smpitools.sh
+include src/sthread/ObjectAccess.cpp
include src/sthread/sthread.c
include src/sthread/sthread.h
include src/sthread/sthread_impl.cpp
add_executable (pthread-${x} EXCLUDE_FROM_ALL pthread-${x}.c)
set_target_properties(pthread-${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
target_link_libraries(pthread-${x} PRIVATE Threads::Threads)
- target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once cmake is >3.13
+ target_link_libraries(pthread-${x} PUBLIC "-Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13
add_dependencies(tests pthread-${x})
ADD_TESH_FACTORIES(pthread-${x} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread ${CMAKE_CURRENT_SOURCE_DIR}/pthread-${x}.tesh)
endforeach()
+# C++ tests with sthread+MC that live in their own directory
+########################################################
+foreach(example
+ stdobject)
+
+ if(SIMGRID_HAVE_MC AND ("${CMAKE_SYSTEM}" MATCHES "Linux")) # sthread is linux-only
+
+ add_executable (${example} EXCLUDE_FROM_ALL ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.cpp)
+ set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
+ target_link_libraries(${example} PRIVATE Threads::Threads)
+ target_link_libraries(${example} PUBLIC "-fPIC -Wl,-znorelro -Wl,-znoseparate-code") # TODO: convert to target_link_option once CMAKE_VERSION is >3.13
+ set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example})
+
+ add_dependencies(tests-mc ${example})
+ #ADD_TESH_FACTORIES(sthread-mc-${example} "^thread" --setenv libdir=${CMAKE_BINARY_DIR}/lib --cd ${CMAKE_BINARY_DIR}/examples/sthread/${example} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)
+ endif()
+
+ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.tesh)
+ set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/${example}.cpp)
+endforeach()
+
# Regular sthread examples: test the internal interface for debugging purpose
#############################################################################
--- /dev/null
+#include <iostream>
+#include <thread>
+#include <vector>
+
+// shared collection object
+std::vector<int> v = {1, 2, 3, 5, 8, 13};
+
+extern "C" {
+extern int sthread_access_begin(void* addr, const char* objname, const char* file, int line) __attribute__((weak));
+extern void sthread_access_end(void* addr, const char* objname, const char* file, int line) __attribute__((weak));
+}
+
+#define STHREAD_ACCESS(obj) \
+ for (bool first = sthread_access_begin(static_cast<void*>(obj), #obj, __FILE__, __LINE__) || true; first; \
+ sthread_access_end(static_cast<void*>(obj), #obj, __FILE__, __LINE__), first = false)
+
+static void thread_code()
+{
+ // Add another integer to the vector
+ STHREAD_ACCESS(&v) v.push_back(21);
+}
+
+int main()
+{
+ std::cout << "starting two helpers...\n";
+ std::thread helper1(thread_code);
+ std::thread helper2(thread_code);
+
+ std::cout << "waiting for helpers to finish..." << std::endl;
+ helper1.join();
+ helper2.join();
+
+ // Print out the vector
+ std::cout << "v = { ";
+ for (int n : v)
+ std::cout << n << ", ";
+ std::cout << "}; \n";
+}
\ No newline at end of file
--- /dev/null
+# This test raises a property violation, thus the return code of 1
+! expect return 1
+
+# We ignore the LD_PRELOAD lines from the expected output because they contain the build path
+! ignore .*LD_PRELOAD.*
+
+$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/stdobject
+> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
+> [0.000000] [sthread/INFO] Starting the simulation.
+> starting two helpers...
+> waiting for helpers to finish...
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [sthread/INFO] thread 1 takes &v
+> [0.000000] [sthread/INFO] thread 1 releases &v
+> [0.000000] [sthread/INFO] thread 2 takes &v
+> [0.000000] [sthread/INFO] thread 2 releases &v
+> v = { 1, 2, 3, 5, 8, 13, 21, 21, };
+> [0.000000] [sthread/INFO] thread 1 takes &v
+> [0.000000] [sthread/INFO] thread 2 takes &v
+> [0.000000] ../../src/sthread/ObjectAccess.cpp:87: [sthread/CRITICAL] Unprotected concurent access to &v: thread 1 at ../../examples/sthread/stdobject/stdobject.cpp:20 vs. thread 2 at ../../examples/sthread/stdobject/stdobject.cpp:20.
+> [0.000000] [mc_ModelChecker/INFO] **************************
+> [0.000000] [mc_ModelChecker/INFO] *** PROPERTY NOT VALID ***
+> [0.000000] [mc_ModelChecker/INFO] **************************
+> [0.000000] [mc_ModelChecker/INFO] Counter-example execution trace:
+> [0.000000] [mc_ModelChecker/INFO] 2: BeginObjectAccess(&v @ ../../examples/sthread/stdobject/stdobject.cpp:20)
+> [0.000000] [mc_ModelChecker/INFO] 3: BeginObjectAccess(&v @ ../../examples/sthread/stdobject/stdobject.cpp:20)
+> [0.000000] [mc_ModelChecker/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 7 unique states visited; 1 backtracks (9 transition replays, 1 states visited overall)
#include "src/mc/transition/TransitionActorJoin.hpp"
#include "src/mc/transition/TransitionAny.hpp"
#include "src/mc/transition/TransitionComm.hpp"
+#include "src/mc/transition/TransitionObjectAccess.hpp"
#include "src/mc/transition/TransitionRandom.hpp"
#include "src/mc/transition/TransitionSynchro.hpp"
#endif
case Transition::Type::ACTOR_JOIN:
return new ActorJoinTransition(issuer, times_considered, stream);
+ case Transition::Type::OBJECT_ACCESS:
+ return new ObjectAccessTransition(issuer, times_considered, stream);
+
case Transition::Type::UNKNOWN:
return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
--- /dev/null
+/* Copyright (c) 2015-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/transition/TransitionObjectAccess.hpp"
+#include "xbt/asserts.h"
+#include "xbt/log.h"
+#include <xbt/string.hpp>
+
+namespace simgrid::mc {
+
+ObjectAccessTransition::ObjectAccessTransition(aid_t issuer, int times_considered, std::stringstream& stream)
+ : Transition(Type::OBJECT_ACCESS, issuer, times_considered)
+{
+ short s;
+ xbt_assert(stream >> s >> objaddr_ >> objname_ >> file_ >> line_);
+ type_ = static_cast<simgrid::mc::ObjectAccessType>(s);
+}
+std::string ObjectAccessTransition::to_string(bool verbose) const
+{
+ if (type_ == ObjectAccessType::ENTER)
+ return xbt::string_printf("BeginObjectAccess(%s @ %s:%d)", objname_.c_str(), file_.c_str(), line_);
+ if (type_ == ObjectAccessType::EXIT)
+ return xbt::string_printf("EndObjectAccess(%s @ %s:%d)", objname_.c_str(), file_.c_str(), line_);
+ return xbt::string_printf("ObjectAccess(%s @ %s:%d)", objname_.c_str(), file_.c_str(), line_);
+}
+bool ObjectAccessTransition::depends(const Transition* o) const
+{
+ if (const auto* other = dynamic_cast<const ObjectAccessTransition*>(o))
+ return objaddr_ == other->objaddr_; // dependent only if it's an access to the same object
+ return false;
+}
+
+} // namespace simgrid::mc
--- /dev/null
+/* Copyright (c) 2015-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_TRANSITION_OBJECT_ACCESS_HPP
+#define SIMGRID_MC_TRANSITION_OBJECT_ACCESS_HPP
+
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid::mc {
+XBT_DECLARE_ENUM_CLASS(ObjectAccessType, ENTER, EXIT, BOTH);
+
+class ObjectAccessTransition : public Transition {
+ ObjectAccessType type_;
+ void* objaddr_;
+ std::string objname_;
+ std::string file_;
+ int line_;
+
+public:
+ ObjectAccessTransition(aid_t issuer, int times_considered, std::stringstream& stream);
+ std::string to_string(bool verbose) const override;
+ bool depends(const Transition* other) const override;
+};
+
+} // namespace simgrid::mc
+
+#endif
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2002-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. */
+
+/* Object access checker, for use in sthread. */
+
+#include "simgrid/modelchecker.h"
+#include "simgrid/s4u/Actor.hpp"
+#include "simgrid/simix.hpp"
+#include "src/kernel/actor/ActorImpl.hpp"
+#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/sthread/sthread.h"
+
+#include <unordered_map>
+
+XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(sthread);
+
+namespace simgrid::sthread {
+XBT_DECLARE_ENUM_CLASS(AccessType, ENTER, EXIT, BOTH);
+
+class ObjectAccessObserver final : public simgrid::kernel::actor::SimcallObserver {
+ AccessType type_;
+ void* objaddr_;
+ const char* objname_;
+ const char* file_;
+ int line_;
+
+public:
+ ObjectAccessObserver(simgrid::kernel::actor::ActorImpl* actor, AccessType type, void* objaddr, const char* objname,
+ const char* file, int line)
+ : SimcallObserver(actor), type_(type), objaddr_(objaddr), objname_(objname), file_(file), line_(line)
+ {
+ }
+ void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
+ bool is_visible() const override { return true; }
+};
+void ObjectAccessObserver::serialize(std::stringstream& stream) const
+{
+ stream << (short)mc::Transition::Type::OBJECT_ACCESS << ' ';
+ stream << (short)type_ << ' ' << objaddr_ << ' ' << objname_ << ' ' << file_ << ' ' << line_;
+}
+std::string ObjectAccessObserver::to_string() const
+{
+ return std::string("AccessObject(") + objname_ + ")";
+}
+}; // namespace simgrid::sthread
+
+struct ObjectOwner {
+ simgrid::kernel::actor::ActorImpl* owner = nullptr;
+ const char* file = nullptr;
+ int line = -1;
+ ObjectOwner(simgrid::kernel::actor::ActorImpl* o) : owner(o) {}
+};
+
+std::unordered_map<void*, ObjectOwner*> owners;
+static void clean_owners()
+{
+ for (auto it = owners.begin(); it != owners.end();) {
+ delete it->second;
+ it = owners.erase(it);
+ }
+}
+static ObjectOwner* get_owner(void* object)
+{
+ if (owners.empty())
+ std::atexit(clean_owners);
+ auto it = owners.find(object);
+ if (it != owners.end())
+ return it->second;
+ auto* o = new ObjectOwner(nullptr);
+ owners.emplace(object, o);
+ return o;
+}
+
+int sthread_access_begin(void* objaddr, const char* objname, const char* file, int line)
+{
+ sthread_disable();
+ auto* self = simgrid::kernel::actor::ActorImpl::self();
+ simgrid::sthread::ObjectAccessObserver observer(self, simgrid::sthread::AccessType::ENTER, objaddr, objname, file,
+ line);
+ bool success = simgrid::kernel::actor::simcall_answered(
+ [self, objaddr, objname, file, line]() -> bool {
+ XBT_INFO("%s takes %s", self->get_cname(), objname);
+ auto* ownership = get_owner(objaddr);
+ if (ownership->owner != nullptr) {
+ XBT_CRITICAL("Unprotected concurent access to %s: %s at %s:%d vs. %s at %s:%d.", objname,
+ ownership->owner->get_cname(), ownership->file, ownership->line, self->get_cname(), file, line);
+ return false;
+ }
+ ownership->owner = self;
+ ownership->file = file;
+ ownership->line = line;
+ return true;
+ },
+ &observer);
+ MC_assert(success);
+ xbt_assert(success, "Problem detected, bailing out");
+ sthread_enable();
+ return true;
+}
+void sthread_access_end(void* objaddr, const char* objname, const char* file, int line)
+{
+ sthread_disable();
+ auto* self = simgrid::kernel::actor::ActorImpl::self();
+ simgrid::sthread::ObjectAccessObserver observer(self, simgrid::sthread::AccessType::EXIT, objaddr, objname, file,
+ line);
+ simgrid::kernel::actor::simcall_answered(
+ [self, objaddr, objname, file, line]() -> void {
+ XBT_INFO("%s releases %s", self->get_cname(), objname);
+ auto* ownership = get_owner(objaddr);
+ xbt_assert(ownership->owner == self, "safety check failed: I'm not owner of the object I'm releasing.");
+ ownership->owner = nullptr;
+ },
+ &observer);
+ sthread_enable();
+}
int sthread_gettimeofday(struct timeval* tv);
void sthread_sleep(double seconds);
+int sthread_access_begin(void* objaddr, const char* objname, const char* file, int line);
+void sthread_access_end(void* objaddr, const char* objname, const char* file, int line);
+
#if defined(__cplusplus)
}
#endif
src/sthread/sthread_impl.cpp
src/sthread/sthread.c
src/sthread/sthread.h
+ src/sthread/ObjectAccess.cpp
)
set(XBT_SRC
src/mc/transition/TransitionAny.hpp
src/mc/transition/TransitionComm.cpp
src/mc/transition/TransitionComm.hpp
+ src/mc/transition/TransitionObjectAccess.cpp
+ src/mc/transition/TransitionObjectAccess.hpp
src/mc/transition/TransitionRandom.cpp
src/mc/transition/TransitionRandom.hpp
src/mc/transition/TransitionSynchro.cpp
