examples/smpi/mc/bugged1_liveness.c

   1 /* Copyright (c) 2013-2021. 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_backbone.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 #include <xbt/dynar.h>
  25
  26 #define GRANT_TAG 0
  27 #define REQUEST_TAG 1
  28 #define RELEASE_TAG 2
  29
  30 int r;
  31 int cs;
  32
  33 int main(int argc, char **argv){
  34   int size;
  35   int rank;
  36   int recv_buff;
  37   MPI_Status status;
  38   xbt_dynar_t requests = xbt_dynar_new(sizeof(int), NULL);
  39
  40   /* Initialize MPI */
  41   int err = MPI_Init(&argc, &argv);
  42   if(err !=  MPI_SUCCESS){
  43     printf("MPI initialization failed !\n");
  44     exit(1);
  45   }
  46
  47   MC_automaton_new_propositional_symbol_pointer("r", &r);
  48   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
  49
  50   MC_ignore(&(status.count), sizeof(status.count));
  51
  52   /* Get number of processes */
  53   MPI_Comm_size(MPI_COMM_WORLD, &size);
  54   /* Get id of this process */
  55   MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  56
  57   if(rank == 0){ /* Coordinator */
  58     int CS_used = 0;
  59     while(1){
  60       MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  61       if(status.MPI_TAG == REQUEST_TAG){
  62         if(CS_used){
  63           printf("CS already used.\n");
  64           xbt_dynar_push(requests, &recv_buff);
  65         }else{
  66           if(recv_buff != size - 1){
  67             printf("CS idle. Grant immediately.\n");
  68             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
  69             CS_used = 1;
  70           }
  71         }
  72       }else{
  73         if(!xbt_dynar_is_empty(requests)){
  74           printf("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
  75           xbt_dynar_shift(requests, &recv_buff);
  76           if(recv_buff != size - 1){
  77             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
  78             CS_used = 1;
  79           }else{
  80             xbt_dynar_push(requests, &recv_buff);
  81             CS_used = 0;
  82           }
  83         }else{
  84           printf("CS release. Resource now idle.\n");
  85           CS_used = 0;
  86         }
  87       }
  88     }
  89   }else{ /* Client */
  90     while(1){
  91       printf("%d asks the request.\n", rank);
  92       MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
  93       if(rank == size - 1){
  94         r = 1;
  95         cs = 0;
  96       }
  97       MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
  98       if(status.MPI_TAG == GRANT_TAG && rank == size - 1){
  99         cs = 1;
 100         r = 0;
 101       }
 102       printf("%d got the answer. Release it.\n", rank);
 103       MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
 104       if(rank == size - 1){
 105         r = 0;
 106         cs = 0;
 107       }
 108     }
 109   }
 110
 111   MPI_Finalize();
 112
 113   return 0;
 114 }