Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Bugfix: fix memory leak related to transition creation/destruction. Instead of using...
[simgrid.git] / src / mc / mc_transition.c
1 #include "private.h"
2
3 /**
4  * \brief Create a model-checker transition and add it to the set of avaiable
5  *        transitions of the current state, if not running in replay mode.
6  * \param process The process who wants to perform the transition
7  * \param comm The type of then transition (comm_send, comm_recv)
8 */
9 mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_rdv_t rdv, smx_comm_t comm)
10 {
11   mc_state_t current_state = NULL;
12   char *type_str = NULL;
13   
14   if(!mc_replay_mode){
15     MC_SET_RAW_MEM;
16     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
17
18     /* Generate a string for the "type" */
19     switch(type){
20       case mc_isend:
21         type_str = bprintf("iSend");
22         break;
23       case mc_irecv:
24         type_str = bprintf("iRecv");
25         break;
26       case mc_wait:
27         type_str = bprintf("Wait");
28         break;
29       case mc_waitany:
30         type_str = bprintf("WaitAny");
31         break;
32       default:
33         xbt_die("Invalid transition type");
34     }
35     
36     trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans);
37     xbt_free(type_str);
38     
39     trans->type = type;
40     trans->process = p;
41     trans->rdv = rdv;
42     trans->comm = comm;
43     /* Push it onto the enabled transitions set of the current state */
44
45    current_state = (mc_state_t) 
46       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
47     xbt_setset_set_insert(current_state->created_transitions, trans);
48     xbt_setset_set_insert(current_state->transitions, trans);
49     MC_UNSET_RAW_MEM;
50     return trans;
51   }
52   return NULL;
53 }
54
55 void MC_random_create(int min, int max)
56 {
57   smx_process_t p;
58   mc_state_t current_state = NULL;
59   char *type_str = NULL;
60   
61   if(!mc_replay_mode){
62     p = SIMIX_process_self();
63     
64     MC_SET_RAW_MEM;
65     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
66     
67     trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
68     xbt_free(type_str);
69
70     trans->type = mc_random ;
71     trans->process = p;
72     trans->min = min;
73     trans->max = max;
74     trans->current_value = min;
75     
76     /* Push it onto the enabled transitions set of the current state */
77     current_state = (mc_state_t) 
78       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
79     xbt_setset_set_insert(current_state->created_transitions, trans);
80     xbt_setset_set_insert(current_state->transitions, trans);
81     MC_UNSET_RAW_MEM;
82   }
83 }
84
85 /** 
86  * \brief Associate a communication to a transition
87  * \param trans The transition
88  * \param comm The communication
89  */
90 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
91 {
92   if(trans)
93     trans->comm = comm;
94   return;
95 }
96
97 /**
98  * \brief Deletes a transition
99  * \param trans The transition to be deleted
100  */
101 void MC_transition_delete(mc_transition_t trans)
102 {
103   xbt_free(trans->name);
104   xbt_free(trans);
105 }
106
107 /**
108  * \brief Determine if two transitions are dependent
109  * \param t1 a transition
110  * \param t2 a transition
111  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
112  */
113 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
114 {
115   /* The semantics of SIMIX network operations implies that ONLY transitions 
116      of the same type, in the same rendez-vous point, and from different processes
117      are dependant, except wait transitions that are always independent */
118   if(t1->process == t2->process) 
119     return FALSE;
120
121   if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
122     return TRUE;
123
124   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
125     return TRUE;
126
127   if(t1->type == mc_wait && t2->type == mc_wait 
128      && t1->comm->src_buff != NULL
129      && t1->comm->dst_buff != NULL
130      && t2->comm->src_buff != NULL
131      && t2->comm->dst_buff != NULL
132      && (   t1->comm->dst_buff == t2->comm->src_buff
133          || t1->comm->dst_buff == t2->comm->dst_buff
134          || t2->comm->dst_buff == t1->comm->src_buff))
135     return TRUE;
136   
137   return FALSE;
138 }