From: Martin Quinson Date: Mon, 6 Mar 2023 08:05:55 +0000 (+0100) Subject: sthread: Add a way to verify accesses to non-reentrant data structures X-Git-Tag: v3.34~365 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fba44e13f2b2b7fb3f99030e5a59cd1eb721d558 sthread: Add a way to verify accesses to non-reentrant data structures The example is very fragile so far, segfaulting 2 times over 3 in general, so don't activate it. --- diff --git a/ChangeLog b/ChangeLog index 5e238de1f7..41bc62f20a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -49,6 +49,8 @@ Models: 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. diff --git a/MANIFEST.in b/MANIFEST.in index c4b443b5bf..f1fe2118e3 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -603,6 +603,8 @@ include examples/sthread/pthread-mutex-simple.tesh 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 @@ -2232,6 +2234,8 @@ include src/mc/transition/TransitionAny.cpp 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 @@ -2458,6 +2462,7 @@ include src/smpi/smpif90.in 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 diff --git a/examples/sthread/CMakeLists.txt b/examples/sthread/CMakeLists.txt index 2f6f99f85c..27b78a2317 100644 --- a/examples/sthread/CMakeLists.txt +++ b/examples/sthread/CMakeLists.txt @@ -12,7 +12,7 @@ foreach(x 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) @@ -51,6 +51,27 @@ foreach(x 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 ############################################################################# diff --git a/examples/sthread/stdobject/stdobject.cpp b/examples/sthread/stdobject/stdobject.cpp new file mode 100644 index 0000000000..06e49c86a5 --- /dev/null +++ b/examples/sthread/stdobject/stdobject.cpp @@ -0,0 +1,38 @@ +#include +#include +#include + +// shared collection object +std::vector 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(obj), #obj, __FILE__, __LINE__) || true; first; \ + sthread_access_end(static_cast(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 diff --git a/examples/sthread/stdobject/stdobject.tesh b/examples/sthread/stdobject/stdobject.tesh new file mode 100644 index 0000000000..1ce83ab48d --- /dev/null +++ b/examples/sthread/stdobject/stdobject.tesh @@ -0,0 +1,28 @@ +# 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) diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index c6bf0b8ffc..2c20b73430 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -14,6 +14,7 @@ #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 @@ -96,6 +97,9 @@ Transition* deserialize_transition(aid_t issuer, int times_considered, std::stri 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); diff --git a/src/mc/transition/TransitionObjectAccess.cpp b/src/mc/transition/TransitionObjectAccess.cpp new file mode 100644 index 0000000000..144107dc75 --- /dev/null +++ b/src/mc/transition/TransitionObjectAccess.cpp @@ -0,0 +1,35 @@ +/* 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 + +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(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(o)) + return objaddr_ == other->objaddr_; // dependent only if it's an access to the same object + return false; +} + +} // namespace simgrid::mc diff --git a/src/mc/transition/TransitionObjectAccess.hpp b/src/mc/transition/TransitionObjectAccess.hpp new file mode 100644 index 0000000000..12314462e5 --- /dev/null +++ b/src/mc/transition/TransitionObjectAccess.hpp @@ -0,0 +1,29 @@ +/* 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 diff --git a/src/sthread/ObjectAccess.cpp b/src/sthread/ObjectAccess.cpp new file mode 100644 index 0000000000..93224388f0 --- /dev/null +++ b/src/sthread/ObjectAccess.cpp @@ -0,0 +1,118 @@ +/* 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 + +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 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(); +} diff --git a/src/sthread/sthread.h b/src/sthread/sthread.h index da9b453dce..65279685e6 100644 --- a/src/sthread/sthread.h +++ b/src/sthread/sthread.h @@ -53,6 +53,9 @@ int sthread_sem_timedwait(sthread_sem_t* sem, const struct timespec* abs_timeout 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 diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 8e7b1acb09..468e51f244 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -251,6 +251,7 @@ set(STHREAD_SRC src/sthread/sthread_impl.cpp src/sthread/sthread.c src/sthread/sthread.h + src/sthread/ObjectAccess.cpp ) set(XBT_SRC @@ -587,6 +588,8 @@ set(MC_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