Process and host names are not handled yet.
_xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \
(_cursor)++ )
+#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
+ for (_xbt_dynar_cursor_first(_dynar,&(_cursor)) ; \
+ (_ptr = _cursor < _dynar->used ? xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
+ (_cursor)++ )
+
/** @} */
SG_END_DECL()
#ifdef HAVE_MC
#include "mc_process.h"
#include "mc_model_checker.h"
+#include "mc_protocol.h"
#endif
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
{
unsigned int index = 0;
smx_synchro_t act = 0;
+#ifdef HAVE_MC
+ s_smx_synchro_t temp_synchro;
+#endif
switch (req->call) {
case SIMCALL_NONE:
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
act = simcall_comm_wait__get__comm(req);
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (simcall_comm_wait__get__timeout(req) >= 0) {
/* If it has a timeout it will be always be enabled, because even if the
* communication is not ready, it can timeout and won't block. */
case SIMCALL_COMM_WAITANY:
/* Check if it has at least one communication ready */
- xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+ xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (act->comm.src_proc && act->comm.dst_proc)
return TRUE;
+ }
return FALSE;
default:
snapshot->address_space.address_space_class = &mc_snapshot_class;
snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
+
smx_process_t process;
- // FIXME, cross-process support (simix_global->process_list)
- xbt_swag_foreach(process, simix_global->process_list) {
- xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid);
- }
+ MC_EACH_SIMIX_PROCESS(process,
+ xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid));
MC_snapshot_handle_ignore(snapshot);
void MC_client_handle_messages(void);
void MC_client_send_message(void* message, size_t size);
+#ifdef HAVE_MC
void MC_ignore(void* addr, size_t size);
-
+#endif
SG_END_DECL()
}
}
+// FIXME, remote comm
static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
{
mc_process_t process = &mc_model_checker->process;
void *addr_pointed;
comm_pattern->src_proc = comm->comm.src_proc->pid;
comm_pattern->dst_proc = comm->comm.dst_proc->pid;
+ // FIXME, get remote host name
comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
}
-void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type)
+void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type)
{
mc_process_t process = &mc_model_checker->process;
mc_comm_pattern_t pattern = NULL;
pattern->data_size = -1;
pattern->data = NULL;
- pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t));
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, request);
+ mc_list_comm_pattern_t initial_pattern =
+ (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+ xbt_dynar_t incomplete_pattern =
+ (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ pattern->index =
+ initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
void *addr_pointed;
pattern->comm = simcall_comm_isend__get__result(request);
pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->src_proc = pattern->comm->comm.src_proc->pid;
- pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
+ // FIXME, get remote host name
+ pattern->src_host = simcall_host_get_name(issuer->smx_host);
if(pattern->comm->comm.src_buff != NULL){
pattern->data_size = pattern->comm->comm.src_buff_size;
pattern->data = xbt_malloc0(pattern->data_size);
pattern->comm = simcall_comm_irecv__get__result(request);
pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
- pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
+ // FIXME, remote process access
+ pattern->dst_host = simcall_host_get_name(issuer->smx_host);
} else {
xbt_die("Unexpected call_type %i", (int) call_type);
}
- xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern);
+ xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
- XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid);
+ XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
}
void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) {
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
}
- }
+ );
xbt_fifo_unshift(mc_stack, initial_state);
}
/* Answer the request */
- SIMIX_simcall_handle(req, value); /* After this call req is no longer useful */
+ MC_simcall_handle(req, value); /* After this call req is no longer useful */
MC_SET_MC_HEAP;
if(!initial_global_state->initial_communications_pattern_done)
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get enabled processes and insert them in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
}
- }
+ );
if (dot_output != NULL)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
smx_process_t process;
if (xbt_swag_size(simix_global->process_list)) {
deadlock = TRUE;
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
deadlock = FALSE;
break;
}
- }
+ );
}
return deadlock;
}
if (saved_req) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- req = &saved_req->issuer->simcall;
+
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ req = &issuer->simcall;
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = mc_get_call_type(req);
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
if (saved_req != NULL) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- req = &saved_req->issuer->simcall;
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ req = &issuer->simcall;
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
}
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
MC_wait_for_requests();
}
initial_pair->depth = 1;
/* Get enabled processes and insert them in the interleave set of the graph_state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_pair->graph_state, process);
}
- }
+ );
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
initial_pair->search_cycle = 0;
mc_stats->visited_pairs++;
/* Answer the request */
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
next_pair->atomic_propositions = get_atomic_propositions_values();
next_pair->depth = current_pair->depth + 1;
/* Get enabled processes and insert them in the interleave set of the next graph_state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_pair->graph_state, process);
}
- }
+ );
next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
#include <sys/types.h>
#include <simgrid_config.h>
+#include <xbt/dynar.h>
#include "mc_forward.h"
#include "mc_process.h"
#include "mc_page_store.h"
+#include "mc_protocol.h"
SG_BEGIN_DECL()
mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
void MC_model_checker_delete(mc_model_checker_t mc);
+#define MC_EACH_SIMIX_PROCESS(process, code) \
+ if (MC_process_is_self(&mc_model_checker->process)) { \
+ xbt_swag_foreach(process, simix_global->process_list) { \
+ code; \
+ } \
+ } else { \
+ MC_process_refresh_simix_processes(&mc_model_checker->process); \
+ unsigned int _smx_process_index; \
+ mc_smx_process_info_t _smx_process_info; \
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
+ smx_process_t process = &_smx_process_info->copy; \
+ code; \
+ } \
+ }
+
SG_END_DECL()
#endif
#include "mc_snapshot.h"
#include "mc_ignore.h"
+#include "simix/smx_private.h"
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
&process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
MC_PROCESS_INDEX_DISABLED);
+ process->smx_process_infos = mc_smx_process_info_list_new();
+ process->smx_old_process_infos = mc_smx_process_info_list_new();
+
process->checkpoint_ignore = MC_checkpoint_ignore_new();
process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors , __BYTE_ORDER);
xbt_dynar_free(&process->checkpoint_ignore);
+ xbt_dynar_free(&process->smx_process_infos);
+ xbt_dynar_free(&process->smx_old_process_infos);
+
size_t i;
for (i=0; i!=process->object_infos_size; ++i) {
MC_free_object_info(&process->object_infos[i]);
MC_PROCESS_INDEX_DISABLED);
}
+/** Load the remote swag of processes into a dynar
+ *
+ * @param process MCed process
+ * @param target Local dynar (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(
+ mc_process_t process,
+ xbt_dynar_t target, xbt_swag_t remote_swag)
+{
+ // swag = REMOTE(*simix_global->process_list)
+ s_xbt_swag_t swag;
+ MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag),
+ MC_PROCESS_INDEX_ANY);
+
+ smx_process_t p;
+ xbt_dynar_reset(target);
+
+ int i = 0;
+ for (p = swag.head; p; ++i) {
+
+ s_mc_smx_process_info_t info;
+ info.address = p;
+ MC_process_read(process, MC_PROCESS_NO_FLAG,
+ &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY);
+ xbt_dynar_push(target, &info);
+
+ // Lookup next process address:
+ p = xbt_swag_getNext(&info.copy, swag.offset);
+ }
+ assert(i == swag.count);
+}
+
+void MC_process_refresh_simix_processes(mc_process_t process)
+{
+ if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
+ return;
+
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+ // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
+
+ // simix_global_p = REMOTE(simix_global);
+ smx_global_t simix_global_p;
+ MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p));
+
+ // simix_global = REMOTE(*simix_global)
+ s_smx_global_t simix_global;
+ MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global),
+ MC_PROCESS_INDEX_ANY);
+
+ MC_process_refresh_simix_process_list(
+ process, process->smx_process_infos, simix_global.process_list);
+ MC_process_refresh_simix_process_list(
+ process, process->smx_old_process_infos, simix_global.process_to_destroy);
+
+ process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+ mmalloc_set_current_heap(heap);
+}
+
#define SO_RE "\\.so[\\.0-9]*$"
#define VERSION_RE "-[\\.0-9]*$"
{
const size_t n = process->object_infos_size;
size_t i;
+
+ // First lookup the variable in the executable shared object.
+ // A global variable used directly by the executable code from a library
+ // is reinstanciated in the executable memory .data/.bss.
+ // We need to look up the variable in the execvutable first.
+ if (process->binary_info) {
+ mc_object_info_t info = process->binary_info;
+ dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
+ if (var)
+ return var;
+ }
+
for (i=0; i!=n; ++i) {
mc_object_info_t info =process->object_infos[i];
dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
if (var)
return var;
}
+
return NULL;
}
+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size)
+{
+ dw_variable_t var = MC_process_find_variable_by_name(process, name);
+ if (!var->address)
+ xbt_die("No simple location for this variable");
+ MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size,
+ MC_PROCESS_INDEX_ANY);
+}
+
// ***** Memory access
int MC_process_vm_open(pid_t pid, int flags)
}
}
}
+
+/** Get the issuer of a simcall (`req->issuer`)
+ *
+ * In split-process mode, it does the black magic necessary to get an address
+ * of a (shallow) copy of the data structure the issuer SIMIX process in the local
+ * address space.
+ *
+ * @param process the MCed process
+ * @param req the simcall (copied in the local process)
+ */
+smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req)
+{
+ if (MC_process_is_self(&mc_model_checker->process))
+ return req->issuer;
+
+ MC_process_refresh_simix_processes(process);
+
+ // This is the address of the smx_process in the MCed process:
+ void* address = req->issuer;
+
+ unsigned i;
+ mc_smx_process_info_t p;
+
+ xbt_dynar_foreach_ptr(process->smx_process_infos, i, p)
+ if (p->address == address)
+ return &p->copy;
+ xbt_dynar_foreach_ptr(process->smx_old_process_infos, i, p)
+ if (p->address == address)
+ return &p->copy;
+
+ xbt_die("Issuer not found");
+}
+
+void MC_simcall_handle(smx_simcall_t req, int value)
+{
+ if (MC_process_is_self(&mc_model_checker->process)) {
+ SIMIX_simcall_handle(req, value);
+ return;
+ }
+
+ MC_process_refresh_simix_processes(&mc_model_checker->process);
+
+ unsigned i;
+ mc_smx_process_info_t pi = NULL;
+
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+ smx_process_t p = (smx_process_t) pi->address;
+ if (req == &pi->copy.simcall) {
+ smx_simcall_t real_req = &p->simcall;
+ // TODO, use a remote call
+ SIMIX_simcall_handle(real_req, value);
+ return;
+ }
+ }
+
+ // Check (remove afterwards):
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+ smx_process_t p = (smx_process_t) pi->address;
+ if (req == &p->simcall)
+ xbt_die("The real simcall was passed. We expected the local copy.");
+ }
+
+ xbt_die("Could not find the request");
+}
+
+void mc_smx_process_info_clear(mc_smx_process_info_t p)
+{
+ // Nothing yet
+}
#include "xbt/mmalloc/mmprivate.h"
#include "simix/popping_private.h"
+#include "simix/smx_private.h"
#include "mc_forward.h"
#include "mc_mmalloc.h" // std_heap
#include "mc_memory_map.h"
#include "mc_address_space.h"
+#include "mc_protocol.h"
SG_BEGIN_DECL()
typedef enum {
MC_PROCESS_CACHE_FLAG_HEAP = 1,
MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,
+ MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,
} e_mc_process_cache_flags_t ;
+struct s_mc_smx_process_info {
+ void* address;
+ struct s_smx_process copy;
+};
+
+typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
+
/** Representation of a process
*/
struct s_mc_process {
size_t object_infos_size;
int memory_file;
- // Cache: don't use those fields directly but with the getters
- // which ensure that proper synchronisation has been done.
+ xbt_dynar_t smx_process_infos;
+ xbt_dynar_t smx_old_process_infos;
+ /** State of the cache (which variables are up to date) */
e_mc_process_cache_flags_t cache_flags;
- /** Address of the heap structure in the target process.
- */
+ /** Address of the heap structure in the MCed process. */
void* heap_address;
/** Copy of the heap structure of the process
* */
void MC_process_refresh_malloc_info(mc_process_t process);
+void MC_process_refresh_simix_processes(mc_process_t process);
+
static inline
bool MC_process_is_self(mc_process_t process)
{
dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size);
+
static inline xbt_mheap_t MC_process_get_heap(mc_process_t process)
{
if (MC_process_is_self(process))
*/
dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
+// ***** Things to move somewhere else:
+
+smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req);
+
+void MC_simcall_handle(smx_simcall_t req, int value);
+
+void mc_smx_process_info_clear(mc_smx_process_info_t p);
+
+static inline
+xbt_dynar_t mc_smx_process_info_list_new()
+{
+ return xbt_dynar_new(
+ sizeof(s_mc_smx_process_info_t), (void_f_pvoid_t) &mc_smx_process_info_clear);
+}
+
SG_END_DECL()
#endif
mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
int value = 0;
smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
- int pid = saved_req->issuer->pid;
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+ const int pid = issuer->pid;
// Serialization the (pid, value) pair:
const char* sep = (item!=start) ? ";" : "";
SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
simcall_comm_irecv__get__rdv(r1);
+ // FIXME, remote access to comm object
+
if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
smx_synchro_t act = NULL;
size_t size = 0;
+ // FIXME, host_get_name
+ // FIXME, buffer access (issuer->name, issuer->smx_host)
+
+ smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+
switch (req->call) {
case SIMCALL_COMM_ISEND:
type = xbt_strdup("iSend");
p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
args =
- bprintf("src=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), issuer->name,
p, bs);
else
args =
- bprintf("src=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
- req->issuer->name, p, bs);
+ bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
+ issuer->name, p, bs);
break;
case SIMCALL_COMM_IRECV:
size =
type = xbt_strdup("iRecv");
p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
bs = buff_size_to_string(size);
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
args =
- bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), issuer->name,
p, bs);
else
args =
- bprintf("dst=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
- req->issuer->name, p, bs);
+ bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
+ issuer->name, p, bs);
break;
case SIMCALL_COMM_WAIT:
act = simcall_comm_wait__get__comm(req);
if (args != NULL) {
str =
- bprintf("[(%lu)%s (%s)] %s(%s)", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), issuer->name,
type, args);
} else {
str =
- bprintf("[(%lu)%s (%s)] %s ", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+ bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), issuer->name,
type);
}
char *MC_request_get_dot_output(smx_simcall_t req, int value)
{
+ // TODO, remote access to MSG_host_get_name(issuer->smx_host)
char *str = NULL, *label = NULL;
smx_synchro_t act = NULL;
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+
switch (req->call) {
case SIMCALL_COMM_ISEND:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] iSend", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] iSend", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] iSend", req->issuer->pid);
+ label = bprintf("[(%lu)] iSend", issuer->pid);
break;
case SIMCALL_COMM_IRECV:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] iRecv", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] iRecv", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] iRecv", req->issuer->pid);
+ label = bprintf("[(%lu)] iRecv", issuer->pid);
break;
case SIMCALL_COMM_WAIT:
act = simcall_comm_wait__get__comm(req);
if (value == -1) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] WaitTimeout", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] WaitTimeout", req->issuer->pid);
+ label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host),
+ bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
+ MSG_host_get_name(issuer->smx_host),
act->comm.src_proc ? act->comm.src_proc->pid : 0,
act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
else
label =
- bprintf("[(%lu)] Wait [(%lu)->(%lu)]", req->issuer->pid,
+ bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
act->comm.src_proc ? act->comm.src_proc->pid : 0,
act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
}
case SIMCALL_COMM_TEST:
act = simcall_comm_test__get__comm(req);
if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Test FALSE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] Test FALSE", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] Test FALSE", req->issuer->pid);
+ label = bprintf("[(%lu)] Test FALSE", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] Test TRUE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] Test TRUE", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] Test TRUE", req->issuer->pid);
+ label = bprintf("[(%lu)] Test TRUE", issuer->pid);
}
break;
case SIMCALL_COMM_WAITANY:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] WaitAny [%d of %lu]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value + 1,
+ bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), value + 1,
xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
else
label =
- bprintf("[(%lu)] WaitAny [%d of %lu]", req->issuer->pid, value + 1,
+ bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
break;
case SIMCALL_COMM_TESTANY:
if (value == -1) {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] TestAny FALSE", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] TestAny FALSE", req->issuer->pid);
+ label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
} else {
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value + 1,
+ bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), value + 1,
xbt_dynar_length(simcall_comm_testany__get__comms(req)));
else
label =
- bprintf("[(%lu)] TestAny TRUE [%d of %lu]", req->issuer->pid,
+ bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
value + 1,
xbt_dynar_length(simcall_comm_testany__get__comms(req)));
}
break;
case SIMCALL_MC_RANDOM:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_RANDOM (%d)", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host), value);
+ bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
+ MSG_host_get_name(issuer->smx_host), value);
else
- label = bprintf("[(%lu)] MC_RANDOM (%d)", req->issuer->pid, value);
+ label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
break;
case SIMCALL_MC_SNAPSHOT:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_SNAPSHOT", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] MC_SNAPSHOT", req->issuer->pid);
+ label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
break;
case SIMCALL_MC_COMPARE_SNAPSHOTS:
- if (req->issuer->smx_host)
+ if (issuer->smx_host)
label =
- bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", req->issuer->pid,
- MSG_host_get_name(req->issuer->smx_host));
+ bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
+ MSG_host_get_name(issuer->smx_host));
else
- label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", req->issuer->pid);
+ label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
break;
default:
str =
bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
- colors[req->issuer->pid - 1], colors[req->issuer->pid - 1]);
+ colors[issuer->pid - 1], colors[issuer->pid - 1]);
xbt_free(label);
return str;
/* 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 <assert.h>
+
#include "mc_state.h"
#include "mc_request.h"
#include "mc_safety.h"
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_state = MC_state_new();
-
MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
+ );
xbt_fifo_unshift(mc_stack, initial_state);
mmalloc_set_current_heap(heap);
mc_stats->executed_transitions++;
/* Answer the request */
- SIMIX_simcall_handle(req, value);
+ MC_simcall_handle(req, value);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get an enabled process and insert it in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
+ );
if (dot_output != NULL)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
if (mc_reduce_kind == e_mc_reduce_dpor) {
req = MC_state_get_internal_request(state);
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
xbt_free(req_str);
}
- if (!MC_state_process_is_done(prev_state, req->issuer))
- MC_state_interleave_process(prev_state, req->issuer);
+ if (!MC_state_process_is_done(prev_state, issuer))
+ MC_state_interleave_process(prev_state, issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
} else {
+ const smx_process_t previous_issuer = MC_process_get_issuer(&mc_model_checker->process, MC_state_get_internal_request(prev_state));
XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
- req->call, req->issuer->pid, state->num,
+ req->call, issuer->pid, state->num,
MC_state_get_internal_request(prev_state)->call,
- MC_state_get_internal_request(prev_state)->issuer->pid,
+ previous_issuer->pid,
prev_state->num);
}
/* 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 <assert.h>
+
#include "../simix/smx_private.h"
#include "xbt/fifo.h"
#include "mc_state.h"
void MC_state_interleave_process(mc_state_t state, smx_process_t process)
{
+ assert(state);
state->proc_status[process->pid].state = MC_INTERLEAVE;
state->proc_status[process->pid].interleave_count = 0;
}
case SIMCALL_COMM_WAITANY:
state->internal_req.call = SIMCALL_COMM_WAIT;
state->internal_req.issuer = req->issuer;
+ // FIXME, read from remote process
state->internal_comm =
*xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
smx_synchro_t);
state->internal_req.issuer = req->issuer;
if (value > 0)
+ // FIXME, read from remote process
state->internal_comm =
*xbt_dynar_get_as(simcall_comm_testany__get__comms(req), value,
smx_synchro_t);
case SIMCALL_COMM_WAIT:
state->internal_req = *req;
+ // FIXME, read from remote process
state->internal_comm = *(simcall_comm_wait__get__comm(req));
simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
case SIMCALL_COMM_TEST:
state->internal_req = *req;
+ // FIXME, read from remote process
state->internal_comm = *simcall_comm_test__get__comm(req);
simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
case SIMCALL_MC_RANDOM:
state->internal_req = *req;
- if (value != simcall_mc_random__get__max(req)) {
- xbt_swag_foreach(process, simix_global->process_list) {
+ int random_max = simcall_mc_random__get__max(req);
+ if (value != random_max) {
+ MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
- if (process->pid == req->issuer->pid) {
+ const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+ if (process->pid == issuer->pid) {
procstate->state = MC_MORE_INTERLEAVE;
break;
}
- }
+ );
}
break;
unsigned int start_count;
smx_synchro_t act = NULL;
- xbt_swag_foreach(process, simix_global->process_list) {
+ MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
if (procstate->state == MC_INTERLEAVE
}
}
}
- }
+ );
return NULL;
}
xbt_test_log("Pop %d, length=%lu", cpt, xbt_dynar_length(d));
}
+ int* pi;
+ xbt_dynar_foreach_ptr(d, cursor, pi) {
+ *pi = 0;
+ }
+ xbt_dynar_foreach(d, cursor, i) {
+ xbt_test_assert(i == 0, "The value is not the same as the expected one.");
+ }
+ xbt_dynar_foreach_ptr(d, cursor, pi) {
+ *pi = 1;
+ }
+ xbt_dynar_foreach(d, cursor, i) {
+ xbt_test_assert(i == 1, "The value is not the same as the expected one.");
+ }
+
/* 5. Free the resources */
xbt_dynar_free(&d); /* This code is used both as example and as regression test, so we try to */
xbt_dynar_free(&d); /* free the struct twice here to check that it's ok, but freeing it only once */