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