examples/msg/mc/centralized_liveness_deadlock.c

   1 /***************** Centralized Mutual Exclusion Algorithm *********************/
   2 /* This example implements a centralized mutual exclusion algorithm.          */
   3 /* LTL property checked : !(GFcs)                                            */
   4 /******************************************************************************/
   5
   6 #include "msg/msg.h"
   7 #include "mc/mc.h"
   8 #include "xbt/automaton.h"
   9 #include "centralized_liveness.h"
  10
  11 XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages");
  12
  13 int cs = 0;
  14
  15 int predCS(){
  16   return cs;
  17 }
  18
  19
  20 int coordinator(int argc, char **argv);
  21 int client(int argc, char **argv);
  22
  23 int coordinator(int argc, char *argv[])
  24 {
  25   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
  26   int CS_used = 0;              // initially the CS is idle
  27
  28   while (1) {
  29     m_task_t task = NULL;
  30     MSG_task_receive(&task, "coordinator");
  31     const char *kind = MSG_task_get_name(task); //is it a request or a release?
  32     if (!strcmp(kind, "request")) {     // that's a request
  33       char *req = MSG_task_get_data(task);
  34       if (CS_used) {            // need to push the request in the vector
  35         XBT_INFO("CS already used. Queue the request");
  36         xbt_dynar_push(requests, &req);
  37       } else {                  // can serve it immediatly
  38         XBT_INFO("CS idle. Grant immediatly");
  39         m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
  40         MSG_task_send(answer, req);
  41         CS_used = 1;
  42       }
  43     } else {                    // that's a release. Check if someone was waiting for the lock
  44       if (!xbt_dynar_is_empty(requests)) {
  45         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
  46               xbt_dynar_length(requests));
  47         char *req;
  48         xbt_dynar_pop(requests, &req);
  49         MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
  50       } else {                  // nobody wants it
  51         XBT_INFO("CS release. resource now idle");
  52         CS_used = 0;
  53       }
  54     }
  55     MSG_task_destroy(task);
  56   }
  57
  58   return 0;
  59 }
  60
  61 int client(int argc, char *argv[])
  62 {
  63   int my_pid = MSG_process_get_PID(MSG_process_self());
  64   char *my_mailbox = bprintf("%s", argv[1]);
  65
  66   while(1){
  67
  68     XBT_INFO("Client (%s) asks the request", my_mailbox);
  69     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
  70                   "coordinator");
  71     // wait the answer
  72     m_task_t grant = NULL;
  73     MSG_task_receive(&grant, my_mailbox);
  74
  75     MSG_task_destroy(grant);
  76     XBT_INFO("Client (%s) got the answer. Sleep a bit and release it", my_mailbox);
  77
  78     if(!strcmp(my_mailbox, "1"))
  79       cs = 1;
  80
  81     /*MSG_process_sleep(my_pid);
  82     MSG_task_send(MSG_task_create("release", 0, 1000, NULL),
  83                   "coordinator");
  84     XBT_INFO("Client (%s) releases the CS", my_mailbox);
  85
  86     if(!strcmp(my_mailbox, "1"))
  87     cs = 0;*/
  88
  89     MSG_process_sleep(my_pid);
  90
  91   }
  92
  93   return 0;
  94 }
  95
  96 int main(int argc, char *argv[])
  97 {
  98
  99   MC_automaton_load("promela_centralized_liveness");
 100   MC_automaton_new_propositional_symbol("cs", &predCS);
 101
 102   MSG_init(&argc, argv);
 103   MSG_create_environment("../msg_platform.xml");
 104   MSG_function_register("coordinator", coordinator);
 105   MSG_function_register("client", client);
 106   MSG_launch_application("deploy_centralized_liveness.xml");
 107   MSG_main_liveness();
 108
 109   return 0;
 110
 111 }