examples/smpi/mc/bugged1_liveness.c

   1 #include <stdio.h>
   2 #include <mpi.h>
   3 #include <simgrid/modelchecker.h>
   4
   5 #define GRANT_TAG 0
   6 #define REQUEST_TAG 1
   7 #define RELEASE_TAG 2
   8
   9 int r, cs;
  10
  11 static int predR(){
  12   return r;
  13 }
  14
  15 static int predCS(){
  16   return cs;
  17 }
  18
  19
  20 int main(int argc, char **argv){
  21
  22   //int i;
  23   int err, size, rank;
  24   int recv_buff;
  25   MPI_Status status;
  26   int CS_used = 0;
  27
  28   /* Initialize MPI */
  29   err = MPI_Init(&argc, &argv);
  30   if(err !=  MPI_SUCCESS){
  31     printf("MPI initialization failed !\n");
  32     exit(1);
  33   }
  34
  35   MC_automaton_new_propositional_symbol("r", &predR);
  36   MC_automaton_new_propositional_symbol("cs", &predCS);
  37
  38   MC_ignore(&(status.count), sizeof(status.count));
  39
  40   /* Get number of processes */
  41   err = MPI_Comm_size(MPI_COMM_WORLD, &size);
  42   /* Get id of this process */
  43   err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  44
  45   if(rank == 0){ /* Coordinator */
  46     //for(i=0; i<size-1; i++) {
  47     while(1){
  48       MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  49       if(status.MPI_TAG == REQUEST_TAG){
  50         if(CS_used){
  51           printf("CS already used.\n");
  52         }else{
  53           if(recv_buff != 1){
  54             printf("CS idle. Grant immediatly.\n");
  55             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
  56             CS_used = 1;
  57           }
  58         }
  59       }else{
  60         printf("CS release. Resource now idle.\n");
  61         CS_used = 0;
  62       }
  63     }
  64   }else{ /* Client */
  65     while(1){
  66       printf("%d asks the request.\n", rank);
  67       MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
  68       if(rank == 1){
  69         r = 1;
  70         cs = 0;
  71       }
  72       MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  73       if(status.MPI_TAG == GRANT_TAG && rank == 1){
  74         cs = 1;
  75         r = 0;
  76       }
  77       printf("%d got the answer. Release it.\n", rank);
  78       MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
  79       if(rank == 1){
  80         r = 0;
  81         cs = 0;
  82       }
  83     }
  84   }
  85
  86   MPI_Finalize();
  87
  88   return 0;
  89 }