source: CIVL/examples/backend/mpiSumarray.cvl@ 04c71e3

1.23 2.0 main test-branch
Last change on this file since 04c71e3 was 6e64101, checked in by Ziqing Luo <ziqing@…>, 9 years ago

update the back-end example by letting CIVL re-print it

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