| 1 | #ifdef _CIVL
|
|---|
| 2 | #include <civlc.cvh>
|
|---|
| 3 | #endif
|
|---|
| 4 | /* FEVS: A Functional Equivalence Verification Suite for High-Performance
|
|---|
| 5 | * Scientific Computing
|
|---|
| 6 | *
|
|---|
| 7 | * Copyright (C) 2010, Stephen F. Siegel, Timothy K. Zirkel,
|
|---|
| 8 | * University of Delaware
|
|---|
| 9 | *
|
|---|
| 10 | * This program is free software; you can redistribute it and/or
|
|---|
| 11 | * modify it under the terms of the GNU General Public License as
|
|---|
| 12 | * published by the Free Software Foundation; either version 3 of the
|
|---|
| 13 | * License, or (at your option) any later version.
|
|---|
| 14 | *
|
|---|
| 15 | * This program is distributed in the hope that it will be useful, but
|
|---|
| 16 | * WITHOUT ANY WARRANTY; without even the implied warranty of
|
|---|
| 17 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
|---|
| 18 | * General Public License for more details.
|
|---|
| 19 | *
|
|---|
| 20 | * You should have received a copy of the GNU General Public License
|
|---|
| 21 | * along with this program; if not, write to the Free Software
|
|---|
| 22 | * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
|
|---|
| 23 | * 02110-1301 USA.
|
|---|
| 24 | */
|
|---|
| 25 |
|
|---|
| 26 | #include<stdio.h>
|
|---|
| 27 | #include<stdlib.h>
|
|---|
| 28 | #include"mpi.h"
|
|---|
| 29 |
|
|---|
| 30 | #pragma CIVL $input int NB;
|
|---|
| 31 | #pragma CIVL $output int __sum;
|
|---|
| 32 | double sum;
|
|---|
| 33 | double localSum = 0.0;
|
|---|
| 34 | int PID;
|
|---|
| 35 | int NPROCS;
|
|---|
| 36 |
|
|---|
| 37 | double computeGlobalSum() {
|
|---|
| 38 | double result = localSum;
|
|---|
| 39 | double buffer;
|
|---|
| 40 | int i;
|
|---|
| 41 | MPI_Status status;
|
|---|
| 42 |
|
|---|
| 43 | for (i=1; i<NPROCS; i++) {
|
|---|
| 44 | MPI_Recv(&buffer, 1, MPI_DOUBLE, i, 0, MPI_COMM_WORLD, &status);
|
|---|
| 45 | result += buffer;
|
|---|
| 46 | }
|
|---|
| 47 | return result;
|
|---|
| 48 | }
|
|---|
| 49 |
|
|---|
| 50 | int main(int argc, char *argv[]) {
|
|---|
| 51 | #ifdef _CIVL
|
|---|
| 52 | $assume(1 < argc);
|
|---|
| 53 | #endif
|
|---|
| 54 | int n = atoi(argv[1]);
|
|---|
| 55 | #pragma CIVL $assume(0 < n && n <= NB);
|
|---|
| 56 | MPI_Init(&argc, &argv);
|
|---|
| 57 | MPI_Comm_size(MPI_COMM_WORLD, &NPROCS);
|
|---|
| 58 | MPI_Comm_rank(MPI_COMM_WORLD, &PID);
|
|---|
| 59 | int first = n*PID/NPROCS;
|
|---|
| 60 | int afterLast = n*(PID+1)/NPROCS;
|
|---|
| 61 | int i;
|
|---|
| 62 | double a[n];
|
|---|
| 63 | FILE *fp = fopen("data","r");
|
|---|
| 64 |
|
|---|
| 65 | for (i=0; i<n; i++) fscanf(fp, "%lf", &a[i]);
|
|---|
| 66 | for (i=first; i<afterLast; i++) localSum += a[i];
|
|---|
| 67 | if (PID == 0) {
|
|---|
| 68 | sum = computeGlobalSum();
|
|---|
| 69 | printf("%lf", sum);
|
|---|
| 70 | #pragma CIVL __sum = sum;
|
|---|
| 71 | } else {
|
|---|
| 72 | MPI_Send(&localSum, 1, MPI_DOUBLE, 0, 0, MPI_COMM_WORLD);
|
|---|
| 73 | }
|
|---|
| 74 | fclose(fp);
|
|---|
| 75 | MPI_Finalize();
|
|---|
| 76 | return 0;
|
|---|
| 77 | }
|
|---|
