Logo AND Algorithmique Numérique Distribuée

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