source: CIVL/examples/contracts/contractsMPI/wildcard-good.c

main
Last change on this file was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 671 bytes
RevLine 
[7f8124c]1#include <mpi.h>
2
[cc2ac3e]3int size, rank;
[7f8124c]4int root;
[cc2ac3e]5int x;
[7f8124c]6
[3b8cd00]7/*@ \mpi_collective(MPI_COMM_WORLD, P2P):
[7f8124c]8 @ requires rank == \mpi_comm_rank;
9 @ requires size == \mpi_comm_size;
[cc2ac3e]10 @ requires 0 <= root && root < \mpi_comm_size;
11 @ requires \mpi_agree(root);
12 @ requires datatype == MPI_INT;
[3b8cd00]13 @ ensures \on(root, x) == size - 1 ||
[cc2ac3e]14 @ (\on(root, x) == size - 2 && size - 1 == root);
[7f8124c]15 @*/
[cc2ac3e]16int wildcard(MPI_Datatype datatype) {
17 if (rank == root) {
[7f8124c]18 for (int i = 0; i < size; i++)
19 if (i != root)
[cc2ac3e]20 MPI_Recv(&x, 1, datatype, i, 0, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
21 } else
22 MPI_Send(&rank, 1, datatype, root, 0, MPI_COMM_WORLD);
23 return 0;
[7f8124c]24}
Note: See TracBrowser for help on using the repository browser.