| 1 | // How to get rid of BOUNDS ?
|
|---|
| 2 | /************************** source code **************************/
|
|---|
| 3 | #include<mpi.h>
|
|---|
| 4 | #include<civl-mpi.cvh>
|
|---|
| 5 | #include<string.h>
|
|---|
| 6 |
|
|---|
| 7 | #define DATA_LIMIT 1024
|
|---|
| 8 | #pragma CIVL ACSL
|
|---|
| 9 | /*@
|
|---|
| 10 | @ \mpi_collective(comm, P2P) :
|
|---|
| 11 | @ requires \mpi_agree(root) && \mpi_agree(sendcount * \mpi_extent(sendtype));
|
|---|
| 12 | @ requires sendcount * \mpi_extent(sendtype) >= 0 && sendcount * \mpi_extent(sendtype) < DATA_LIMIT;
|
|---|
| 13 | @ requires recvcount * \mpi_extent(recvtype) >= 0 && recvcount * \mpi_extent(recvtype) < DATA_LIMIT;
|
|---|
| 14 | @ requires 0 <= root && root < \mpi_comm_size;
|
|---|
| 15 | @ requires \mpi_valid(sendbuf, sendcount, sendtype);
|
|---|
| 16 | @ behavior imroot:
|
|---|
| 17 | @ assumes \mpi_comm_rank == root;
|
|---|
| 18 | @ assigns \mpi_region(recvbuf, recvcount * \mpi_comm_size, recvtype);
|
|---|
| 19 | @ requires \mpi_valid(recvbuf, recvcount * \mpi_comm_size, recvtype);
|
|---|
| 20 | @ requires recvcount * \mpi_extent(recvtype) ==
|
|---|
| 21 | @ sendcount * \mpi_extent(sendtype);
|
|---|
| 22 | @ ensures \mpi_equals(\mpi_region(\mpi_offset(recvbuf, root * sendcount, sendtype),
|
|---|
| 23 | @ recvcount, recvtype),
|
|---|
| 24 | @ \mpi_region(sendbuf, sendcount, sendtype)
|
|---|
| 25 | @ );
|
|---|
| 26 | @
|
|---|
| 27 | @ waitsfor (0 .. \mpi_comm_size-1);
|
|---|
| 28 | @ behavior imnroot:
|
|---|
| 29 | @ assumes \mpi_comm_rank != root;
|
|---|
| 30 | @ ensures \mpi_equals(\mpi_region(sendbuf, sendcount, sendtype),
|
|---|
| 31 | @ \mpi_region(\mpi_offset(\on(root, recvbuf),
|
|---|
| 32 | @ \mpi_comm_rank * sendcount, sendtype),
|
|---|
| 33 | @ sendcount, sendtype)
|
|---|
| 34 | @ );
|
|---|
| 35 | @*/
|
|---|
| 36 | int gather(void* sendbuf, int sendcount, MPI_Datatype sendtype,
|
|---|
| 37 | void* recvbuf, int recvcount, MPI_Datatype recvtype,
|
|---|
| 38 | int root, MPI_Comm comm){
|
|---|
| 39 | int rank, nprocs;
|
|---|
| 40 | MPI_Status status;
|
|---|
| 41 | int tag = 998;
|
|---|
| 42 |
|
|---|
| 43 | MPI_Comm_rank(comm, &rank);
|
|---|
| 44 | MPI_Comm_size(comm, &nprocs);
|
|---|
| 45 | if(root == rank) {
|
|---|
| 46 | void *ptr;
|
|---|
| 47 |
|
|---|
| 48 | ptr = $mpi_pointer_add(recvbuf, root * recvcount, recvtype);
|
|---|
| 49 | memcpy(ptr, sendbuf, recvcount * sizeofDatatype(recvtype));
|
|---|
| 50 | }else
|
|---|
| 51 | MPI_Send(sendbuf, sendcount, sendtype, root, tag, comm);
|
|---|
| 52 | if(rank == root) {
|
|---|
| 53 | int real_recvcount;
|
|---|
| 54 | int offset;
|
|---|
| 55 |
|
|---|
| 56 | for(int i=0; i<nprocs; i++) {
|
|---|
| 57 | if(i != root) {
|
|---|
| 58 | void * ptr;
|
|---|
| 59 |
|
|---|
| 60 | offset = i * recvcount;
|
|---|
| 61 | ptr = $mpi_pointer_add(recvbuf, offset, recvtype);
|
|---|
| 62 | MPI_Recv(ptr, recvcount, recvtype, i, tag, comm,
|
|---|
| 63 | &status);
|
|---|
| 64 |
|
|---|
| 65 | // Inserted twist which will make the ensurance not hold:
|
|---|
| 66 | memset(ptr, 0, recvcount * sizeofDatatype(recvtype));
|
|---|
| 67 | }
|
|---|
| 68 | }
|
|---|
| 69 | }
|
|---|
| 70 | return 0;
|
|---|
| 71 | }
|
|---|
