if (!MSG_comm_test(node.comm_receive)) {
// no task was received: make some periodic calls
- if (MSG_get_clock() >= next_stabilize_date) {
- stabilize(&node);
- next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
- }
- else if (MSG_get_clock() >= next_fix_fingers_date) {
- fix_fingers(&node);
- next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
- }
- else if (MSG_get_clock() >= next_check_predecessor_date) {
- check_predecessor(&node);
- next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
- }
- else if (MSG_get_clock() >= next_lookup_date) {
- random_lookup(&node);
- next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
- }
- else {
- // nothing to do: sleep for a while
- MSG_process_sleep(5);
+
+ if(MC_is_active()){
+ if(MC_random()){
+ stabilize(&node);
+ }else if(MC_random()){
+ fix_fingers(&node);
+ }else if(MC_random()){
+ check_predecessor(&node);
+ }else if(MC_random()){
+ random_lookup(&node);
+ }else{
+ MSG_process_sleep(5);
+ }
+ }else{
+ if (MSG_get_clock() >= next_stabilize_date) {
+ stabilize(&node);
+ next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
+ }
+ else if (MSG_get_clock() >= next_fix_fingers_date) {
+ fix_fingers(&node);
+ next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
+ }
+ else if (MSG_get_clock() >= next_check_predecessor_date) {
+ check_predecessor(&node);
+ next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
+ }
+ else if (MSG_get_clock() >= next_lookup_date) {
+ random_lookup(&node);
+ next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
+ }
+ else {
+ // nothing to do: sleep for a while
+ MSG_process_sleep(5);
+ }
}
+
} else {
// a transfer has occurred
#define MC_is_active() _sg_do_model_check
XBT_PUBLIC(void) MC_assert(int);
-XBT_PUBLIC(int) MC_random(int min, int max);
+XBT_PUBLIC(int) MC_random(void);
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
XBT_PUBLIC(void *) MC_snapshot(void);
XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
/************************** MC simcalls **********************************/
XBT_PUBLIC(void *) simcall_mc_snapshot(void);
XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2);
-XBT_PUBLIC(int) simcall_mc_random(int min, int max);
+XBT_PUBLIC(int) simcall_mc_random(void);
/************************** New API simcalls **********************************/
/* TUTORIAL: New API */
xbt_abort();
}
-int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+int SIMIX_pre_mc_random(smx_simcall_t simcall){
return simcall->mc_value;
}
-int MC_random(int min, int max)
+int MC_random(void)
{
/*FIXME: return mc_current_state->executed_transition->random.value;*/
- return simcall_mc_random(min, max);
+ return simcall_mc_random();
}
/**
void MC_show_deadlock(smx_simcall_t req);
void MC_show_stack_safety(xbt_fifo_t stack);
void MC_dump_stack_safety(xbt_fifo_t stack);
-
-int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
+void MC_init(void);
+int SIMIX_pre_mc_random(smx_simcall_t simcall);
/********************************* Requests ***********************************/
int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
typedef enum {
MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */
MC_INTERLEAVE, /* Interleave the process (one or more request) */
+ MC_MORE_INTERLEAVE, /* Interleave twice the process (for mc_random simcall) */
MC_DONE /* Already interleaved */
} e_mc_process_state_t;
void MC_dpor_init(void);
void MC_dpor(void);
-void MC_init(void);
typedef struct s_mc_safety_visited_state{
mc_snapshot_t system_state;
return TRUE;
if (r1->issuer == r2->issuer)
- return FALSE;
-
- if((r1->call == SIMCALL_MC_RANDOM) || (r2->call == SIMCALL_MC_RANDOM))
- return FALSE;
+ return FALSE;
if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
return FALSE;
case SIMCALL_MC_RANDOM:
type = xbt_strdup("MC_RANDOM");
- args = '\0';
+ args = bprintf("%d", value);
break;
default:
unsigned int i, size=0;
for(i=0; i < state->max_pid; i++){
- if(state->proc_status[i].state == MC_INTERLEAVE)
+ if((state->proc_status[i].state == MC_INTERLEAVE) || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
size++;
}
{
state->executed_req = *req;
state->req_num = value;
+ smx_process_t process = NULL;
+ mc_procstate_t procstate = NULL;
/* The waitany and testany request are transformed into a wait or test request over the
* corresponding communication action so it can be treated later by the dependence
case SIMCALL_MC_RANDOM:
state->internal_req = *req;
simcall_mc_random__set__result(&state->internal_req, value);
+ if(value == 0){
+ xbt_swag_foreach(process, simix_global->process_list){
+ procstate = &state->proc_status[process->pid];
+ if(process->pid == req->issuer->pid){
+ procstate->state = MC_MORE_INTERLEAVE;
+ break;
+ }
+ }
+ }
break;
default:
break;
}
}
-
+
smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value)
{
*value = state->req_num;
smx_process_t process = NULL;
mc_procstate_t procstate = NULL;
unsigned int start_count;
- int min, max;
-
- static int first = 0;
- if(first == 0){
- srand(987654321);
- first = 1;
- }
xbt_swag_foreach(process, simix_global->process_list){
procstate = &state->proc_status[process->pid];
- if(procstate->state == MC_INTERLEAVE){
+ if(procstate->state == MC_INTERLEAVE || procstate->state == MC_MORE_INTERLEAVE){
if(MC_process_is_enabled(process)){
switch(process->simcall.call){
case SIMCALL_COMM_WAITANY:
break;
case SIMCALL_MC_RANDOM:
- min = simcall_mc_random__get__min(&process->simcall);
- max = simcall_mc_random__get__max(&process->simcall);
- *value = (int)((rand() % ((max-min)+1)) + min);
+ if(procstate->state == MC_INTERLEAVE)
+ *value = 0;
+ else
+ *value = 1;
procstate->state = MC_DONE;
return &process->simcall;
break;
#define SIMCALL_LIST4(ACTION, sep) \
ACTION(SIMCALL_MC_SNAPSHOT, mc_snapshot, WITH_ANSWER, TPTR(result)) sep \
ACTION(SIMCALL_MC_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) sep \
-ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result), TINT(min), TINT(max)) sep
+ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result)) sep
#else
#define SIMCALL_LIST4(ACTION, sep)
#endif
return simcall_BODY_mc_compare_snapshots(s1, s2);
}
-int simcall_mc_random(int min, int max)
+int simcall_mc_random(void)
{
- return simcall_BODY_mc_random(min, max);
+ return simcall_BODY_mc_random();
}