examples/msg/mc/bugged1_for_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 #define AMOUNT_OF_CLIENTS 2
  15 #define CS_PER_PROCESS 2
  16
  17 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
  18
  19
  20 int r=0;
  21 int cs=0;
  22
  23 int predR(){
  24   return r;
  25 }
  26
  27 int predCS(){
  28   return cs;
  29 }
  30
  31
  32 int coordinator(int argc, char *argv[])
  33 {
  34   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
  35   int CS_used = 0;              // initially the CS is idle
  36   int todo = AMOUNT_OF_CLIENTS * CS_PER_PROCESS;        // amount of releases we are expecting
  37   while (todo > 0) {
  38     m_task_t task = NULL;
  39     MSG_task_receive(&task, "coordinator");
  40     const char *kind = MSG_task_get_name(task); //is it a request or a release?
  41     if (!strcmp(kind, "request")) {     // that's a request
  42       char *req = MSG_task_get_data(task);
  43       if (CS_used) {            // need to push the request in the vector
  44         XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
  45         xbt_dynar_push(requests, &req);
  46       } else {                  // can serve it immediatly
  47         if(strcmp(req, "2") == 0){
  48           m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
  49           MSG_task_send(answer, req);
  50           CS_used = 1;
  51           XBT_INFO("CS idle. Grant immediatly");
  52         }
  53       }
  54     } else {                    // that's a release. Check if someone was waiting for the lock
  55       if (xbt_dynar_length(requests) > 0) {
  56         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
  57         char *req ;
  58         xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);
  59         if(strcmp(req, "2") == 0){
  60           xbt_dynar_pop(requests, &req);
  61           MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
  62           todo--;
  63         }else{
  64           xbt_dynar_pop(requests, &req);
  65           MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
  66           CS_used = 0;
  67           todo--;
  68         }
  69       } else {                  // nobody wants it
  70         XBT_INFO("CS release. resource now idle");
  71         CS_used = 0;
  72         todo--;
  73       }
  74     }
  75     MSG_task_destroy(task);
  76   }
  77   XBT_INFO("Received all releases, quit now");
  78   return 0;
  79 }
  80
  81 int client(int argc, char *argv[])
  82 {
  83   int my_pid = MSG_process_get_PID(MSG_process_self());
  84
  85   char *my_mailbox = bprintf("%s", argv[1]);
  86   int i;
  87
  88   // request the CS (CS_PER_PROCESS times), sleeping a bit in between
  89   for (i = 0; i < CS_PER_PROCESS; i++) {
  90
  91     XBT_INFO("Ask the request");
  92     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
  93
  94     if(strcmp(my_mailbox, "1") == 0){
  95       r = 1;
  96       cs = 0;
  97       XBT_DEBUG("Propositions changed : r=1, cs=0");
  98     }
  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
 105     if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){
 106       cs = 1;
 107       r = 0;
 108       XBT_DEBUG("Propositions changed : r=0, cs=1");
 109     }
 110
 111
 112     MSG_task_destroy(grant);
 113     XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
 114     MSG_process_sleep(1);
 115     MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
 116
 117     MSG_process_sleep(my_pid);
 118
 119     if(strcmp(my_mailbox, "1") == 0){
 120       cs=0;
 121       r=0;
 122       XBT_DEBUG("Propositions changed : r=0, cs=0");
 123     }
 124
 125   }
 126
 127   XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox);
 128   return 0;
 129 }
 130
 131 int main(int argc, char *argv[])
 132 {
 133   init();
 134   yyparse();
 135   automaton = get_automaton();
 136   xbt_new_propositional_symbol(automaton,"r", &predR);
 137   xbt_new_propositional_symbol(automaton,"cs", &predCS);
 138
 139   MSG_global_init(&argc, argv);
 140   MSG_create_environment("../msg_platform.xml");
 141   MSG_function_register("coordinator", coordinator);
 142   MSG_function_register("client", client);
 143   MSG_launch_application("deploy_bugged1_liveness.xml");
 144   MSG_main_liveness(automaton, argv[0]);
 145
 146   return 0;
 147 }