/***************************************** * SOURCE: adder_par.c by vsl@udel * The source program is included in FEVS * vsl.cis.udel.edu/fevs * FILE: adder_par.cvl * DESCRIPTION: This a manually translated * CIVL program which is based on "adder_par.c" * This program sums all elements of an array * up. * * AUTHOR: Ziqing Luo * COMMANS: civl verify adder_par.cvl * -inputNPROCSB=5 -inputNB=10 * or * make civl *****************************************/ #include #include #include #include #include $input int NPROCS; $input int NPROCSB; $input int N; $input int NB; $input double a[N]; $output double SUM; $assume 0 < N && N < NB; $assume 0 < NPROCS && NPROCS <= NPROCSB; $assume NPROCS <= N; CMPI_Gcomm __MPI_COMM_WORLD; void MPI_Process(int place){ double sum; double localSum = 0.0; int PID; int nprocs; MPI_Comm MPI_COMM_WORLD; __MPI_Sys_status__ _my_status = __UNINIT; $assert _my_status == __UNINIT; double computeGlobalSum() { double result = localSum; double buffer; int i; MPI_Status status; for (i=1; i