Logo AND Algorithmique Numérique Distribuée

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