Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : function to compare propositional symbol values
[simgrid.git] / examples / msg / mc / example_liveness_with_cycle.c
1 /***************** Centralized Mutual Exclusion Algorithm *********************/
2 /* This example implements a centralized mutual exclusion algorithm.          */
3 /* There is no bug on it, it is just provided to test the state space         */
4 /* reduction of DPOR.                                                         */
5 /******************************************************************************/
6
7 #include "msg/msg.h"
8 #include "mc/mc.h"
9 #include "xbt/automaton.h"
10 #include "xbt/automatonparse_promela.h"
11 #include "example_liveness_with_cycle.h"
12 #include "y.tab.c"
13
14 #define AMOUNT_OF_CLIENTS 2
15 #define CS_PER_PROCESS 2
16
17 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
18
19 int p=0; 
20 int q=0;
21
22 int predP(){
23   return p;
24 }
25
26 int predQ(){
27   return q;
28 }
29
30
31 //xbt_dynar_t listeVars -> { void *ptr; int size (nb octets); } => liste de structures 
32 //=> parcourir la liste et comparer les contenus de chaque pointeur
33
34 int coordinator(int argc, char *argv[])
35 {
36   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
37   int CS_used = 0;              // initially the CS is idle
38   int todo = AMOUNT_OF_CLIENTS * CS_PER_PROCESS;        // amount of releases we are expecting
39   while (todo > 0) {
40     m_task_t task = NULL;
41     MSG_task_receive(&task, "coordinator");
42     const char *kind = MSG_task_get_name(task); //is it a request or a release?
43     if (!strcmp(kind, "request")) {     // that's a request
44       char *req = MSG_task_get_data(task);
45       //XBT_INFO("Req %s", req);
46       if (CS_used) {            // need to push the request in the vector
47         XBT_INFO("CS already used. Queue the request");
48         xbt_dynar_push(requests, &req);
49       } else {                  // can serve it immediatly
50         XBT_INFO("CS idle. Grant immediatly");
51         if(strcmp(req, "1") == 0){
52           m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
53           MSG_task_send(answer, req);
54           CS_used = 1;
55         }else{
56           m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL);
57           MSG_task_send(answer, req);
58         }
59       }
60     } else {                    // that's a release. Check if someone was waiting for the lock
61       if (xbt_dynar_length(requests) > 0) {
62         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
63               xbt_dynar_length(requests));
64         char *req ;
65         xbt_dynar_pop(requests, &req);
66         if(strcmp(req, "1") == 0){
67           MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
68           todo--;
69         }else{
70           MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
71           todo--;
72         }
73       } else {                  // nobody wants it
74         XBT_INFO("CS release. resource now idle");
75         CS_used = 0;
76         todo--;
77       }
78     }
79     MSG_task_destroy(task);
80   }
81   XBT_INFO("Received all releases, quit now"); 
82   return 0;
83 }
84
85 int client(int argc, char *argv[])
86 {
87   int my_pid = MSG_process_get_PID(MSG_process_self());
88   // use my pid as name of mailbox to contact me
89   char *my_mailbox = bprintf("%s", argv[1]);
90   // request the CS 2 times, sleeping a bit in between
91   int i;
92   for (i = 0; i < CS_PER_PROCESS; i++) {
93     XBT_INFO("Ask the request");
94     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
95                   "coordinator");
96     if(strcmp(my_mailbox, "2") == 0){
97       p = 1;
98       q = 0;
99     }
100     // wait the answer
101     m_task_t grant = NULL;
102     MSG_task_receive(&grant, my_mailbox);
103     const char *kind = MSG_task_get_name(grant);
104     if(!strcmp(kind, "grant")){
105       if(strcmp(my_mailbox, "2") == 0){
106         q = 1;
107         p = 0;
108       }
109         //answers ++;
110       MSG_task_destroy(grant);
111       XBT_INFO("got the answer. Sleep a bit and release it");
112       MSG_process_sleep(1);
113       MSG_task_send(MSG_task_create("release", 0, 1000,NULL ),
114                     "coordinator");
115     }
116     
117     MSG_process_sleep(my_pid);
118
119   }
120
121   //XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox);
122   return 0;
123 }
124
125 int main(int argc, char *argv[])
126 {
127   init();
128   yyparse();
129   automaton = get_automaton();
130   xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); 
131   ps = xbt_new_propositional_symbol(automaton,"q", &predQ); 
132   
133   MSG_global_init(&argc, argv);
134   MSG_create_environment("../msg_platform.xml");
135   MSG_function_register("coordinator", coordinator);
136   MSG_function_register("client", client);
137   MSG_launch_application("deploy_mutex2.xml");
138   MSG_main_liveness_stateless(automaton);
139   //MSG_main();
140   
141   return 0;
142 }