examples/smpi/mc/bugged1_liveness.c

   1 /* Copyright (c) 2013-2015. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 /***************** Centralized Mutual Exclusion Algorithm *********************/
   8 /* This example implements a centralized mutual exclusion algorithm.          */
   9 /* Bug : CS requests of process 1 not satisfied                                      */
  10 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
  11 /******************************************************************************/
  12
  13 /* Run :
  14   /usr/bin/time -f "clock:%e user:%U sys:%S swapped:%W exitval:%x max:%Mk" "$@" \
  15     ../../../smpi_script/bin/smpirun -hostfile hostfile_bugged1_liveness -platform ../../platforms/cluster.xml \
  16     --cfg=contexts/factory:ucontext --cfg=model-check/reduction:none \
  17     --cfg=model-check/property:promela_bugged1_liveness --cfg=smpi/send-is-detached-thresh:0 \
  18     --cfg=contexts/stack-size:128 --cfg=model-check/visited:100000 --cfg=model-check/max-depth:100000 ./bugged1_liveness
  19 */
  20
  21 #include <stdio.h>
  22 #include <mpi.h>
  23 #include <simgrid/modelchecker.h>
  24
  25 #define GRANT_TAG 0
  26 #define REQUEST_TAG 1
  27 #define RELEASE_TAG 2
  28
  29 int r, cs;
  30
  31 int main(int argc, char **argv){
  32   int size;
  33   int rank;
  34   int recv_buff;
  35   MPI_Status status;
  36   xbt_dynar_t requests = xbt_dynar_new(sizeof(int), NULL);
  37
  38   /* Initialize MPI */
  39   int err = MPI_Init(&argc, &argv);
  40   if(err !=  MPI_SUCCESS){
  41     printf("MPI initialization failed !\n");
  42     exit(1);
  43   }
  44
  45   MC_automaton_new_propositional_symbol_pointer("r", &r);
  46   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
  47
  48   MC_ignore(&(status.count), sizeof(status.count));
  49
  50   /* Get number of processes */
  51   MPI_Comm_size(MPI_COMM_WORLD, &size);
  52   /* Get id of this process */
  53   MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  54
  55   if(rank == 0){ /* Coordinator */
  56     int CS_used = 0;
  57     while(1){
  58       MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  59       if(status.MPI_TAG == REQUEST_TAG){
  60         if(CS_used){
  61           printf("CS already used.\n");
  62           xbt_dynar_push(requests, &recv_buff);
  63         }else{
  64           if(recv_buff != size - 1){
  65             printf("CS idle. Grant immediatly.\n");
  66             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
  67             CS_used = 1;
  68           }
  69         }
  70       }else{
  71         if(!xbt_dynar_is_empty(requests)){
  72           printf("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
  73           xbt_dynar_shift(requests, &recv_buff);
  74           if(recv_buff != size - 1){
  75             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
  76             CS_used = 1;
  77           }else{
  78             xbt_dynar_push(requests, &recv_buff);
  79             CS_used = 0;
  80           }
  81         }else{
  82           printf("CS release. Resource now idle.\n");
  83           CS_used = 0;
  84         }
  85       }
  86     }
  87   }else{ /* Client */
  88     while(1){
  89       printf("%d asks the request.\n", rank);
  90       MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
  91       if(rank == size - 1){
  92         r = 1;
  93         cs = 0;
  94       }
  95       MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  96       if(status.MPI_TAG == GRANT_TAG && rank == size - 1){
  97         cs = 1;
  98         r = 0;
  99       }
 100       printf("%d got the answer. Release it.\n", rank);
 101       MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
 102       if(rank == size - 1){
 103         r = 0;
 104         cs = 0;
 105       }
 106     }
 107   }
 108
 109   MPI_Finalize();
 110
 111   return 0;
 112 }