$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 1 --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] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] 0 actors remain, but none of them need to be interleaved (depth 4).
> [Checker] Execution came to an end at 1;1 (state: 3, depth: 3)
> [Checker] Backtracking from 1;1
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --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] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Executed 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=3)
> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Backtracking from 1;2;1;2
> [Checker] Sleep set actually containing:
> [Checker] <1,BARRIER_ASYNC_LOCK(barrier: 0)>
-> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] 2 actors remain, but none of them need to be interleaved (depth 3).
> [Checker] Backtracking from 2
> [Checker] DFS exploration ended. 6 unique states visited; 1 backtracks (0 transition replays, 7 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${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] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Executed 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #2 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Executed 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] Executed 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 BARRIER_WAIT(barrier: 0) (state=4)
> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
+> [Checker] Executed 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #2 BARRIER_WAIT(barrier: 0) (state=5)
> [Checker] #3 BARRIER_WAIT(barrier: 0) (state=6)
> [Checker] Backtracking from 1;2;3;1;2;3
> [Checker] Sleep set actually containing:
> [Checker] <2,BARRIER_ASYNC_LOCK(barrier: 0)>
-> [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Executed 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
> [Checker] #3 BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
> [App ] Configuration change: Set 'actors' to '1'
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Executed 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Executed 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
+> [Checker] Executed 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
+> [Checker] Executed 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
+> [Checker] Executed 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=6)
> [Checker] Backtracking from 1;1;1;2;2;2
> [Checker] Sleep set actually containing:
> [Checker] <1,MUTEX_UNLOCK(mutex: 0, owner: -1)>
-> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Executed 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
> [Checker] Backtracking from 1;1;2
> [Checker] Sleep set actually containing:
> [Checker] <1,MUTEX_ASYNC_LOCK(mutex: 0, owner: 1)>
-> [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Executed 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 9, 0 interleaves)
+> [Checker] Executed 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 9, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #2 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 10, 0 interleaves)
+> [Checker] Executed 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 10, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
> [Checker] #2 MUTEX_WAIT(mutex: 0, owner: 2) (state=10)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 11, 0 interleaves)
+> [Checker] Executed 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 11, 0 interleaves)
> [Checker] INDEPENDENT Transitions:
> [Checker] #1 MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 12, 0 interleaves)
+> [Checker] Executed 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 12, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
> [Checker] #1 MUTEX_WAIT(mutex: 0, owner: 1) (state=12)
> [Checker] Sleep set actually containing:
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 13, 0 interleaves)
+> [Checker] Executed 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 13, 0 interleaves)
> [Checker] Dependent Transitions:
> [Checker] #2 MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
> [Checker] #1 MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -C 1 -P 1
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 39 unique states visited; 0 backtracks (0 transition replays, 39 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 617 unique states visited; 29 backtracks (524 transition replays, 1170 states visited overall)
}
#define STHREAD_ACCESS(obj) \
- for (bool first = sthread_access_begin(static_cast<void*>(obj), #obj, __FILE__, __LINE__, __FUNCTION__) || true; \
- first; sthread_access_end(static_cast<void*>(obj), #obj, __FILE__, __LINE__, __FUNCTION__), first = false)
+ for (bool first = sthread_access_begin(static_cast<void*>(obj), #obj, __FILE__, __LINE__, __func__) || true; first; \
+ sthread_access_end(static_cast<void*>(obj), #obj, __FILE__, __LINE__, __func__), first = false)
static void thread_code()
{
std::vector<s4u::Link*> CommImpl::get_traversed_links() const
{
- xbt_assert(get_state() != State::WAITING, "You cannot use %s() if your communication is not ready (%s)", __FUNCTION__,
+ xbt_assert(get_state() != State::WAITING, "You cannot use %s() if your communication is not ready (%s)", __func__,
get_state_str());
std::vector<s4u::Link*> vlinks;
XBT_ATTRIB_UNUSED double res = 0;
std::deque<SemAcquisitionImplPtr> ongoing_acquisitions_;
static unsigned next_id_;
- unsigned id_ = next_id_++;
+ const unsigned id_ = next_id_++;
friend SemAcquisitionImpl;
friend actor::SemaphoreObserver;
/** (in kernel mode) unpack the simcall and activate the handler */
void ActorImpl::simcall_handle(int times_considered)
{
- XBT_DEBUG("Handling simcall %p: %s(%ld) %s", &simcall_, simcall_.issuer_->get_cname(), simcall_.issuer_->get_pid(),
- (simcall_.observer_ != nullptr ? simcall_.observer_->to_string().c_str() : simcall_.get_cname()));
+ XBT_DEBUG("Handling simcall %p: %s(%ld) %s (times_considered:%d)", &simcall_, simcall_.issuer_->get_cname(),
+ simcall_.issuer_->get_pid(),
+ (simcall_.observer_ != nullptr ? simcall_.observer_->to_string().c_str() : simcall_.get_cname()),
+ times_considered);
if (simcall_.observer_ != nullptr)
simcall_.observer_->prepare(times_considered);
if (wannadie())
std::string MutexObserver::to_string() const
{
return std::string(mc::Transition::to_c_str(type_)) + "(mutex_id:" + std::to_string(get_mutex()->get_id()) +
- " owner:" + std::to_string(get_mutex()->get_owner()->get_pid()) + ")";
+ " owner:" +
+ (get_mutex()->get_owner() == nullptr ? "none" : std::to_string(get_mutex()->get_owner()->get_pid())) + ")";
}
bool MutexObserver::is_enabled()
void SemaphoreObserver::serialize(std::stringstream& stream) const
{
- stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */;
+ stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */ << ' '
+ << get_sem()->get_capacity();
}
std::string SemaphoreObserver::to_string() const
{
}
void SemaphoreAcquisitionObserver::serialize(std::stringstream& stream) const
{
- stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_;
+ stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_ << ' '
+ << acquisition_->semaphore_->get_capacity();
}
std::string SemaphoreAcquisitionObserver::to_string() const
{
// Find an enabled transition to pick
for (const auto& [_, actor] : get_actors_list()) {
if (actor.is_enabled()) {
- // For each variant of the transition, we want
- // to insert the action into the tree. This ensures
- // that all variants are searched
+ // For each variant of the transition that is enabled, we want to insert the action into the tree.
+ // This ensures that all variants are searched
for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
}
~BasicStrategy() override = default;
std::pair<aid_t, int> best_transition(bool must_be_todo) 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() && must_be_todo) || not actor.is_enabled() || actor.is_done()) {
+ 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() && must_be_todo) || not actor.is_enabled() || actor.is_done())
continue;
- }
return std::make_pair(aid, depth_);
}
}
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) {
- // NOTE: The outgoing transition for the top-most
- // state of the stack refers to that which was taken
- // as part of the last trace explored by the algorithm.
- // Thus, only the sequence of transitions leading up to,
- // but not including, the last state must be included
- // when reconstructing the Exploration for SDPOR.
+ // NOTE: The outgoing transition for the top-most state of the stack refers to that which was taken
+ // as part of the last trace explored by the algorithm. Thus, only the sequence of transitions leading up to,
+ // but not including, the last state must be included when reconstructing the Exploration for SDPOR.
for (auto iter = std::next(stack_.begin()); iter != stack_.end(); ++iter) {
execution_seq_.push_transition((*iter)->get_transition_in());
}
}
if (reduction_mode_ == ReductionMode::odpor) {
- // In the case of ODPOR, the wakeup tree for this
- // state may be empty if we're exploring new territory
- // (rather than following the partial execution of a
- // wakeup tree). This corresponds to lines 9 to 13 of
+ // In the case of ODPOR, the wakeup tree for this state may be empty if we're exploring new territory
+ // (rather than following the partial execution of a wakeup tree). This corresponds to lines 9 to 13 of
// the ODPOR pseudocode
//
- // INVARIANT: The execution sequence should be consistent
- // with the state when seeding the tree. If the sequence
- // gets out of sync with the state, selection will not
- // work as we intend
+ // INVARIANT: The execution sequence should be consistent with the state when seeding the tree. If the sequence
+ // gets out of sync with the state, selection will not work as we intend
state->seed_wakeup_tree_if_needed(execution_seq_);
}
XBT_VERB(" <%ld,%s>", aid, transition->to_string().c_str());
}
+ auto todo = state->get_actors_list().at(next).get_transition();
+ XBT_DEBUG("wanna execute %ld: %.60s", next, todo->to_string().c_str());
+
/* Actually answer the request: let's execute the selected request (MCed does one step) */
auto executed_transition = state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition_out().get(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
- XBT_VERB("Execute %ld: %.150s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
+ XBT_VERB("Executed %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
state->get_transition_out()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
/* Create the new expanded state (copy the state of MCed into our MCer data) */
on_state_creation_signal(next_state.get(), get_remote_app());
if (reduction_mode_ == ReductionMode::odpor) {
- // With ODPOR, after taking a step forward, we must
- // assign a copy of that subtree to the next state.
+ // With ODPOR, after taking a step forward, we must assign a copy of that subtree to the next state.
//
- // NOTE: We only add actions to the sleep set AFTER
- // we've regenerated states. We must perform the search
- // fully down a single path before we consider adding
- // any elements to the sleep set according to the pseudocode
+ // NOTE: We only add actions to the sleep set AFTER we've regenerated states. We must perform the search
+ // fully down a single path before we consider adding any elements to the sleep set according to the pseudocode
next_state->sprout_tree_from_parent_state();
} else {
/* Sleep set procedure:
/**
* SDPOR Source Set Procedure:
*
- * Find "reversible races" in the current execution `E` with respect
- * to the latest action `p`. For each such race, determine one thread
- * not contained in the backtrack set at the "race point" `r` which
- * "represents" the trace formed by first executing everything after
- * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
+ * Find "reversible races" in the current execution `E` with respect to the latest action `p`. For each such race,
+ * determine one thread not contained in the backtrack set at the "race point" `r` which "represents" the trace
+ * formed by first executing everything after `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
* flip the race.
*
- * The intuition is that some subsequence of `v` may enable `p`, so
- * we want to be sure that search "in that direction"
+ * The intuition is that some subsequence of `v` may enable `p`, so we want to be sure that search "in that
+ * direction"
*/
execution_seq_.push_transition(std::move(executed_transition));
xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR execution "
State* prev_state = stack_[e_race].get();
const auto choices = execution_seq_.get_missing_source_set_actors_from(e_race, prev_state->get_backtrack_set());
if (not choices.empty()) {
- // NOTE: To incorporate the idea of attempting to select the "best"
- // backtrack point into SDPOR, instead of selecting the `first` initial,
- // we should instead compute all choices and decide which is best
+ // NOTE: To incorporate the idea of attempting to select the "best" backtrack point into SDPOR, instead of
+ // selecting the `first` initial, we should instead compute all choices and decide which is best
//
- // Here, we choose the actor with the lowest ID to ensure
- // we get deterministic results
+ // Here, we choose the actor with the lowest ID to ensure we get deterministic results
const auto q =
std::min_element(choices.begin(), choices.end(), [](const aid_t a1, const aid_t a2) { return a1 < a2; });
prev_state->consider_one(*q);
}
}
} else if (reduction_mode_ == ReductionMode::odpor) {
- // In the case of ODPOR, we simply observe the transition that was executed
- // until we've reached a maximal trace
+ // In the case of ODPOR, we simply observe the transition that was executed until we've reached a maximal trace
execution_seq_.push_transition(std::move(executed_transition));
}
/**
* ODPOR Race Detection Procedure:
*
- * For each reversible race in the current execution, we
- * note if there are any continuations `C` equivalent to that which
- * would reverse the race that have already either a) been searched by ODPOR or
- * b) been *noted* to be searched by the wakeup tree at the
- * appropriate reversal point, either as `C` directly or
- * an as equivalent to `C` ("eventually looks like C", viz. the `~_E`
- * relation)
+ * For each reversible race in the current execution, we note if there are any continuations `C` equivalent to that
+ * which would reverse the race that have already either a) been searched by ODPOR or b) been *noted* to be searched
+ * by the wakeup tree at the appropriate reversal point, either as `C` directly or an as equivalent to `C`
+ * ("eventually looks like C", viz. the `~_E` relation)
*/
for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
#include <functional>
#include <unordered_map>
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
const Transition* /*e2*/)
{
- // TODO: Get the semantics correct here
- // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori,
- // il doit même suffir de considérer le cas où leur capacity après execution est <=1
- // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir
- // wait avant le unlock.
- return false;
+ // Reversible with everynbody but unlock which creates a free token
+ const auto e1_transition = E.get_transition_for_handle(e1);
+ if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
+ static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1)
+ return false;
+ return true;
}
bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
{
kernel::actor::ActorImpl* actor = kernel::EngineImpl::get_instance()->get_actor_by_pid(message->aid_);
xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_);
+ xbt_assert(actor->simcall_.observer_ == nullptr || actor->simcall_.observer_->is_enabled(),
+ "Please, model-checker, don't execute disabled transitions.");
// The client may send some messages to the server while processing the transition
actor->simcall_handle(message->times_considered_);
std::string SemaphoreTransition::to_string(bool verbose) const
{
if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
- return xbt::string_printf("%s(semaphore: %" PRIxPTR ")", Transition::to_c_str(type_), sem_);
+ return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), capacity_, sem_);
if (type_ == Type::SEM_WAIT)
- return xbt::string_printf("%s(semaphore: %" PRIxPTR ", granted: %s)", Transition::to_c_str(type_), sem_,
- granted_ ? "yes" : "no");
+ return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), capacity_,
+ sem_, granted_ ? "yes" : "no");
THROW_IMPOSSIBLE;
}
SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
: Transition(type, issuer, times_considered)
{
- xbt_assert(stream >> sem_ >> granted_);
+ xbt_assert(stream >> sem_ >> granted_ >> capacity_);
}
bool SemaphoreTransition::depends(const Transition* o) const
{
};
class SemaphoreTransition : public Transition {
- uintptr_t sem_;
+ unsigned int sem_; // ID
bool granted_;
+ unsigned capacity_;
public:
std::string to_string(bool verbose) const override;
SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
bool depends(const Transition* other) const override;
+ int get_capacity() const { return capacity_; }
};
} // namespace simgrid::mc
CommPtr Comm::set_rate(double rate)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
rate_ = rate;
return this;
}
CommPtr Comm::set_mailbox(Mailbox* mailbox)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
mailbox_ = mailbox;
return this;
}
CommPtr Comm::set_src_data(void* buff)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
xbt_assert(dst_buff_ == nullptr, "Cannot set the src and dst buffers at the same time");
src_buff_ = buff;
return this;
CommPtr Comm::set_src_data_size(size_t size)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
src_buff_size_ = size;
return this;
}
CommPtr Comm::set_src_data(void* buff, size_t size)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
xbt_assert(dst_buff_ == nullptr, "Cannot set the src and dst buffers at the same time");
src_buff_ = buff;
CommPtr Comm::set_dst_data(void** buff)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
xbt_assert(src_buff_ == nullptr, "Cannot set the src and dst buffers at the same time");
dst_buff_ = buff;
return this;
CommPtr Comm::set_dst_data(void** buff, size_t size)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
xbt_assert(src_buff_ == nullptr, "Cannot set the src and dst buffers at the same time");
dst_buff_ = buff;
Comm* Comm::do_start()
{
xbt_assert(get_state() == State::INITED || get_state() == State::STARTING,
- "You cannot use %s() once your communication started (not implemented)", __FUNCTION__);
+ "You cannot use %s() once your communication started (not implemented)", __func__);
auto myself = kernel::actor::ActorImpl::self();
Comm* Comm::detach()
{
xbt_assert(state_ == State::INITED || state_ == State::STARTING,
- "You cannot use %s() once your communication is %s (not implemented)", __FUNCTION__, get_state_str());
+ "You cannot use %s() once your communication is %s (not implemented)", __func__, get_state_str());
xbt_assert(dst_buff_ == nullptr && dst_buff_size_ == 0, "You can only detach sends, not recvs");
detached_ = true;
start();
MessPtr Mess::set_dst_data(void** buff, size_t size)
{
xbt_assert(state_ == State::INITED, "You cannot use %s() once your communication started (not implemented)",
- __FUNCTION__);
+ __func__);
dst_buff_ = buff;
dst_buff_size_ = size;
Mess* Mess::do_start()
{
xbt_assert(get_state() == State::INITED || get_state() == State::STARTING,
- "You cannot use %s() once your message exchange has started (not implemented)", __FUNCTION__);
+ "You cannot use %s() once your message exchange has started (not implemented)", __func__);
auto myself = kernel::actor::ActorImpl::self();
if (myself == sender_) {
if (mutex->mutex == nullptr)
sthread_mutex_init(mutex, nullptr);
- XBT_DEBUG("%s(%p)", __FUNCTION__, mutex);
+ XBT_DEBUG("%s(%p)", __func__, mutex);
static_cast<sg4::Mutex*>(mutex->mutex)->lock();
return 0;
}
if (mutex->mutex == nullptr)
sthread_mutex_init(mutex, nullptr);
- XBT_DEBUG("%s(%p)", __FUNCTION__, mutex);
+ XBT_DEBUG("%s(%p)", __func__, mutex);
if (static_cast<sg4::Mutex*>(mutex->mutex)->try_lock())
return 0;
return EBUSY;
if (mutex->mutex == nullptr)
sthread_mutex_init(mutex, nullptr);
- XBT_DEBUG("%s(%p)", __FUNCTION__, mutex);
+ XBT_DEBUG("%s(%p)", __func__, mutex);
static_cast<sg4::Mutex*>(mutex->mutex)->unlock();
return 0;
}
if (mutex->mutex == nullptr)
sthread_mutex_init(mutex, nullptr);
- XBT_DEBUG("%s(%p)", __FUNCTION__, mutex);
+ XBT_DEBUG("%s(%p)", __func__, mutex);
intrusive_ptr_release(static_cast<sg4::Mutex*>(mutex->mutex));
return 0;
}
/usr/bin/python3-coverage xml -i -o ./python_coverage.xml
#convert all gcov reports to xml cobertura reports
- gcovr -r "$WORKSPACE" --xml-pretty -e "$WORKSPACE"/teshsuite -e MBI -e "$WORKSPACE"/examples/smpi/NAS -e "$WORKSPACE"/examples/smpi/mc -u -o xml_coverage.xml --gcov-ignore-parse-errors
+ gcovr -r "$WORKSPACE" --xml-pretty -e "$WORKSPACE"/teshsuite -e MBI -e "$WORKSPACE"/examples/smpi/NAS -e "$WORKSPACE"/examples/smpi/mc -u -o xml_coverage.xml --gcov-ignore-parse-errors all --gcov-ignore-errors all
cd "$WORKSPACE"
xsltproc "$WORKSPACE"/tools/jenkins/ctest2junit.xsl build/Testing/"$( head -n 1 < build/Testing/TAG )"/Test.xml > CTestResults_memcheck.xml
