Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
1e56dada33a5aeb8fa0159395f5098a8dd2e2c9b
[simgrid.git] / examples / msg / mc / bugged1_while_liveness.c
1 /***************** Centralized Mutual Exclusion Algorithm *********************/
2 /* This example implements a centralized mutual exclusion algorithm.          */
3 /* CS requests of client 1 not satisfied                                      */
4 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
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 "bugged1_liveness.h"
12 #include "y.tab.c"
13
14 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
15
16 int r=0; 
17 int cs=0;
18
19 int predR(){
20   return r;
21 }
22
23 int predCS(){
24   return cs;
25 }
26
27
28 int coordinator(int argc, char *argv[])
29 {
30   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
31   int CS_used = 0;              // initially the CS is idle
32   while (1) {
33     m_task_t task = NULL;
34     MSG_task_receive(&task, "coordinator");
35     const char *kind = MSG_task_get_name(task); //is it a request or a release?
36     if (!strcmp(kind, "request")) {     // that's a request
37       char *req = MSG_task_get_data(task);
38       if (CS_used) {            // need to push the request in the vector
39         XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
40         xbt_dynar_push(requests, &req);
41       } else {                  // can serve it immediatly
42         if(strcmp(req, "2") == 0){
43           m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
44           MSG_task_send(answer, req);
45           CS_used = 1;
46           XBT_INFO("CS idle. Grant immediatly");
47         }
48       }
49     } else {                    // that's a release. Check if someone was waiting for the lock
50       if (xbt_dynar_length(requests) > 0) {
51         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
52         char *req ;
53         xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);
54         if(strcmp(req, "2") == 0){
55           xbt_dynar_pop(requests, &req);
56           MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
57         }else{
58           xbt_dynar_pop(requests, &req);
59           MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
60           CS_used = 0;
61         }
62       } else {                  // nobody wants it
63         XBT_INFO("CS release. resource now idle");
64         CS_used = 0;
65       }
66     }
67     MSG_task_destroy(task);
68   }
69  
70   return 0;
71 }
72
73 int client(int argc, char *argv[])
74 {
75   int my_pid = MSG_process_get_PID(MSG_process_self());
76
77   char *my_mailbox = bprintf("%s", argv[1]);
78
79   // request the CS, sleeping a bit in between
80   while(1) {
81       
82     XBT_INFO("Ask the request");
83     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
84
85     if(strcmp(my_mailbox, "1") == 0){
86       r = 1;
87       cs = 0;
88       XBT_INFO("Propositions changed : r=1, cs=0");
89     }
90
91     // wait the answer
92     m_task_t grant = NULL;
93     MSG_task_receive(&grant, my_mailbox);
94     const char *kind = MSG_task_get_name(grant);
95
96     if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){
97       cs = 1;
98       r = 0;
99       XBT_INFO("Propositions changed : r=0, cs=1");
100     }
101
102
103     MSG_task_destroy(grant);
104     XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
105     MSG_process_sleep(1);
106     MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
107
108     MSG_process_sleep(my_pid);
109     
110     if(strcmp(my_mailbox, "1") == 0){
111       cs=0;
112       r=0;
113       XBT_INFO("Propositions changed : r=0, cs=0");
114     }
115     
116   }
117
118   return 0;
119 }
120
121 int main(int argc, char *argv[])
122 {
123   init();
124   yyparse();
125   automaton = get_automaton();
126   xbt_new_propositional_symbol(automaton,"r", &predR); 
127   xbt_new_propositional_symbol(automaton,"cs", &predCS); 
128   
129   MSG_global_init(&argc, argv);
130   MSG_create_environment("../msg_platform.xml");
131   MSG_function_register("coordinator", coordinator);
132   MSG_function_register("client", client);
133   MSG_launch_application("deploy_bugged1_liveness.xml");
134   MSG_main_liveness(automaton);
135
136   return 0;
137 }