From 5ce5b5c91c7ed6031f502835a07124f7e38d91f2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 24 Feb 2014 18:44:02 +0100 Subject: [PATCH 1/1] model-checker : smpi examples for the communication pattern detection --- examples/smpi/CMakeLists.txt | 8 +++ examples/smpi/mc/hostfile_non_deterministic | 3 ++ examples/smpi/mc/hostfile_send_deterministic | 3 ++ examples/smpi/mc/non_deterministic.c | 54 ++++++++++++++++++++ examples/smpi/mc/send_deterministic.c | 50 ++++++++++++++++++ 5 files changed, 118 insertions(+) create mode 100644 examples/smpi/mc/hostfile_non_deterministic create mode 100644 examples/smpi/mc/hostfile_send_deterministic create mode 100644 examples/smpi/mc/non_deterministic.c create mode 100644 examples/smpi/mc/send_deterministic.c diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt index 154b3d585b..9afad64a60 100644 --- a/examples/smpi/CMakeLists.txt +++ b/examples/smpi/CMakeLists.txt @@ -23,10 +23,14 @@ if(enable_smpi) add_executable(mc/bugged1 mc/bugged1.c) add_executable(mc/bugged2 mc/bugged2.c) add_executable(mc/bugged1_liveness mc/bugged1_liveness.c) + add_executable(mc/send_deterministic mc/send_deterministic.c) + add_executable(mc/non_deterministic mc/non_deterministic.c) target_link_libraries(mc/bugged1 simgrid) target_link_libraries(mc/bugged2 simgrid) target_link_libraries(mc/bugged1_liveness simgrid) + target_link_libraries(mc/send_deterministic simgrid) + target_link_libraries(mc/non_deterministic simgrid) endif() target_link_libraries(bcbench simgrid) @@ -58,6 +62,8 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c PARENT_SCOPE ) set(bin_files @@ -67,6 +73,8 @@ set(bin_files ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1 ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2 + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic PARENT_SCOPE ) set(txt_files diff --git a/examples/smpi/mc/hostfile_non_deterministic b/examples/smpi/mc/hostfile_non_deterministic new file mode 100644 index 0000000000..b6d1c07b45 --- /dev/null +++ b/examples/smpi/mc/hostfile_non_deterministic @@ -0,0 +1,3 @@ +c-1.me +c-2.me +c-3.me diff --git a/examples/smpi/mc/hostfile_send_deterministic b/examples/smpi/mc/hostfile_send_deterministic new file mode 100644 index 0000000000..b6d1c07b45 --- /dev/null +++ b/examples/smpi/mc/hostfile_send_deterministic @@ -0,0 +1,3 @@ +c-1.me +c-2.me +c-3.me diff --git a/examples/smpi/mc/non_deterministic.c b/examples/smpi/mc/non_deterministic.c new file mode 100644 index 0000000000..0f10100b36 --- /dev/null +++ b/examples/smpi/mc/non_deterministic.c @@ -0,0 +1,54 @@ +/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */ + +/* Copyright (c) 2009 - 2014. The SimGrid Team. + * All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include +#include +#include + + +int main(int argc, char **argv) +{ + int recv_buff, err, size, rank, i; + MPI_Status status; + + /* Initialize MPI */ + err = MPI_Init(&argc, &argv); + if (err != MPI_SUCCESS) { + printf("MPI initialization failed!\n"); + exit(1); + } + + err = MPI_Comm_size(MPI_COMM_WORLD, &size); /* Get nr of tasks */ + err = MPI_Comm_rank(MPI_COMM_WORLD, &rank); /* Get id of this process */ + if (size < 2) { + printf("run this program with at least 2 processes \n"); + MPI_Finalize(); + exit(0); + } + + if (rank == 0) { + printf("MPI_ISend / MPI_IRecv Test \n"); + + for(i=0; i < size - 1; i++){ + MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status); + printf("Message received from %d\n", recv_buff); + MPI_Send(&recv_buff, 1, MPI_INT, status.MPI_SOURCE, 42, MPI_COMM_WORLD); + printf("Sent %d to rank %d\n", status.MPI_SOURCE); + } + + }else{ + MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD); + printf("Sent %d to rank 0\n", rank); + MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status); + printf("Message received from %d\n", recv_buff); + } + + MPI_Finalize(); + + return 0; +} diff --git a/examples/smpi/mc/send_deterministic.c b/examples/smpi/mc/send_deterministic.c new file mode 100644 index 0000000000..ecbcc49426 --- /dev/null +++ b/examples/smpi/mc/send_deterministic.c @@ -0,0 +1,50 @@ +/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */ + +/* Copyright (c) 2009 - 2014. The SimGrid Team. + * All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include +#include +#include + + +int main(int argc, char **argv) +{ + int recv_buff, err, size, rank, i; + MPI_Status status; + + /* Initialize MPI */ + err = MPI_Init(&argc, &argv); + if (err != MPI_SUCCESS) { + printf("MPI initialization failed!\n"); + exit(1); + } + + err = MPI_Comm_size(MPI_COMM_WORLD, &size); /* Get nr of tasks */ + err = MPI_Comm_rank(MPI_COMM_WORLD, &rank); /* Get id of this process */ + if (size < 2) { + printf("run this program with at least 2 processes \n"); + MPI_Finalize(); + exit(0); + } + + if (rank == 0) { + printf("MPI_ISend / MPI_IRecv Test \n"); + + for(i=0; i < size - 1; i++){ + MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status); + printf("Message received from %d\n", recv_buff); + } + + }else{ + MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD); + printf("Sent %d to rank 0\n", rank); + } + + MPI_Finalize(); + + return 0; +} -- 2.20.1