visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
- for (i=0; i<simix_process_maxpid; i++){
+ for (i=0; i < MC_smx_get_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), comm_pattern_free_voidp);
process_list_pattern->index_comm = 0;
xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
}
incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
- for (i=0; i<simix_process_maxpid; i++){
+ for (i=0; i < MC_smx_get_maxpid(); i++){
xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
}
}
- mc_time = xbt_new0(double, simix_process_maxpid);
-
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_model_checker = MC_model_checker_new(pid, socket);
+ if (mc_mode == MC_MODE_SERVER) {
+ int maxpid;
+ MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+ &maxpid, sizeof(maxpid));
+ simix_process_maxpid = maxpid;
+ }
+
+ mmalloc_set_current_heap(std_heap);
+ mc_time = xbt_new0(double, MC_smx_get_maxpid());
+ mmalloc_set_current_heap(mc_heap);
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
/* Those requests are handled on the client side and propagated by message
* to the server: */
- MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+ MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double));
smx_process_t process;
xbt_swag_foreach(process, simix_global->process_list) {
MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
}
}
+
}
mmalloc_set_current_heap(heap);
mc_comm_pattern_t comm;
cursor = 0;
xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;
- for(int i=0; i<simix_process_maxpid; i++){
+ for(int i=0; i < MC_smx_get_maxpid(); i++){
initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
xbt_dynar_reset(initial_incomplete_process_comms);
incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- for (j=0; j<simix_process_maxpid; j++) {
+ for (j=0; j < simix_process_maxpid; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
}
mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
void MC_model_checker_delete(mc_model_checker_t mc);
+static inline
+int MC_smx_get_maxpid(void)
+{
+ // Currently we use the same variable in STANDALONE and in SERVER mode:
+ return simix_process_maxpid;
+}
+
SG_END_DECL()
#endif
#include "xbt/parmap.h"
#include "mc_forward.h"
+#include "mc_protocol.h"
SG_BEGIN_DECL()
void MC_record_replay_init()
{
- mc_time = xbt_new0(double, simix_process_maxpid);
+ mc_time = xbt_new0(double, MC_smx_get_maxpid());
}
mc_comm_pattern_t comm;
unsigned int cursor;
state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
- for (i=0; i<simix_process_maxpid; i++) {
+ for (i=0; i < MC_smx_get_maxpid(); i++) {
incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
xbt_dynar_t incomplete_process_comms_copy = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
xbt_dynar_foreach(incomplete_process_comms, cursor, comm) {
*/
mc_state_t MC_state_new()
{
- mc_state_t state = NULL;
-
- state = xbt_new0(s_mc_state_t, 1);
- state->max_pid = simix_process_maxpid;
+ mc_state_t state = xbt_new0(s_mc_state_t, 1);
+ state->max_pid = MC_smx_get_maxpid();
state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
state->system_state = NULL;
state->num = ++mc_stats->expanded_states;
are incomplete and they cannot be analyzed and compared with the initial pattern. */
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
int current_process = 1;
- while (current_process < simix_process_maxpid) {
+ while (current_process < MC_smx_get_maxpid()) {
if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
partial_comm = 1;
#include "xbt/log.h"
#include "xbt/dict.h"
#include "mc/mc.h"
+#include "mc/mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
"Logging specific to SIMIX (process)");