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 }