source: CIVL/examples/backend/mpiSumarray.cvl@ dcfde95

1.23 2.0 main test-branch
Last change on this file since dcfde95 was f65e51c, checked in by Manchun Zheng <zmanchun@…>, 10 years ago

cleaned up example according to the change of library implementations.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@3442 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 23.5 KB
Line 
1//======================= int_div.cvl ======================
2$system[civlc] void $assert(_Bool expr, ...);
3int $int_div(int numerator, int denominator) {
4 $assert(denominator != 0, "Possible division by zero");
5 if (numerator == 0)
6 return 0;
7 if (numerator >= 0) {
8 if (denominator >= 0)
9 return numerator / denominator;
10 else
11 return -(numerator / (-denominator));
12 }
13 else {
14 if (denominator >= 0)
15 return -((-numerator) / denominator);
16 else
17 return (-numerator) / (-denominator);
18 }
19}
20//======================= sum_array.c ======================
21$input int _civl_argc;
22$system[civlc] void $assume(_Bool expression);
23$assume(0 < _civl_argc);
24$input char _civl_argv[_civl_argc][];
25//======================== civlc.cvh =======================
26typedef struct $scope $scope;
27/*@ depends_on \nothing;
28 @ executes_when $true;
29 @*/
30$system[civlc] void* $malloc($scope s, int size);
31typedef struct $proc $proc;
32/*@ depends_on \nothing;
33 @ executes_when $true;
34 @*/
35$system[civlc] void $assert(_Bool expr, ...);
36/*@ depends_on \nothing;
37 @ executes_when $true;
38 @*/
39$system[civlc] void $assume(_Bool expr);
40/*@ pure;
41 @ depends_on \nothing;
42 @ executes_when $true;
43 @*/
44$system[civlc] void $elaborate(int x);
45/*@ depends_on \write(p);
46 @ executes_when $true;
47 @*/
48$system[civlc] void $free(void* p);
49//======================= sum_array.c ======================
50$input long NB = 20;
51$input long N;
52$assume((0 < N) && (N <= NB));
53//========================= seq.cvh ========================
54/*@ depends_on \write(array);
55 @ executes_when $true;
56 @*/
57$system[seq] int $seq_length(void* array);
58/*@ depends_on \write(array, value);
59 @ executes_when $true;
60 @*/
61$system[seq] void $seq_init(void* array, int count, void* value);
62/*@ depends_on \write(array, values);
63 @ executes_when $true;
64 @*/
65$system[seq] void $seq_insert(void* array, int index, void* values, int count);
66/*@ depends_on \write(array, values);
67 @*/
68$atomic_f void $seq_append(void* array, void* values, int count);
69//======================= bundle.cvh =======================
70typedef struct _bundle $bundle;
71/*@ depends_on \write(ptr);
72 @ executes_when $true;
73 @*/
74$system[bundle] $bundle $bundle_pack(void* ptr, int size);
75/*@ depends_on \write(ptr);
76 @ executes_when $true;
77 @*/
78$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
79//===================== concurrency.cvh ====================
80typedef struct _gbarrier* $gbarrier;
81typedef struct _barrier* $barrier;
82/*@ depends_on \nothing;
83 @ assigns \nothing;
84 @ reads \nothing;
85 @*/
86$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
87/*@ depends_on \write(gbarrier);
88 @ reads \nothing;
89 @ assigns gbarrier;
90 @*/
91$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
92/*@ depends_on \nothing;
93 @ assigns gbarrier;
94 @ reads gbarrier;
95 @*/
96$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
97/*@ depends_on \write(barrier);
98 @ assigns barrier;
99 @ reads \nothing;
100 @*/
101$atomic_f void $barrier_destroy($barrier barrier);
102typedef struct _collator_entry $collator_entry;
103typedef struct _gcollator* $gcollator;
104typedef struct _collator* $collator;
105/*@ depends_on \nothing;
106 @ reads \nothing;
107 @ assigns \nothing;
108 @*/
109$atomic_f $gcollator $gcollator_create($scope scope);
110/*@ depends_on \write(gcollator);
111 @ assigns gcollator;
112 @ reads \nothing;
113 @*/
114$atomic_f int $gcollator_destroy($gcollator gcollator);
115/*@ depends_on \nothing;
116 @ executes_when $true;
117 @*/
118$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
119/*@ depends_on \write(collator);
120 @ executes_when $true;
121 @*/
122$atomic_f void $collator_destroy($collator collator);
123//======================== comm.cvh ========================
124typedef struct _message{
125 int source;
126 int dest;
127 int tag;
128 $bundle data;
129 int size;
130} $message;
131typedef struct _queue $queue;
132typedef struct _gcomm* $gcomm;
133typedef struct _comm* $comm;
134/*@ pure;
135 @ depends_on \nothing;
136 @ executes_when $true;
137 @*/
138$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
139/*@ pure;
140 @ depends_on \nothing;
141 @ executes_when $true;
142 @*/
143$atomic_f int $message_source($message message);
144/*@ pure;
145 @ depends_on \nothing;
146 @ executes_when $true;
147 @*/
148$atomic_f int $message_tag($message message);
149/*@ pure;
150 @ depends_on \nothing;
151 @ executes_when $true;
152 @*/
153$atomic_f int $message_dest($message message);
154/*@ pure;
155 @ depends_on \nothing;
156 @ executes_when $true;
157 @*/
158$atomic_f int $message_size($message message);
159/*@ depends_on \write(buf);
160 @ executes_when $true;
161 @*/
162$atomic_f void $message_unpack($message message, void* buf, int size);
163/*@ depends_on \nothing;
164 @ assigns \nothing;
165 @ reads \nothing;
166 @*/
167$atomic_f $gcomm $gcomm_create($scope scope, int size);
168/*@ depends_on \write(junkMsgs), \write(gcomm);
169 @ assigns junkMsgs, gcomm;
170 @*/
171$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
172$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
173/*@ depends_on \write(comm);
174 @ assigns comm;
175 @ reads \nothing;
176 @*/
177$atomic_f void $comm_destroy($comm comm);
178/*@ pure;
179 @ depends_on \nothing;
180 @*/
181$atomic_f int $comm_size($comm comm);
182/*@ pure;
183 @ depends_on \nothing;
184 @ executes_when $true;
185 @*/
186$atomic_f int $comm_place($comm comm);
187/*@ depends_on \write(comm);
188 @ executes_when $true;
189 @*/
190$system[comm] void $comm_enqueue($comm comm, $message message);
191/*@ pure;
192 @ depends_on \write(comm);
193 @ executes_when $true;
194 @*/
195$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
196/*@ depends_on \write(comm);
197 @ executes_when $comm_probe(comm, source, tag);
198 @*/
199$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
200//====================== civl-mpi.cvh ======================
201typedef struct $mpi_gcomm $mpi_gcomm;
202$mpi_gcomm $mpi_gcomm_create($scope, int);
203void $mpi_gcomm_destroy($mpi_gcomm);
204//========================= seq.cvl ========================
205/*@ depends_on \write(array, values);
206 @*/
207$atomic_f void $seq_append(void* array, void* values, int count) {
208 int length = $seq_length(array);
209 $seq_insert(array, length, values, count);
210}
211//===================== concurrency.cvl ====================
212struct _gbarrier{
213 int nprocs;
214 $proc proc_map[];
215 _Bool in_barrier[];
216 int num_in_barrier;
217};
218struct _barrier{
219 int place;
220 $gbarrier gbarrier;
221};
222struct _collator_entry{
223 $bundle entries;
224 _Bool marks[];
225 int numMarked;
226};
227struct _gcollator{
228 int length;
229 $collator_entry entries[];
230};
231struct _collator{
232 $gcollator gcollator;
233};
234/*@ depends_on \nothing;
235 @ assigns \nothing;
236 @ reads \nothing;
237 @*/
238$atomic_f $gbarrier $gbarrier_create($scope scope, int size) {
239 $gbarrier gbarrier = ($gbarrier)($malloc(scope, sizeof(struct _gbarrier)));
240 (gbarrier)->nprocs = size;
241 (gbarrier)->proc_map = ($proc[size]) $lambda (int i) $proc_null;
242 (gbarrier)->in_barrier = (_Bool[size]) $lambda (int i) $false;
243 (gbarrier)->num_in_barrier = 0;
244 return gbarrier;
245}
246/*@ depends_on \write(gbarrier);
247 @ reads \nothing;
248 @ assigns gbarrier;
249 @*/
250$atomic_f void $gbarrier_destroy($gbarrier gbarrier) {
251 $free(gbarrier);
252}
253/*@ depends_on \nothing;
254 @ assigns gbarrier;
255 @ reads gbarrier;
256 @*/
257$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place) {
258 $assert(((gbarrier)->proc_map[place]) == $proc_null, "the place %d in the global barrier has already been taken.", place);
259 $barrier barrier = ($barrier)($malloc(scope, sizeof(struct _barrier)));
260 (barrier)->place = place;
261 (barrier)->gbarrier = gbarrier;
262 (gbarrier)->proc_map[place] = $self;
263 return barrier;
264}
265/*@ depends_on \write(barrier);
266 @ assigns barrier;
267 @ reads \nothing;
268 @*/
269$atomic_f void $barrier_destroy($barrier barrier) {
270 $free(barrier);
271}
272/*@ depends_on \nothing;
273 @ reads \nothing;
274 @ assigns \nothing;
275 @*/
276$atomic_f $gcollator $gcollator_create($scope scope) {
277 $gcollator gcollator = ($gcollator)($malloc(scope, sizeof(struct _gcollator)));
278 (gcollator)->length = 0;
279 $seq_init(&((gcollator)->entries), 0, (void*)0);
280 return gcollator;
281}
282/*@ depends_on \write(gcollator);
283 @ assigns gcollator;
284 @ reads \nothing;
285 @*/
286$atomic_f int $gcollator_destroy($gcollator gcollator) {
287 int numRemaining = (gcollator)->length;
288 $free(gcollator);
289 return numRemaining;
290}
291/*@ depends_on \nothing;
292 @ executes_when $true;
293 @*/
294$atomic_f $collator $collator_create($scope scope, $gcollator gcollator) {
295 $collator collator = ($collator)($malloc(scope, sizeof(struct _collator)));
296 (collator)->gcollator = gcollator;
297 return collator;
298}
299/*@ depends_on \write(collator);
300 @ executes_when $true;
301 @*/
302$atomic_f void $collator_destroy($collator collator) {
303 $free(collator);
304}
305//====================== civl-mpi.cvl ======================
306char* $mpi_coroutine_name(int tag);
307struct $mpi_gcomm{
308 $gcomm p2p;
309 $gcomm col;
310 $gcollator gcollator;
311 $gbarrier gbarrier;
312};
313$mpi_gcomm $mpi_gcomm_create($scope scope, int size) {
314 $mpi_gcomm result;
315 result.p2p = $gcomm_create(scope, size);
316 result.col = $gcomm_create(scope, size);
317 result.gcollator = $gcollator_create(scope);
318 result.gbarrier = $gbarrier_create(scope, size);
319 return result;
320}
321void $mpi_gcomm_destroy($mpi_gcomm gc) {
322 int numJunkRecord;
323 int numJunkMsg;
324 $message junkMsgs[];
325 $seq_init(&(junkMsgs), 0, (void*)0);
326 numJunkMsg = $gcomm_destroy(gc.p2p, &(junkMsgs));
327 {
328 int i = 0;
329 for (; i < numJunkMsg; i = i + 1) {
330 int src;
331 int dest;
332 int tag;
333 src = $message_source(junkMsgs[i]);
334 dest = $message_dest(junkMsgs[i]);
335 tag = $message_tag(junkMsgs[i]);
336 $assert($false, "MPI message leak: There is a message from rank %d to rank %d with tag %d has been sent but is never received in point-to-point communication.", src, dest, tag);
337 }
338 }
339 numJunkMsg = $gcomm_destroy(gc.col, &(junkMsgs));
340 {
341 int i = 0;
342 for (; i < numJunkMsg; i = i + 1) {
343 int src;
344 int tag;
345 char* routine;
346 src = $message_source(junkMsgs[i]);
347 tag = $message_tag(junkMsgs[i]);
348 routine = $mpi_coroutine_name(tag);
349 $assert($false, "MPI message leak: There is a message sent by rank %d for collective routine %s that is never received.", src, routine);
350 }
351 }
352 numJunkRecord = $gcollator_destroy(gc.gcollator);
353 $gbarrier_destroy(gc.gbarrier);
354 $assert(numJunkRecord == 0, "MPI collective routines are called inappropriately because there are %d collective records still remaining the collective routine checker.", numJunkRecord);
355}
356char* $mpi_coroutine_name(int tag) {
357 switch (tag) {
358 case 9999:
359 return "MPI_Bcast";
360 case 9998:
361 return "MPI_Reduce";
362 case 9997:
363 return "MPI_Allreduce";
364 case 9996:
365 return "MPI_Gather";
366 case 9995:
367 return "MPI_Scatter";
368 case 9994:
369 return "MPI_Gatherv";
370 case 9993:
371 return "MPI_Scatterv";
372 case 9992:
373 return "MPI_Allgather";
374 case 9991:
375 return "MPI_Reduce_scatter";
376 case 9990:
377 return "MPI_Alltoall";
378 case 9989:
379 return "MPI_Alltoallv";
380 case 9988:
381 return "MPI_Alltoallw";
382 case 9987:
383 return "MPI_Barrier";
384 case 9986:
385 return "MPI_Commdup";
386 case 9985:
387 return "MPI_Commfree";
388 default:
389 $assert($false, "Internal Error: Unexpected MPI routine tag:%d.\n", tag);
390 }
391}
392//======================== comm.cvl ========================
393struct _queue{
394 int length;
395 $message messages[];
396};
397struct _gcomm{
398 int nprocs;
399 $proc procs[];
400 _Bool isInit[];
401 $queue buf[][];
402};
403struct _comm{
404 int place;
405 $gcomm gcomm;
406};
407/*@ depends_on \write(data);
408 @*/
409$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size) {
410 $message result;
411 result.source = source;
412 result.dest = dest;
413 result.tag = tag;
414 result.data = $bundle_pack(data, size);
415 result.size = size;
416 return result;
417}
418int $message_source($message message) {
419 return message.source;
420}
421int $message_tag($message message) {
422 return message.tag;
423}
424int $message_dest($message message) {
425 return message.dest;
426}
427int $message_size($message message) {
428 return message.size;
429}
430/*@ depends_on \write(buf);
431 @*/
432$atomic_f void $message_unpack($message message, void* buf, int size) {
433 $bundle_unpack(message.data, buf);
434 $assert(message.size <= size, "Message of size %d exceeds the specified size %d.", message.size, size);
435}
436/*@ depends_on \nothing;
437 @ assigns \nothing;
438 @ reads \nothing;
439 @*/
440$atomic_f $gcomm $gcomm_create($scope scope, int size) {
441 $gcomm gcomm = ($gcomm)($malloc(scope, sizeof(struct _gcomm)));
442 $queue empty;
443 empty.length = 0;
444 $seq_init(&(empty.messages), 0, (void*)0);
445 (gcomm)->nprocs = size;
446 (gcomm)->procs = (($proc[size]) $lambda (int i) $proc_null);
447 (gcomm)->isInit = ((_Bool[size]) $lambda (int i) $false);
448 (gcomm)->buf = (($queue[size][size]) $lambda (int i, j) empty);
449 return gcomm;
450}
451/*@ depends_on \write(junkMsgs), \write(gcomm);
452 @ assigns junkMsgs, gcomm;
453 @ reads \nothing;
454 @*/
455$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs) {
456 int nprocs = (gcomm)->nprocs;
457 int numJunks = 0;
458 if (junkMsgs != (void*)0) {
459 {
460 int i = 0;
461 for (; i < nprocs; i = i + 1) {
462 int j = 0;
463 for (; j < nprocs; j = j + 1) {
464 $queue queue = (gcomm)->buf[i][j];
465 if (queue.length > 0)
466 $seq_append(junkMsgs, queue.messages, queue.length);
467 }
468 }
469 }
470 numJunks = $seq_length(junkMsgs);
471 }
472 $free(gcomm);
473 return numJunks;
474}
475/*@ depends_on \nothing;
476 @ reads gcomm;
477 @ assigns gcomm;
478 @*/
479$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place) {
480 $assert(!((gcomm)->isInit[place]), "the place %d is already occupied in the global communicator!", place);
481 $comm comm = ($comm)($malloc(scope, sizeof(struct _comm)));
482 (gcomm)->procs[place] = $self;
483 (gcomm)->isInit[place] = $true;
484 (comm)->gcomm = gcomm;
485 (comm)->place = place;
486 return comm;
487}
488/*@ depends_on \write(comm);
489 @ assigns comm;
490 @ reads \nothing;
491 @*/
492$atomic_f void $comm_destroy($comm comm) {
493 $free(comm);
494}
495/*@ pure;
496 @ depends_on \nothing;
497 @*/
498$atomic_f int $comm_place($comm comm) {
499 return (comm)->place;
500}
501/*@ pure;
502 @ depends_on \nothing;
503 @*/
504$atomic_f int $comm_size($comm comm) {
505 return ((comm)->gcomm)->nprocs;
506}
507//===================== MPITransformer =====================
508$input int _mpi_nprocs;
509$input int _mpi_nprocs_lo = 1;
510//======================= sum_array.c ======================
511$input int _mpi_nprocs_hi = 8;
512//===================== MPITransformer =====================
513$assume((_mpi_nprocs_lo <= _mpi_nprocs) && (_mpi_nprocs <= _mpi_nprocs_hi));
514$scope _mpi_root = $here;
515$mpi_gcomm _mpi_gcomm;
516$mpi_gcomm _mpi_gcomms[];
517void _mpi_process(int _mpi_rank) {
518 /*@ depends_on \write(format);
519 @ executes_when $true;
520 @*/
521 $system[stdio] int printf(char* restrict format, ...);
522 typedef enum MPI_Datatype{
523 MPI_CHAR,
524 MPI_CHARACTER,
525 MPI_SIGNED_CHAR,
526 MPI_UNSIGNED_CHAR,
527 MPI_BYTE,
528 MPI_WCHAR,
529 MPI_SHORT,
530 MPI_UNSIGNED_SHORT,
531 MPI_INT,
532 MPI_INT16_T,
533 MPI_INT32_T,
534 MPI_INT64_T,
535 MPI_INT8_T,
536 MPI_INTEGER,
537 MPI_INTEGER1,
538 MPI_INTEGER16,
539 MPI_INTEGER2,
540 MPI_INTEGER4,
541 MPI_INTEGER8,
542 MPI_UNSIGNED,
543 MPI_LONG,
544 MPI_UNSIGNED_LONG,
545 MPI_FLOAT,
546 MPI_DOUBLE,
547 MPI_LONG_DOUBLE,
548 MPI_LONG_LONG_INT,
549 MPI_UNSIGNED_LONG_LONG,
550 MPI_LONG_LONG,
551 MPI_PACKED,
552 MPI_LB,
553 MPI_UB,
554 MPI_UINT16_T,
555 MPI_UINT32_T,
556 MPI_UINT64_T,
557 MPI_UINT8_T,
558 MPI_FLOAT_INT,
559 MPI_DOUBLE_INT,
560 MPI_LONG_INT,
561 MPI_SHORT_INT,
562 MPI_2INT,
563 MPI_LONG_DOUBLE_INT,
564 MPI_AINT,
565 MPI_OFFSET,
566 MPI_2DOUBLE_PRECISION,
567 MPI_2INTEGER,
568 MPI_2REAL,
569 MPI_C_BOOL,
570 MPI_C_COMPLEX,
571 MPI_C_DOUBLE_COMPLEX,
572 MPI_C_FLOAT_COMPLEX,
573 MPI_C_LONG_DOUBLE_COMPLEX,
574 MPI_COMPLEX,
575 MPI_COMPLEX16,
576 MPI_COMPLEX32,
577 MPI_COMPLEX4,
578 MPI_COMPLEX8,
579 MPI_REAL,
580 MPI_REAL16,
581 MPI_REAL2,
582 MPI_REAL4,
583 MPI_REAL8
584 } MPI_Datatype;
585 typedef struct MPI_Comm MPI_Comm;
586 MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
587 MPI_Comm MPI_COMM_WORLD = $mpi_comm_create($here, _mpi_gcomm, _mpi_rank);
588 typedef struct MPI_Request* MPI_Request;
589 typedef struct MPI_Status{
590 int MPI_SOURCE;
591 int MPI_TAG;
592 int MPI_ERROR;
593 int size;
594 } MPI_Status;
595 int MPI_Send(void*, int, MPI_Datatype, int, int, MPI_Comm);
596 int MPI_Recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
597 int MPI_Get_count(MPI_Status*, MPI_Datatype, int*);
598 int MPI_Comm_size(MPI_Comm, int*);
599 int MPI_Comm_rank(MPI_Comm, int*);
600 typedef enum _mpi_state{
601 _MPI_UNINIT,
602 _MPI_INIT,
603 _MPI_FINALIZED
604 } $mpi_state;
605 $mpi_state _mpi_state = _MPI_UNINIT;
606 int $mpi_init(void) {
607 $assert(_mpi_state == _MPI_UNINIT, "Process can only call MPI_Init() at most once.");
608 _mpi_state = _MPI_INIT;
609 return 0;
610 }
611 void $mpi_comm_destroy(MPI_Comm, $mpi_state);
612 int MPI_Finalize(void);
613 double oracle;
614 void master(void);
615 void slave(void);
616 int _civl_main(int argc, char** argv) {
617 int myrank;
618 $mpi_init();
619 MPI_Comm_rank(MPI_COMM_WORLD, &(myrank));
620 if (!myrank)
621 master();
622 else
623 slave();
624 MPI_Finalize();
625 return 0;
626 }
627 void master(void) {
628 float array[N];
629 double mysum;
630 double tmpsum;
631 unsigned long long step;
632 unsigned long long i;
633 int size;
634 MPI_Status status;
635 for (i = 0; i < N; i = i + 1)
636 array[i] = i + 1;
637 oracle = 0.0;
638 for (i = 0; i < N; i = i + 1)
639 oracle = oracle + (array[i]);
640 MPI_Comm_size(MPI_COMM_WORLD, &(size));
641 if (size != 1)
642 step = $int_div(N, size - 1);
643 else
644 step = N;
645 for (i = 0; i < (size - 1); i = i + 1)
646 MPI_Send(array + (i * step), step, MPI_FLOAT, i + 1, 100, MPI_COMM_WORLD);
647 {
648 i = (size - 1) * step;
649 mysum = 0;
650 for (; i < N; i = i + 1)
651 mysum = mysum + (array[i]);
652 }
653 for (i = 1; i < size; ) {
654 MPI_Recv(&(tmpsum), 1, MPI_DOUBLE, -1, 101, MPI_COMM_WORLD, &(status));
655 mysum = mysum + tmpsum;
656 i = i + 1;
657 }
658 $assert(oracle == mysum, "The sum of %d array elements is %f but the expected one is %f.\n", N, mysum, oracle);
659 printf("%lf\n", mysum);
660 }
661 void slave(void) {
662 float array[N];
663 double sum;
664 unsigned long long i;
665 int count;
666 MPI_Status status;
667 MPI_Recv(array, N, MPI_FLOAT, 0, 100, MPI_COMM_WORLD, &(status));
668 MPI_Get_count(&(status), MPI_FLOAT, &(count));
669 {
670 i = 0;
671 sum = 0;
672 for (; i < count; i = i + 1)
673 sum = sum + (array[i]);
674 }
675 MPI_Send(&(sum), 1, MPI_DOUBLE, 0, 101, MPI_COMM_WORLD);
676 }
677 int sizeofDatatype(MPI_Datatype);
678 int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
679 int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
680 /*@ depends_on \write(buf);
681 @ executes_when $true;
682 @*/
683 $system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
684 struct MPI_Request{
685 MPI_Status status;
686 _Bool isSend;
687 };
688 struct MPI_Comm{
689 $comm p2p;
690 $comm col;
691 $collator collator;
692 $barrier barrier;
693 int gcommIndex;
694 };
695 int MPI_Finalize(void) {
696 $assert(_mpi_state == _MPI_INIT, "Process can only call MPI_Finalize() after the MPI enviroment is created and before cleaned.");
697 _mpi_state = _MPI_FINALIZED;
698 return 0;
699 }
700 int MPI_Comm_size(MPI_Comm comm, int* size) {
701 $assert(_mpi_state == _MPI_INIT, "MPI_Comm_size() cannot be invoked without MPI_Init() being called before.\n");
702 *size = $comm_size(comm.p2p);
703 return 0;
704 }
705 int MPI_Comm_rank(MPI_Comm comm, int* rank) {
706 $assert(_mpi_state == _MPI_INIT, "MPI_Comm_rank() cannot be invoked without MPI_Init() being called before.\n");
707 *rank = $comm_place(comm.p2p);
708 return 0;
709 }
710 int MPI_Send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm) {
711 $assert(_mpi_state == _MPI_INIT, "MPI_Send() cannot be invoked without MPI_Init() being called before.\n");
712 $mpi_check_buffer(buf, count, datatype);
713 int $sef$0 = $mpi_send(buf, count, datatype, dest, tag, comm);
714 return $sef$0;
715 }
716 int MPI_Recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status) {
717 $assert(_mpi_state == _MPI_INIT, "MPI_Recv() cannot be invoked without MPI_Init() being called before.\n");
718 int $sef$1 = $mpi_recv(buf, count, datatype, source, tag, comm, status);
719 return $sef$1;
720 }
721 int MPI_Get_count(MPI_Status* status, MPI_Datatype datatype, int* count) {
722 $assert(_mpi_state == _MPI_INIT, "MPI_Get_count() cannot be invoked without MPI_Init() being called before.\n");
723 int $sef$2 = sizeofDatatype(datatype);
724 *count = $int_div((status)->size, $sef$2);
725 return 0;
726 }
727 int sizeofDatatype(MPI_Datatype datatype) {
728 switch (datatype) {
729 case MPI_INT:
730 return sizeof(int);
731 case MPI_2INT:
732 return sizeof(int) * 2;
733 case MPI_FLOAT:
734 return sizeof(float);
735 case MPI_DOUBLE:
736 return sizeof(double);
737 case MPI_CHAR:
738 return sizeof(char);
739 case MPI_BYTE:
740 return sizeof(char);
741 case MPI_SHORT:
742 return sizeof(short);
743 case MPI_LONG:
744 return sizeof(long);
745 case MPI_LONG_DOUBLE:
746 return sizeof(long double);
747 case MPI_LONG_LONG_INT:
748 return sizeof(long long);
749 case MPI_LONG_LONG:
750 return sizeof(long long);
751 case MPI_UNSIGNED_LONG_LONG:
752 return sizeof(unsigned long long);
753 default:
754 $assert(0, "Unreachable");
755 }
756 }
757 MPI_Comm $mpi_comm_create($scope scope, $mpi_gcomm gc, int rank) {
758 MPI_Comm result;
759 result.p2p = $comm_create(scope, gc.p2p, rank);
760 result.col = $comm_create(scope, gc.col, rank);
761 result.collator = $collator_create(scope, gc.gcollator);
762 result.barrier = $barrier_create(scope, gc.gbarrier, rank);
763 result.gcommIndex = 0;
764 return result;
765 }
766 void $mpi_comm_destroy(MPI_Comm comm, $mpi_state mpi_state) {
767 if (comm.gcommIndex == 0)
768 $assert(mpi_state == _MPI_FINALIZED, "Process terminates without calling MPI_Finalize() first.");
769 $comm_destroy(comm.p2p);
770 $comm_destroy(comm.col);
771 $collator_destroy(comm.collator);
772 $barrier_destroy(comm.barrier);
773 }
774 int $mpi_send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm) {
775 if (dest >= 0) {
776 int $sef$5 = sizeofDatatype(datatype);
777 int size = count * $sef$5;
778 int place = $comm_place(comm.p2p);
779 $message out = $message_pack(place, dest, tag, buf, size);
780 $comm_enqueue(comm.p2p, out);
781 }
782 return 0;
783 }
784 int $mpi_recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status) {
785 if ((source >= 0) || (source == (-1))) {
786 $message in;
787 int place = $comm_place(comm.p2p);
788 int deterministicTag;
789 $assert((tag == (-2)) || (tag >= 0), "Illegal MPI message receive tag %d.\n", tag);
790 deterministicTag = tag < 0 ? -2 : tag;
791 $elaborate(source);
792 in = $comm_dequeue(comm.p2p, source, deterministicTag);
793 int $sef$6 = sizeofDatatype(datatype);
794 int size = count * $sef$6;
795 $message_unpack(in, buf, size);
796 if (status != (void*)0) {
797 (status)->size = $message_size(in);
798 (status)->MPI_SOURCE = $message_source(in);
799 (status)->MPI_TAG = $message_tag(in);
800 (status)->MPI_ERROR = 0;
801 }
802 }
803 return 0;
804 }
805 {
806 _civl_main(_civl_argc, (char*[_civl_argc]) $lambda (int i) _civl_argv[i]);
807 }
808 $mpi_comm_destroy(MPI_COMM_WORLD, _mpi_state);
809}
810int main() {
811 _mpi_gcomm = $mpi_gcomm_create(_mpi_root, _mpi_nprocs);
812 $seq_init(&(_mpi_gcomms), 1, &(_mpi_gcomm));
813 $parfor (int i: 0 .. _mpi_nprocs - 1)
814
815 _mpi_process(i);
816 $mpi_gcomm_destroy(_mpi_gcomm);
817}
Note: See TracBrowser for help on using the repository browser.