source: CIVL/examples/backend/mpiSumarray.cvl@ 1e03cfd

1.23 2.0 main test-branch
Last change on this file since 1e03cfd was e3ed948, checked in by Ziqing Luo <ziqing@…>, 10 years ago

fixed a bug in bundle_pack

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