namespace simgrid {
namespace mc {
-static
int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
{
simgrid::mc::Process* process = &mc_model_checker->process();
return errors > 0 || hash_result;
}
-int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
-{
- simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
- simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
- int num1 = state1->num;
- int num2 = state2->num;
- return snapshot_compare(num1, s1, num2, s2);
-}
-
int snapshot_compare(mc_state_t state1, mc_state_t state2)
{
simgrid::mc::Snapshot* s1 = state1->system_state;
MC_print_statistics(mc_stats);
}
-namespace simgrid {
-namespace mc {
-
-void show_stack_liveness(xbt_fifo_t stack)
-{
- int value;
- simgrid::mc::Pair* pair;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(pair->graph_state, &value);
- if (req && req->call != SIMCALL_NONE) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void dump_stack_liveness(xbt_fifo_t stack)
-{
- simgrid::mc::Pair* pair;
- while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
- delete pair;
-}
-
-}
-}
-
void MC_print_statistics(mc_stats_t stats)
{
if(_sg_mc_comms_determinism) {
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
#include "src/mc/Client.hpp"
+#include "src/mc/mc_private.h"
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
namespace simgrid {
namespace mc {
+static xbt_dynar_t visited_pairs;
+
Pair::Pair() : num(++mc_stats->expanded_pairs),
visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
{}
MC_state_delete(this->graph_state, 1);
}
+static void show_stack_liveness(xbt_fifo_t stack)
+{
+ int value;
+ simgrid::mc::Pair* pair;
+ xbt_fifo_item_t item;
+ smx_simcall_t req;
+ char *req_str = nullptr;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ item; item = xbt_fifo_get_prev_item(item)) {
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+ req = MC_state_get_executed_request(pair->graph_state, &value);
+ if (req && req->call != SIMCALL_NONE) {
+ req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+static void dump_stack_liveness(xbt_fifo_t stack)
+{
+ simgrid::mc::Pair* pair;
+ while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
+ delete pair;
+}
+
static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
{
unsigned int cursor = 0;
return std::move(values);
}
+static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
+ simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
+}
+
static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
{
simgrid::mc::VisitedPair* new_pair = new VisitedPair(
XBT_DEBUG("**** End Replay ****");
}
+/**
+ * \brief Checks whether a given pair has already been visited by the algorithm.
+ */
+static
+int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+{
+ if (_sg_mc_visited == 0)
+ return -1;
+
+ simgrid::mc::VisitedPair* new_visited_pair = nullptr;
+ if (visited_pair == nullptr)
+ new_visited_pair = new simgrid::mc::VisitedPair(
+ pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+ pair->graph_state);
+ else
+ new_visited_pair = visited_pair;
+
+ if (xbt_dynar_is_empty(visited_pairs)) {
+ xbt_dynar_push(visited_pairs, &new_visited_pair);
+ return -1;
+ }
+
+ int min = -1, max = -1, index;
+ //int res;
+ simgrid::mc::VisitedPair* pair_test;
+ int cursor;
+
+ index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
+
+ if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
+ cursor = min;
+ while (cursor <= max) {
+ pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_visited_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+ if (pair_test->other_num == -1)
+ new_visited_pair->other_num = pair_test->num;
+ else
+ new_visited_pair->other_num = pair_test->other_num;
+ if (dot_output == nullptr)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+ xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair
+ || pair_test->acceptance_removed == 1)
+ delete pair_test;
+ return new_visited_pair->other_num;
+ }
+ }
+ }
+ cursor++;
+ }
+ xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
+ } else {
+ pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
+ if (pair_test->nb_processes < new_visited_pair->nb_processes)
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+ else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+ else
+ xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
+ }
+
+ if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
+ int min2 = mc_stats->expanded_pairs;
+ unsigned int cursor2 = 0;
+ unsigned int index2 = 0;
+ xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
+ if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+ && pair_test->num < min2) {
+ index2 = cursor2;
+ min2 = pair_test->num;
+ }
+ }
+ xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+ delete pair_test;
+ }
+ return -1;
+}
+
static int MC_modelcheck_liveness_main(void)
{
simgrid::mc::Pair* current_pair = nullptr;
};
int modelcheck_liveness(void);
-XBT_PRIVATE void show_stack_liveness(xbt_fifo_t stack);
-XBT_PRIVATE void dump_stack_liveness(xbt_fifo_t stack);
-
-XBT_PRIVATE extern xbt_dynar_t visited_pairs;
-XBT_PRIVATE int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
-
-XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);
}
}
XBT_PRIVATE void MC_report_assertion_error(void);
XBT_PRIVATE void MC_report_crash(int status);
+SG_END_DECL()
+
#ifdef __cplusplus
namespace simgrid {
XBT_PRIVATE void find_object_address(
std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
+XBT_PRIVATE
+int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2);
+
}
}
#endif
-SG_END_DECL()
-
#endif
namespace simgrid {
namespace mc {
-xbt_dynar_t visited_pairs;
std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
return nullptr;
}
-/**
- * \brief Checks whether a given pair has already been visited by the algorithm.
- */
-int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
-
- if (_sg_mc_visited == 0)
- return -1;
-
- simgrid::mc::VisitedPair* new_visited_pair = nullptr;
- if (visited_pair == nullptr)
- new_visited_pair = new simgrid::mc::VisitedPair(
- pair->num, pair->automaton_state, pair->atomic_propositions.get(),
- pair->graph_state);
- else
- new_visited_pair = visited_pair;
-
- if (xbt_dynar_is_empty(visited_pairs)) {
- xbt_dynar_push(visited_pairs, &new_visited_pair);
- return -1;
- }
-
- int min = -1, max = -1, index;
- //int res;
- simgrid::mc::VisitedPair* pair_test;
- int cursor;
-
- index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
-
- if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
- cursor = min;
- while (cursor <= max) {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value(
- pair_test->atomic_propositions.get(),
- new_visited_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_visited_pair) == 0) {
- if (pair_test->other_num == -1)
- new_visited_pair->other_num = pair_test->num;
- else
- new_visited_pair->other_num = pair_test->other_num;
- if (dot_output == nullptr)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
- else
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
- xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
- xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair
- || pair_test->acceptance_removed == 1)
- delete pair_test;
- return new_visited_pair->other_num;
- }
- }
- }
- cursor++;
- }
- xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
- } else {
- pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
- if (pair_test->nb_processes < new_visited_pair->nb_processes)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
- else
- xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
- }
-
- if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
- int min2 = mc_stats->expanded_pairs;
- unsigned int cursor2 = 0;
- unsigned int index2 = 0;
- xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
- && pair_test->num < min2) {
- index2 = cursor2;
- min2 = pair_test->num;
- }
- }
- xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
- pair_test->visited_removed = 1;
- if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
- delete pair_test;
- }
- return -1;
-}
-
}
}
\ No newline at end of file