Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : add commande line in comment to run the example
[simgrid.git] / examples / smpi / mc / bugged1_liveness.c
1 /* Copyright (c) 2013-2014. 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" "$@" ../../../smpi_script/bin/smpirun -hostfile hostfile_bugged1_liveness -platform ../../platforms/cluster.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/reduction:none --cfg=model-check/property:promela_bugged1_liveness --cfg=smpi/send_is_detached_thres:0 --cfg=contexts/stack_size:128 --cfg=model-check/visited:100000 --cfg=model-check/max_depth:100000 ./bugged1_liveness */
15
16 #include <stdio.h>
17 #include <mpi.h>
18 #include <simgrid/modelchecker.h>
19
20 #define GRANT_TAG 0
21 #define REQUEST_TAG 1
22 #define RELEASE_TAG 2
23
24 int r, cs;
25
26 static int predR(){
27   return r;
28 }
29
30 static int predCS(){
31   return cs;
32 }
33
34
35 int main(int argc, char **argv){
36
37   int err, size, rank;
38   int recv_buff;
39   MPI_Status status;
40   int CS_used = 0;
41   xbt_dynar_t requests = xbt_dynar_new(sizeof(int), NULL);
42   
43   /* Initialize MPI */
44   err = MPI_Init(&argc, &argv);
45   if(err !=  MPI_SUCCESS){
46     printf("MPI initialization failed !\n");
47     exit(1);
48   }
49
50   MC_automaton_new_propositional_symbol("r", &predR);
51   MC_automaton_new_propositional_symbol("cs", &predCS);
52
53   MC_ignore(&(status.count), sizeof(status.count));
54
55   /* Get number of processes */
56   err = MPI_Comm_size(MPI_COMM_WORLD, &size);
57   /* Get id of this process */
58   err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);
59
60   if(rank == 0){ /* Coordinator */
61     while(1){
62       MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
63       if(status.MPI_TAG == REQUEST_TAG){
64         if(CS_used){
65           printf("CS already used.\n");
66           xbt_dynar_push(requests, &recv_buff);
67         }else{
68           if(recv_buff != size - 1){
69             printf("CS idle. Grant immediatly.\n");
70             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
71             CS_used = 1;
72           }
73         }
74       }else{
75         if(!xbt_dynar_is_empty(requests)){
76           printf("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
77           xbt_dynar_shift(requests, &recv_buff);
78           if(recv_buff != size - 1){
79             MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
80             CS_used = 1;
81           }else{
82             xbt_dynar_push(requests, &recv_buff);
83             CS_used = 0;
84           }
85         }else{
86           printf("CS release. Resource now idle.\n");
87           CS_used = 0;
88         }
89       }
90     }
91   }else{ /* Client */
92     while(1){
93       printf("%d asks the request.\n", rank);
94       MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
95       if(rank == size - 1){
96         r = 1;
97         cs = 0;
98       }
99       MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
100       if(status.MPI_TAG == GRANT_TAG && rank == size - 1){
101         cs = 1;
102         r = 0;
103       }
104       printf("%d got the answer. Release it.\n", rank);
105       MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
106       if(rank == size - 1){
107         r = 0;
108         cs = 0;
109       }
110     }
111   }
112
113   MPI_Finalize();
114
115   return 0;
116 }