source: CIVL/examples/messagePassing/hybrid2.cvl@ 13ac9574

1.23 2.0 main test-branch
Last change on this file since 13ac9574 was b70deeb, checked in by Stephen Siegel <siegel@…>, 12 years ago

Added streamlined version of hybrid example, but still can't complete model checking of entire state space.

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

  • Property mode set to 100644
File size: 965 bytes
Line 
1/* CIVL model of simple hybrid MPI+threads program.
2 * The program has a defect.
3 */
4#include<civlc.h>
5#include<stdio.h>
6#include "mp_root2.cvh"
7#define TAG 0
8
9void MPI_Process (int __rank) {
10#include "mp_proc2.cvh"
11 int rank;
12
13 MPI_Comm_rank(MPI_COMM_WORLD, &rank);
14 $proc threads[2];
15 void Thread(int tid) {
16 int x = 2*rank + tid, y;
17
18 for (int j=0; j<2; j++) {
19 if (rank == 1) {
20 for (int i=0; i<2; i++)
21 MPI_Send(&x, 1, MPI_INT, 1, TAG, MPI_COMM_WORLD);
22 for (int i=0; i<2; i++)
23 MPI_Recv(&y, 1, MPI_INT, 1, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
24 } else {
25 for (int i=0; i<2; i++)
26 MPI_Recv(&y, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
27 for (int i=0; i<2; i++)
28 MPI_Send(&x, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD);
29 }
30 }
31 }
32 $atomic {
33 for (int i=0; i<2; i++) threads[i] = $spawn Thread(i);
34 for (int i=0; i<2; i++) $wait threads[i];
35 }
36}
Note: See TracBrowser for help on using the repository browser.