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 int p=0;
  20 int q=0;
  21
  22 int predP(){
  23   return p;
  24 }
  25
  26 int predQ(){
  27   return q;
  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       //XBT_INFO("Req %s", req);
  42       if (CS_used) {            // need to push the request in the vector
  43         XBT_INFO("CS already used. Queue the request");
  44         xbt_dynar_push(requests, &req);
  45       } else {                  // can serve it immediatly
  46         XBT_INFO("CS idle. Grant immediatly");
  47         if(strcmp(req, "1") == 0){
  48           m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
  49           MSG_task_send(answer, req);
  50           CS_used = 1;
  51           }else{
  52           m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL);
  53           MSG_task_send(answer, req);
  54         }
  55
  56       }
  57     } else {                    // that's a release. Check if someone was waiting for the lock
  58       if (xbt_dynar_length(requests) > 0) {
  59         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
  60               xbt_dynar_length(requests));
  61         char *req;
  62         if(strcmp(req, "1") == 0){
  63           xbt_dynar_pop(requests, &req);
  64           MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
  65           todo--;
  66         }else{
  67           xbt_dynar_pop(requests, &req);
  68           MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
  69           todo--;
  70         }
  71       } else {                  // nobody wants it
  72         XBT_INFO("CS release. resource now idle");
  73         CS_used = 0;
  74         todo--;
  75       }
  76     }
  77     MSG_task_destroy(task);
  78   }
  79   XBT_INFO("Received all releases, quit now");
  80   return 0;
  81 }
  82
  83 int client(int argc, char *argv[])
  84 {
  85   int my_pid = MSG_process_get_PID(MSG_process_self());
  86   // use my pid as name of mailbox to contact me
  87   char *my_mailbox = bprintf("%s", argv[1]);
  88   // request the CS 2 times, sleeping a bit in between
  89   int i;
  90   for (i = 0; i < CS_PER_PROCESS; i++) {
  91     p = 1;
  92     q = 0;
  93     XBT_INFO("Ask the request");
  94     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
  95                   "coordinator");
  96     if(strcmp(my_mailbox, "1") == 0){
  97       p = 1;
  98       q = 0;
  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     if(!strcmp(kind, "grant")){
 105       if(strcmp(my_mailbox, "2") == 0){
 106         q = 1;
 107         p = 0;
 108       }
 109         //answers ++;
 110       MSG_task_destroy(grant);
 111       XBT_INFO("got the answer. Sleep a bit and release it");
 112       MSG_process_sleep(1);
 113       MSG_task_send(MSG_task_create("release", 0, 1000,NULL ),
 114                     "coordinator");
 115     }else{
 116       MSG_task_destroy(grant);
 117       XBT_INFO("Negative answer");
 118       MSG_process_sleep(1);
 119       MSG_task_send(MSG_task_create("notrelease", 0, 1000,NULL ),
 120                     "coordinator");
 121     }
 122
 123     MSG_process_sleep(my_pid);
 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_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP);
 137   ps = xbt_new_propositional_symbol(automaton,"q", &predQ);
 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_mutex2.xml");
 144   MSG_main_liveness_stateless(automaton);
 145   //MSG_main();
 146
 147   return 0;
 148 }