Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : update bugged mutual exclusion algorithm
[simgrid.git] / examples / msg / mc / bugged1_liveness.c
1 /***************** Centralized Mutual Exclusion Algorithm *********************/
2 /* This example implements a centralized mutual exclusion algorithm.          */
3 /* Bug : 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 "bugged1_liveness.h"
11
12 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
13
14 int r=0; 
15 int cs=0;
16
17 int predR(){
18   return r;
19 }
20
21 int predCS(){
22   return cs;
23 }
24
25
26 int coordinator(int argc, char *argv[])
27 {
28
29   int CS_used = 0;   
30   msg_task_t task = NULL, answer = NULL; 
31   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
32   char *req;
33
34   while(1){  
35     MSG_task_receive(&task, "coordinator");
36     const char *kind = MSG_task_get_name(task); 
37     if (!strcmp(kind, "request")) {    
38       req = MSG_task_get_data(task);
39       if (CS_used) {           
40         XBT_INFO("CS already used. Queue the request.");
41         xbt_dynar_push(requests, &req);
42       } else {               
43         if(strcmp(req, "1") != 0){
44           XBT_INFO("CS idle. Grant immediatly");
45           answer = MSG_task_create("grant", 0, 1000, NULL);
46           MSG_task_send(answer, req);
47           CS_used = 1;
48           answer = NULL;
49         }
50       }
51     } else {      
52       if (!xbt_dynar_is_empty(requests)) {
53         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
54         xbt_dynar_shift(requests, &req);
55         if(strcmp(req, "1") != 0){
56           MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
57         }else{
58           xbt_dynar_push(requests, &req);
59           CS_used = 0;
60         }
61       }else{
62         XBT_INFO("CS release. resource now idle");
63         CS_used = 0;
64       }
65     }
66     MSG_task_destroy(task);
67     task = NULL;
68     kind = NULL;
69     req = NULL;
70   }
71  
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 = xbt_strdup(argv[1]);
80   msg_task_t grant = NULL, release = NULL;
81     
82   while(1){
83     XBT_INFO("Ask the request");
84     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
85
86     if(strcmp(my_mailbox, "1") == 0){
87       r = 1;
88       cs = 0;
89       XBT_INFO("Propositions changed : r=1, cs=0");
90     }
91
92     MSG_task_receive(&grant, my_mailbox);
93     const char *kind = MSG_task_get_name(grant);
94
95     if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){
96       cs = 1;
97       r = 0;
98       XBT_INFO("Propositions changed : r=0, cs=1");
99     }
100
101     MSG_task_destroy(grant);
102     grant = NULL;
103     kind = NULL;
104
105     XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
106
107     MSG_process_sleep(1);
108
109     release = MSG_task_create("release", 0, 1000, NULL);
110     MSG_task_send(release, "coordinator");
111
112     release = NULL;
113
114     MSG_process_sleep(my_pid);
115     
116     if(strcmp(my_mailbox, "1") == 0){
117       cs=0;
118       r=0;
119       XBT_INFO("Propositions changed : r=0, cs=0");
120     }
121     
122   }
123
124   return 0;
125 }
126
127 int main(int argc, char *argv[])
128 {
129
130   MSG_init(&argc, argv);
131
132   char **options = &argv[1];
133
134   MSG_config("model-check/property","promela_bugged1_liveness");
135   MC_automaton_new_propositional_symbol("r", &predR);
136   MC_automaton_new_propositional_symbol("cs", &predCS);
137
138   const char* platform_file = options[0];
139   const char* application_file = options[1];
140   
141   MSG_create_environment(platform_file);
142   MSG_function_register("coordinator", coordinator);
143   MSG_function_register("client", client);
144   MSG_launch_application(application_file);
145   MSG_main();
146
147   return 0;
148 }