Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : new examples (with tesh) for verification of liveness properties...
[simgrid.git] / examples / msg / mc / bugged3.c
1 /* Copyright (c) 2012. 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
8 /**************** Shared buffer between asynchronous receives *****************/
9 /* Server process assumes that the data from the second communication comm2   */
10 /* will overwrite the one from the first communication, because of the order  */
11 /* of the wait calls. This is not true because data copy can be triggered by  */
12 /* a call to wait on the other end of the communication (client).             */
13 /* NOTE that the communications use different mailboxes, but they share the   */
14 /* same buffer for reception (task1).                                         */
15 /******************************************************************************/
16
17 #include <msg/msg.h>
18 #include <simgrid/modelchecker.h>
19
20 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example");
21
22 int server(int argc, char *argv[]);
23 int client(int argc, char *argv[]);
24
25 int server(int argc, char *argv[])
26 {
27   msg_task_t task1;
28   long val1;
29   msg_comm_t comm1, comm2;
30
31   comm1 = MSG_task_irecv(&task1, "mymailbox1");
32   comm2 = MSG_task_irecv(&task1, "mymailbox2");
33   MSG_comm_wait(comm1, -1);
34   MSG_comm_wait(comm2, -1);
35
36   val1 = (long) MSG_task_get_data(task1);
37   XBT_INFO("Received %lu", val1);
38
39   MC_assert(val1 == 2);
40
41   XBT_INFO("OK");
42   return 0;
43 }
44
45 int client(int argc, char *argv[])
46 {
47   msg_comm_t comm;
48   char *mbox;
49   msg_task_t task1 =
50       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
51
52   mbox = bprintf("mymailbox%s", argv[1]);
53
54   XBT_INFO("Send %d!", atoi(argv[1]));
55   comm = MSG_task_isend(task1, mbox);
56   MSG_comm_wait(comm, -1);
57
58   xbt_free(mbox);
59
60   return 0;
61 }
62
63 int main(int argc, char *argv[])
64 {
65   MSG_init(&argc, argv);
66
67   MSG_create_environment("platform.xml");
68
69   MSG_function_register("server", server);
70
71   MSG_function_register("client", client);
72
73   MSG_launch_application("deploy_bugged3.xml");
74
75   MSG_main();
76
77   return 0;
78 }