#include <xbt/log.h>
#include <xbt/sysdep.h>
#include <xbt/mmalloc.h>
+#include <xbt/swag.h>
#include "src/internal_config.h"
client_ = std::unique_ptr<Client>(new simgrid::mc::Client(fd));
// Wait for the model-checker:
- if (ptrace(PTRACE_TRACEME, 0, nullptr, NULL) == -1 || raise(SIGSTOP) != 0)
+ if (ptrace(PTRACE_TRACEME, 0, nullptr, nullptr) == -1 || raise(SIGSTOP) != 0)
xbt_die("Could not wait for the model-checker");
client_->handleMessages();
/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
if(comm1->type != comm2->type)
return TYPE_DIFF;
if (comm1->rdv != comm2->rdv)
return NONE_DIFF;
}
-static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
+static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
char *type, *res;
if(comm->type == SIMIX_COMM_SEND)
return res;
}
-static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
+static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
{
s_smx_synchro_t comm;
mc_model_checker->process().read(&comm, remote(comm_addr));
}
}
-static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
+static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
- mc_list_comm_pattern_t list =
- xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
+ simgrid::mc::PatternCommunicationList* list =
+ xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
if(!backtracking){
- mc_comm_pattern_t initial_comm =
- xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
e_mc_comm_pattern_difference_t diff =
- compare_comm_pattern(initial_comm, comm);
+ compare_comm_pattern(list->list[list->index_comm].get(), comm);
if (diff != NONE_DIFF) {
if (comm->type == SIMIX_COMM_SEND){
}
}
}
-
- MC_comm_pattern_free(comm);
-
}
/********** Non Static functions ***********/
void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
- mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+ simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
- mc_comm_pattern_t pattern = new s_mc_comm_pattern_t();
+ std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
+ std::unique_ptr<simgrid::mc::PatternCommunication>(
+ new simgrid::mc::PatternCommunication());
pattern->index =
initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
if(mpi_request.detached){
if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
/* Store comm pattern */
- xbt_dynar_push(
- xbt_dynar_get_as(
- initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
- )->list,
- &pattern);
+ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
+ initial_communications_pattern, pattern->src_proc,
+ simgrid::mc::PatternCommunicationList*);
+ list->list.push_back(std::move(pattern));
} else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
+ deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
xbt_dynar_get_as(
- initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
+ initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
)->index_comm++;
}
return;
} else
xbt_die("Unexpected call_type %i", (int) call_type);
- xbt_dynar_push(
- xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
- &pattern);
-
- XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
+ XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
+ pattern.get(), issuer->pid);
+ xbt_dynar_t dynar =
+ xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ simgrid::mc::PatternCommunication* pattern2 = pattern.release();
+ xbt_dynar_push(dynar, &pattern2);
}
void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
- mc_comm_pattern_t current_comm_pattern;
+ simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
- mc_comm_pattern_t comm_pattern;
+ std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
int completed = 0;
/* Complete comm pattern */
if (current_comm_pattern->comm_addr == comm_addr) {
update_comm_pattern(current_comm_pattern, comm_addr);
completed = 1;
+ simgrid::mc::PatternCommunication* temp;
xbt_dynar_remove_at(
xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
- cursor, &comm_pattern);
+ cursor, &temp);
+ comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
break;
}
if(!completed)
xbt_die("Corresponding communication not found!");
- mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer, mc_list_comm_pattern_t);
+ simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
/* Store comm pattern */
- xbt_dynar_push(pattern->list, &comm_pattern);
+ pattern->list.push_back(std::move(comm_pattern));
else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(issuer, comm_pattern, backtracking);
+ deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
pattern->index_comm++;
}
}
const int maxpid = MC_smx_get_maxpid();
// Create initial_communications_pattern elements:
- initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
+ initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
for (i=0; i < maxpid; i++){
- mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
- process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
- process_list_pattern->index_comm = 0;
+ simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
}
// Create incomplete_communications_pattern elements:
incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
for (i=0; i < maxpid; i++){
- xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr);
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
XBT_INFO("Check communication determinism");
mc_model_checker->wait_for_requests();
- if (mc_mode == MC_MODE_CLIENT)
- // This will move somehwere else:
- simgrid::mc::Client::get()->handleMessages();
-
this->prepare();
initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
#include <simgrid_config.h>
#include <xbt/base.h>
-#include <xbt/dynar.h>
#include <xbt/automaton.h>
#include <xbt/memory.hpp>
#include "src/mc/mc_state.h"
#include <cassert>
#include <cstdio>
-#include <list>
+#include <memory>
+#include <string>
+#include <vector>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
-#include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_safety.h"
#include <vector>
#include <xbt/mmalloc.h>
+#include <xbt/dynar.h>
#include "src/mc/mc_forward.hpp"
#include "src/mc/Process.hpp"
#include <xbt/log.h>
#include <xbt/sysdep.h>
+#include <xbt/automaton.h>
#include <simgrid/modelchecker.h>
#include "src/mc/mc_record.h"
#include <xbt/sysdep.h>
#include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
"Logging specific to MC communication patterns");
-extern "C" {
-
-mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm)
-{
- mc_comm_pattern_t res = new s_mc_comm_pattern_t();
- res->index = comm->index;
- res->type = comm->type;
- res->comm_addr = comm->comm_addr;
- res->rdv = comm->rdv;
- res->data = comm->data;
- res->dst_proc = comm->dst_proc;
- res->dst_host = comm->dst_host;
- return res;
-}
-
-xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t patterns)
-{
- xbt_dynar_t res = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
-
- mc_comm_pattern_t comm;
- unsigned int cursor;
- xbt_dynar_foreach(patterns, cursor, comm) {
- mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
- xbt_dynar_push(res, ©_comm);
- }
-
- return res;
-}
-
-static void MC_patterns_copy(xbt_dynar_t dest, xbt_dynar_t source)
+static void MC_patterns_copy(xbt_dynar_t dest,
+ std::vector<simgrid::mc::PatternCommunication> const& source)
{
xbt_dynar_reset(dest);
-
- unsigned int cursor;
- mc_comm_pattern_t comm;
- xbt_dynar_foreach(source, cursor, comm) {
- mc_comm_pattern_t copy_comm = MC_comm_pattern_dup(comm);
+ for (simgrid::mc::PatternCommunication const& comm : source) {
+ simgrid::mc::PatternCommunication* copy_comm = new simgrid::mc::PatternCommunication(comm.dup());
xbt_dynar_push(dest, ©_comm);
}
}
void MC_restore_communications_pattern(simgrid::mc::State* state)
{
- mc_list_comm_pattern_t list_process_comm;
+ simgrid::mc::PatternCommunicationList* list_process_comm;
unsigned int cursor;
xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
for (unsigned i = 0; i < MC_smx_get_maxpid(); i++)
MC_patterns_copy(
xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
- xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t)
+ state->incomplete_comm_pattern[i]
);
}
void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state)
{
- state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
-
+ state->incomplete_comm_pattern.clear();
for (unsigned i=0; i < MC_smx_get_maxpid(); i++) {
- xbt_dynar_t comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
- xbt_dynar_t copy = MC_comm_patterns_dup(comms);
- xbt_dynar_insert_at(state->incomplete_comm_pattern, i, ©);
+ xbt_dynar_t patterns = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+ std::vector<simgrid::mc::PatternCommunication> res;
+ simgrid::mc::PatternCommunication* comm;
+ unsigned int cursor;
+ xbt_dynar_foreach(patterns, cursor, comm)
+ res.push_back(comm->dup());
+ state->incomplete_comm_pattern.push_back(std::move(res));
}
}
void MC_state_copy_index_communications_pattern(simgrid::mc::State* state)
{
state->communicationIndices.clear();
- mc_list_comm_pattern_t list_process_comm;
+ simgrid::mc::PatternCommunicationList* list_process_comm;
unsigned int cursor;
xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
state->communicationIndices.push_back(list_process_comm->index_comm);
}
}
-
-void MC_comm_pattern_free(mc_comm_pattern_t p)
-{
- delete p;
- p = nullptr;
-}
-
-static void MC_list_comm_pattern_free(mc_list_comm_pattern_t l)
-{
- xbt_dynar_free(&(l->list));
- xbt_free(l);
- l = nullptr;
-}
-
-void MC_comm_pattern_free_voidp(void *p)
-{
- MC_comm_pattern_free((mc_comm_pattern_t) * (void **) p);
-}
-
-void MC_list_comm_pattern_free_voidp(void *p)
-{
- MC_list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
-}
-
-}
#include "src/mc/mc_state.h"
-SG_BEGIN_DECL()
-
-typedef struct s_mc_comm_pattern{
- int num = 0;
- smx_synchro_t comm_addr;
- e_smx_comm_type_t type = SIMIX_COMM_SEND;
- unsigned long src_proc = 0;
- unsigned long dst_proc = 0;
- const char *src_host = nullptr;
- const char *dst_host = nullptr;
- std::string rdv;
- std::vector<char> data;
- int tag = 0;
- int index = 0;
-
- s_mc_comm_pattern()
- {
- std::memset(&comm_addr, 0, sizeof(comm_addr));
- }
+namespace simgrid {
+namespace mc {
- // No copy:
- s_mc_comm_pattern(s_mc_comm_pattern const&) = delete;
- s_mc_comm_pattern& operator=(s_mc_comm_pattern const&) = delete;
+struct PatternCommunicationList {
+ unsigned int index_comm = 0;
+ std::vector<std::unique_ptr<simgrid::mc::PatternCommunication>> list;
+};
-} s_mc_comm_pattern_t, *mc_comm_pattern_t;
+}
+}
-typedef struct s_mc_list_comm_pattern{
- unsigned int index_comm;
- xbt_dynar_t list;
-}s_mc_list_comm_pattern_t, *mc_list_comm_pattern_t;
+SG_BEGIN_DECL()
/**
* Type: `xbt_dynar_t<mc_list_comm_pattenr_t>`
extern XBT_PRIVATE xbt_dynar_t initial_communications_pattern;
/**
- * Type: `xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>>`
+ * Type: `xbt_dynar_t<xbt_dynar_t<simgrid::mc::PatternCommunication*>>`
*/
extern XBT_PRIVATE xbt_dynar_t incomplete_communications_pattern;
XBT_PRIVATE void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking);
-XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p);
-XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state);
-XBT_PRIVATE mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
-XBT_PRIVATE xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
-
XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state);
XBT_PRIVATE void MC_state_copy_index_communications_pattern(simgrid::mc::State* state);
-XBT_PRIVATE void MC_comm_pattern_free(mc_comm_pattern_t p);
-
SG_END_DECL()
#endif
if (type->subtype && type->subtype->type == DW_TAG_subroutine_type)
return (addr_pointed1 != addr_pointed2);
- if (addr_pointed1 == nullptr && addr_pointed2 == NULL)
+ if (addr_pointed1 == nullptr && addr_pointed2 == nullptr)
return 0;
- if (addr_pointed1 == nullptr || addr_pointed2 == NULL)
+ if (addr_pointed1 == nullptr || addr_pointed2 == nullptr)
return 1;
if (!state.compared_pointers.insert(
std::make_pair(addr_pointed1, addr_pointed2)).second)
#include "src/mc/mc_dwarf.hpp"
#include "src/mc/Type.hpp"
+#include <xbt/dynar.h>
+
using simgrid::mc::remote;
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
res_compare =
compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
- nullptr, NULL, 0);
+ nullptr, nullptr, 0);
if (res_compare != 1) {
for (k = 1; k < heapinfo2->busy_block.size; k++)
res_compare =
compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
- nullptr, NULL, 0);
+ nullptr, nullptr, 0);
if (res_compare != 1) {
for (k = 1; k < heapinfo2b->busy_block.size; k++)
res_compare =
compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot1, snapshot2,
- nullptr, NULL, 0);
+ nullptr, nullptr, 0);
if (res_compare != 1)
equal = 1;
res_compare =
compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot2, snapshot2,
- nullptr, NULL, 0);
+ nullptr, nullptr, 0);
if (res_compare != 1) {
equal = 1;
int type_size = -1;
int offset1 = 0, offset2 = 0;
int new_size1 = -1, new_size2 = -1;
- simgrid::mc::Type *new_type1 = nullptr, *new_type2 = NULL;
+ simgrid::mc::Type *new_type1 = nullptr, *new_type2 = nullptr;
int match_pairs = 0;
return -1;
}
- if (new_type1 != nullptr && new_type2 != NULL && new_type1 != new_type2) {
+ if (new_type1 != nullptr && new_type2 != nullptr && new_type1 != new_type2) {
type = new_type1;
while (type->byte_size == 0 && type->subtype != nullptr)
Dwarf_Off next_offset = 0;
size_t length;
- while (dwarf_nextcu(dwarf, offset, &next_offset, &length, nullptr, NULL, NULL) ==
+ while (dwarf_nextcu(dwarf, offset, &next_offset, &length, nullptr, nullptr, nullptr) ==
0) {
Dwarf_Die unit_die;
if (dwarf_offdie(dwarf, offset + length, &unit_die) != nullptr)
- MC_dwarf_handle_children(info, &unit_die, &unit_die, nullptr, NULL);
+ MC_dwarf_handle_children(info, &unit_die, &unit_die, nullptr, nullptr);
offset = next_offset;
}
}
#include <vector>
+#include <xbt/dynar.h>
+#include <xbt/automaton.h>
+#include <xbt/swag.h>
+
#include "mc_base.h"
#include "mc/mc.h"
assert(n == xbt_dynar_length(initial_communications_pattern));
for (unsigned j=0; j < n ; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
- xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
+ xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
}
}
#include <elfutils/libdw.h>
#include <simgrid/msg.h>
-#include <xbt/fifo.h>
#include <xbt/config.h>
#include <xbt/base.h>
#include <xbt/automaton.h>
#include <sstream>
#include <string>
-#include <xbt/fifo.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include <vector>
#include <xbt/base.h>
-#include <xbt/dynar.h>
-#include <xbt/fifo.h>
namespace simgrid {
namespace mc {
// **** Data conversion
-/** Generate a string representation
-*
-* The current format is a ";"-delimited list of pairs:
-* "pid0,value0;pid2,value2;pid3,value3". The value can be
-* omitted is it is null.
-*/
-XBT_PRIVATE char* MC_record_stack_to_string(xbt_fifo_t stack);
-
SG_END_DECL()
#endif
/** Replay path (if any) in string representation
*
- * This is a path as generated by `MC_record_stack_to_string()`.
+ * This is using the format generated by traceToString().
*/
XBT_PUBLIC_DATA(char*) MC_record_path;
#include <xbt/str.h>
#include <xbt/sysdep.h>
#include <xbt/dynar.h>
+#include <xbt/swag.h>
#include "src/mc/mc_request.h"
#include "src/mc/mc_safety.h"
if (r1->call == SIMCALL_COMM_WAIT
&& (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
- && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == NULL))
+ && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == nullptr))
return false;
if (r1->call == SIMCALL_COMM_TEST &&
act = remote_act;
char* p;
- if (act->comm.src_proc == nullptr || act->comm.dst_proc == NULL) {
+ if (act->comm.src_proc == nullptr || act->comm.dst_proc == nullptr) {
type = "Test FALSE";
p = pointer_to_string(remote_act);
args = bprintf("comm=%s", p);
s_smx_synchro_t synchro;
mc_model_checker->process().read_bytes(&synchro,
sizeof(synchro), remote(remote_act));
- if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == NULL) {
+ if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == nullptr) {
if (issuer->host)
label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
issuer->pid,
#include <simgrid_config.h>
#include <xbt/base.h>
-#include <xbt/dynar.h>
#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_state.h"
return process_info;
}
-/** Load the remote swag of processes into a dynar
+/** Load the remote swag of processes into a vector
*
* @param process MCed process
- * @param target Local dynar (to be filled with copies of `s_smx_process_t`)
+ * @param target Local vector (to be filled with copies of `s_smx_process_t`)
* @param remote_swag Address of the process SWAG in the remote list
*/
static void MC_process_refresh_simix_process_list(
s_xbt_swag_t swag;
process->read_bytes(&swag, sizeof(swag), remote(remote_swag));
- // Load each element of the dynar from the MCed process:
+ // Load each element of the vector from the MCed process:
int i = 0;
for (smx_process_t p = (smx_process_t) swag.head; p; ++i) {
static inline __attribute__ ((always_inline))
const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot)
{
- if(snapshot==NULL)
- xbt_die("snapshot is NULL");
+ if(snapshot==nullptr)
+ xbt_die("snapshot is nullptr");
return mc_model_checker->process().get_heap()->breakval;
}
simgrid::mc::State* MC_state_new()
{
simgrid::mc::State* state = new simgrid::mc::State();
- std::memset(&state->internal_comm, 0, sizeof(state->internal_comm));
- std::memset(&state->internal_req, 0, sizeof(state->internal_req));
- std::memset(&state->executed_req, 0, sizeof(state->executed_req));
state->processStates.resize(MC_smx_get_maxpid());
state->num = ++mc_stats->expanded_states;
/* Stateful model checking */
std::memset(&this->executed_req, 0, sizeof(this->executed_req));
}
-State::~State()
-{
- xbt_free(this->incomplete_comm_pattern);
-}
-
std::size_t State::interleaveSize() const
{
return std::count_if(this->processStates.begin(), this->processStates.end(),
state->processStates[process->pid].interleave_count = 0;
}
-void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process)
-{
- if (state->processStates[process->pid].state == simgrid::mc::ProcessInterleaveState::interleave)
- state->processStates[process->pid].state = simgrid::mc::ProcessInterleaveState::done;
-}
-
void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req,
int value)
{
extern XBT_PRIVATE std::unique_ptr<s_mc_global_t> initial_global_state;
+struct PatternCommunication {
+ int num = 0;
+ smx_synchro_t comm_addr;
+ e_smx_comm_type_t type = SIMIX_COMM_SEND;
+ unsigned long src_proc = 0;
+ unsigned long dst_proc = 0;
+ const char *src_host = nullptr;
+ const char *dst_host = nullptr;
+ std::string rdv;
+ std::vector<char> data;
+ int tag = 0;
+ int index = 0;
+
+ PatternCommunication()
+ {
+ std::memset(&comm_addr, 0, sizeof(comm_addr));
+ }
+
+ PatternCommunication dup() const
+ {
+ simgrid::mc::PatternCommunication res;
+ // num?
+ res.comm_addr = this->comm_addr;
+ res.type = this->type;
+ // src_proc?
+ // dst_proc?
+ res.dst_proc = this->dst_proc;
+ res.dst_host = this->dst_host;
+ res.rdv = this->rdv;
+ res.data = this->data;
+ // tag?
+ res.index = this->index;
+ return res;
+ }
+
+};
+
/* Possible exploration status of a process in a state */
enum class ProcessInterleaveState {
no_interleave=0, /* Do not interleave (do not execute) */
int num = 0;
int in_visited_states = 0;
- // comm determinism verification (xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>):
- xbt_dynar_t incomplete_comm_pattern = nullptr;
+ // comm determinism verification (xbt_dynar_t<xbt_dynar_t<simgrid::mc::PatternCommunication*>):
+ std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern;
// For communication determinism verification:
std::vector<unsigned> communicationIndices;
State();
- ~State();
-
- State(State const&) = delete;
- State operator=(State const&) = delete;
- State(State const&&) = delete;
- State operator=(State const&&) = delete;
std::size_t interleaveSize() const;
};
XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value);
XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
-XBT_PRIVATE void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process);
#endif
echo "XX"
tar xzf `cat VERSION`.tar.gz
cd `cat VERSION`
- SRCFOLDER="."
+ mkdir build
+ cd build
+ SRCFOLDER=".."
else
#for windows we don't make dist, but we still want to build out of source
SRCFOLDER=$WORKSPACE
if test "$(uname -o)" != "Msys"; then
cd $WORKSPACE/build
- cd `cat VERSION`
+ cd `cat VERSION`/build
fi
TRES=0
