Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid
[simgrid.git] / examples / smpi / mc / bugged1_liveness.c
1 /***************** Centralized Mutual Exclusion Algorithm *********************/
2 /* This example implements a centralized mutual exclusion algorithm.          */
3 /* Bug : CS requests of process 1 not satisfied                                      */
4 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
5 /******************************************************************************/
6
7 #include <stdio.h>
8 #include <mpi.h>
9 #include <simgrid/modelchecker.h>
10
11 #define GRANT_TAG 0
12 #define REQUEST_TAG 1
13 #define RELEASE_TAG 2
14
15 int r, cs;
16
17 static int predR(){
18   return r;
19 }
20
21 static int predCS(){
22   return cs;
23 }
24
25
26 int main(int argc, char **argv){
27
28   int err, size, rank;
29   int recv_buff;
30   MPI_Status status;
31   int CS_used = 0;
32   xbt_dynar_t requests = xbt_dynar_new(sizeof(int), NULL);
33   
34   /* Initialize MPI */
35   err = MPI_Init(&argc, &argv);
36   if(err !=  MPI_SUCCESS){
37     printf("MPI initialization failed !\n");
38     exit(1);
39   }
40
41   MC_automaton_new_propositional_symbol("r", &predR);
42   MC_automaton_new_propositional_symbol("cs", &predCS);
43
44   MC_ignore(&(status.count), sizeof(status.count));
45
46   /* Get number of processes */
47   err = MPI_Comm_size(MPI_COMM_WORLD, &size);
48   /* Get id of this process */
49   err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);
50
51   if(rank == 0){ /* Coordinator */
52     while(1){
53       MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
54       if(status.MPI_TAG == REQUEST_TAG){
55         if(CS_used){
56           printf("CS already used.\n");
57           xbt_dynar_push(requests, &recv_buff);
58         }else{
59           if(recv_buff != 1){
60             printf("CS idle. Grant immediatly.\n");
61             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
62             CS_used = 1;
63           }
64         }
65       }else{
66         if(!xbt_dynar_is_empty(requests)){
67           printf("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
68           xbt_dynar_pop(requests, &recv_buff);
69           if(recv_buff != 1){
70             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
71             CS_used = 1;
72           }else{
73             xbt_dynar_push(requests, &recv_buff);
74           }
75         }else{
76           printf("CS release. Resource now idle.\n");
77           CS_used = 0;
78         }
79       }
80     }
81   }else{ /* Client */
82     while(1){
83       printf("%d asks the request.\n", rank);
84       MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
85       if(rank == 1){
86         r = 1;
87         cs = 0;
88       }
89       MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
90       if(status.MPI_TAG == GRANT_TAG && rank == 1){
91         cs = 1;
92         r = 0;
93       }
94       printf("%d got the answer. Release it.\n", rank);
95       MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
96       if(rank == 1){
97         r = 0;
98         cs = 0;
99       }
100     }
101   }
102
103   MPI_Finalize();
104
105   return 0;
106 }