examples/msg/mc/centralized_liveness.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   int CS_used = 0;              // initially the CS is idle
  26
  27   while (1) {
  28     m_task_t task = NULL;
  29     MSG_task_receive(&task, "coordinator");
  30     const char *kind = MSG_task_get_name(task); //is it a request or a release?
  31     if (!strcmp(kind, "request")) {     // that's a request
  32       char *req = MSG_task_get_data(task);
  33       if (CS_used) {
  34         XBT_INFO("CS already used.");
  35   m_task_t answer = MSG_task_create("not grant", 0, 1000, NULL);
  36         MSG_task_send(answer, 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       XBT_INFO("CS release. resource now idle");
  45       CS_used = 0;
  46     }
  47     MSG_task_destroy(task);
  48   }
  49
  50   return 0;
  51 }
  52
  53 int client(int argc, char *argv[])
  54 {
  55   int my_pid = MSG_process_get_PID(MSG_process_self());
  56   char *my_mailbox = bprintf("%s", argv[1]);
  57   const char* kind;
  58
  59   while(1){
  60
  61     XBT_INFO("Client (%s) asks the request", my_mailbox);
  62     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
  63                   "coordinator");
  64     // wait the answer
  65     m_task_t answer = NULL;
  66     MSG_task_receive(&answer, my_mailbox);
  67
  68     kind = MSG_task_get_name(answer);
  69
  70     if (!strcmp(kind, "grant")) {
  71
  72       XBT_INFO("Client (%s) got the answer (grant). Sleep a bit and release it", my_mailbox);
  73
  74       if(!strcmp(my_mailbox, "1"))
  75   cs = 1;
  76
  77       /*MSG_process_sleep(my_pid);
  78       MSG_task_send(MSG_task_create("release", 0, 1000, NULL),
  79         "coordinator");
  80         XBT_INFO("Client (%s) releases the CS", my_mailbox);
  81
  82       if(!strcmp(my_mailbox, "1"))
  83   cs = 0;*/
  84
  85     }else{
  86
  87       XBT_INFO("Client (%s) got the answer (not grant). Try again", my_mailbox);
  88
  89     }
  90
  91     MSG_task_destroy(answer);
  92
  93     MSG_process_sleep(my_pid);
  94   }
  95
  96   return 0;
  97 }
  98
  99 int main(int argc, char *argv[])
 100 {
 101
 102   MC_automaton_load("promela_centralized_liveness");
 103   MC_automaton_new_propositional_symbol("cs", &predCS);
 104
 105   MSG_init(&argc, argv);
 106   MSG_create_environment("../msg_platform.xml");
 107   MSG_function_register("coordinator", coordinator);
 108   MSG_function_register("client", client);
 109   MSG_launch_application("deploy_centralized_liveness.xml");
 110   MSG_main_liveness();
 111
 112   return 0;
 113
 114 }