source: CIVL/examples/backend/mpiSumarray.cvl

main
Last change on this file was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

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