source: CIVL/examples/backend/mpiSumarray.cvl@ 3a2ec5e

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

implemented checking of array length when it is declared

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@3408 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 36.9 KB
Line 
1//======================= int_div.cvl ======================
2$system[civlc] void $assert(_Bool expr, ...);
3int $int_div(int numerator, int denominator)
4{
5 $assert(denominator != 0, "Possible division by zero");
6 if (numerator == 0)
7 return 0;
8 if (numerator >= 0)
9 {
10 if (denominator >= 0)
11 return numerator / denominator;
12 else
13 return -(numerator / (-denominator));
14 }
15 else
16 {
17 if (denominator >= 0)
18 return -((-numerator) / denominator);
19 else
20 return (-numerator) / (-denominator);
21 }
22}
23//======================== civlc.cvh =======================
24typedef struct $proc $proc;
25typedef struct $scope $scope;
26/*@ depends_on \nothing;
27 @ executes_when $true;
28 @*/
29$system[civlc] void $assert(_Bool expr, ...);
30/*@ depends_on \nothing;
31 @ executes_when $true;
32 @*/
33$system[civlc] void $assume(_Bool expr);
34/*@ pure;
35 @ depends_on \nothing;
36 @ executes_when $true;
37 @*/
38$system[civlc] void $elaborate(int x);
39/*@ depends_on \nothing;
40 @ executes_when $true;
41 @*/
42$system[civlc] void* $malloc($scope s, int size);
43/*@ depends_on \write(p);
44 @ executes_when $true;
45 @*/
46$system[civlc] void $free(void* p);
47/*@ depends_on \nothing;
48 @ executes_when $true;
49 @*/
50$system[civlc] void $assert(_Bool expr, ...);
51/*@ depends_on \nothing;
52 @ executes_when $true;
53 @*/
54$system[civlc] void $assume(_Bool expr);
55/*@ pure;
56 @ depends_on \nothing;
57 @ executes_when $true;
58 @*/
59$system[civlc] void $elaborate(int x);
60/*@ depends_on \nothing;
61 @ executes_when $true;
62 @*/
63$system[civlc] void* $malloc($scope s, int size);
64/*@ depends_on \write(p);
65 @ executes_when $true;
66 @*/
67$system[civlc] void $free(void* p);
68//========================= stdio.h ========================
69$system[stdio] int printf(char* restrict format, ...);
70//========================= seq.cvh ========================
71/*@ depends_on \write(array);
72 @ executes_when $true;
73 @*/
74$system[seq] int $seq_length(void* array);
75/*@ depends_on \write(array, value);
76 @ executes_when $true;
77 @*/
78$system[seq] void $seq_init(void* array, int count, void* value);
79/*@ depends_on \write(array, values);
80 @ executes_when $true;
81 @*/
82$system[seq] void $seq_insert(void* array, int index, void* values, int count);
83/*@ depends_on \write(array, values);
84 @*/
85$atomic_f void $seq_append(void* array, void* values, int count);
86//======================== civlc.cvh =======================
87/*@ depends_on \nothing;
88 @ executes_when $true;
89 @*/
90$system[civlc] void $assert(_Bool expr, ...);
91/*@ depends_on \nothing;
92 @ executes_when $true;
93 @*/
94$system[civlc] void $assume(_Bool expr);
95/*@ pure;
96 @ depends_on \nothing;
97 @ executes_when $true;
98 @*/
99$system[civlc] void $elaborate(int x);
100/*@ depends_on \nothing;
101 @ executes_when $true;
102 @*/
103$system[civlc] void* $malloc($scope s, int size);
104/*@ depends_on \write(p);
105 @ executes_when $true;
106 @*/
107$system[civlc] void $free(void* p);
108//======================= bundle.cvh =======================
109typedef struct _bundle $bundle;
110/*@ depends_on \write(ptr);
111 @ executes_when $true;
112 @*/
113$system[bundle] $bundle $bundle_pack(void* ptr, int size);
114/*@ depends_on \write(ptr);
115 @ executes_when $true;
116 @*/
117$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
118//===================== concurrency.cvh ====================
119typedef struct _gbarrier* $gbarrier;
120typedef struct _barrier* $barrier;
121/*@ depends_on \nothing;
122 @ assigns \nothing;
123 @ reads \nothing;
124 @*/
125$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
126/*@ depends_on \write(gbarrier);
127 @ reads \nothing;
128 @ assigns gbarrier;
129 @*/
130$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
131/*@ depends_on \nothing;
132 @ assigns gbarrier;
133 @ reads gbarrier;
134 @*/
135$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
136/*@ depends_on \write(barrier);
137 @ assigns barrier;
138 @ reads \nothing;
139 @*/
140$atomic_f void $barrier_destroy($barrier barrier);
141typedef struct _collator_entry $collator_entry;
142typedef struct _gcollator* $gcollator;
143typedef struct _collator* $collator;
144/*@ depends_on \nothing;
145 @ reads \nothing;
146 @ assigns \nothing;
147 @*/
148$atomic_f $gcollator $gcollator_create($scope scope);
149/*@ depends_on \write(gcollator);
150 @ assigns gcollator;
151 @ reads \nothing;
152 @*/
153$atomic_f int $gcollator_destroy($gcollator gcollator);
154/*@ depends_on \nothing;
155 @ executes_when $true;
156 @*/
157$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
158/*@ depends_on \write(collator);
159 @ executes_when $true;
160 @*/
161$atomic_f void $collator_destroy($collator collator);
162//========================== mpi.h =========================
163typedef enum $anon_enum_0{
164 MPI_CHAR,
165 MPI_CHARACTER,
166 MPI_SIGNED_CHAR,
167 MPI_UNSIGNED_CHAR,
168 MPI_BYTE,
169 MPI_WCHAR,
170 MPI_SHORT,
171 MPI_UNSIGNED_SHORT,
172 MPI_INT,
173 MPI_INT16_T,
174 MPI_INT32_T,
175 MPI_INT64_T,
176 MPI_INT8_T,
177 MPI_INTEGER,
178 MPI_INTEGER1,
179 MPI_INTEGER16,
180 MPI_INTEGER2,
181 MPI_INTEGER4,
182 MPI_INTEGER8,
183 MPI_UNSIGNED,
184 MPI_LONG,
185 MPI_UNSIGNED_LONG,
186 MPI_FLOAT,
187 MPI_DOUBLE,
188 MPI_LONG_DOUBLE,
189 MPI_LONG_LONG_INT,
190 MPI_UNSIGNED_LONG_LONG,
191 MPI_LONG_LONG,
192 MPI_PACKED,
193 MPI_LB,
194 MPI_UB,
195 MPI_UINT16_T,
196 MPI_UINT32_T,
197 MPI_UINT64_T,
198 MPI_UINT8_T,
199 MPI_FLOAT_INT,
200 MPI_DOUBLE_INT,
201 MPI_LONG_INT,
202 MPI_SHORT_INT,
203 MPI_2INT,
204 MPI_LONG_DOUBLE_INT,
205 MPI_AINT,
206 MPI_OFFSET,
207 MPI_2DOUBLE_PRECISION,
208 MPI_2INTEGER,
209 MPI_2REAL,
210 MPI_C_BOOL,
211 MPI_C_COMPLEX,
212 MPI_C_DOUBLE_COMPLEX,
213 MPI_C_FLOAT_COMPLEX,
214 MPI_C_LONG_DOUBLE_COMPLEX,
215 MPI_COMPLEX,
216 MPI_COMPLEX16,
217 MPI_COMPLEX32,
218 MPI_COMPLEX4,
219 MPI_COMPLEX8,
220 MPI_REAL,
221 MPI_REAL16,
222 MPI_REAL2,
223 MPI_REAL4,
224 MPI_REAL8
225} MPI_Datatype;
226typedef struct MPI_Comm MPI_Comm;
227typedef struct MPI_Status{
228 int MPI_SOURCE;
229 int MPI_TAG;
230 int MPI_ERROR;
231 int size;
232} MPI_Status;
233//======================== comm.cvh ========================
234typedef struct _message{
235 int source;
236 int dest;
237 int tag;
238 $bundle data;
239 int size;
240} $message;
241typedef struct _queue $queue;
242typedef struct _gcomm* $gcomm;
243typedef struct _comm* $comm;
244/*@ pure;
245 @ depends_on \nothing;
246 @ executes_when $true;
247 @*/
248$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
249/*@ pure;
250 @ depends_on \nothing;
251 @ executes_when $true;
252 @*/
253$atomic_f int $message_source($message message);
254/*@ pure;
255 @ depends_on \nothing;
256 @ executes_when $true;
257 @*/
258$atomic_f int $message_tag($message message);
259/*@ pure;
260 @ depends_on \nothing;
261 @ executes_when $true;
262 @*/
263$atomic_f int $message_dest($message message);
264/*@ pure;
265 @ depends_on \nothing;
266 @ executes_when $true;
267 @*/
268$atomic_f int $message_size($message message);
269/*@ depends_on \write(buf);
270 @ executes_when $true;
271 @*/
272$atomic_f void $message_unpack($message message, void* buf, int size);
273/*@ depends_on \nothing;
274 @ assigns \nothing;
275 @ reads \nothing;
276 @*/
277$atomic_f $gcomm $gcomm_create($scope scope, int size);
278/*@ depends_on \write(junkMsgs), \write(gcomm);
279 @ assigns junkMsgs, gcomm;
280 @*/
281$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
282$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
283/*@ depends_on \write(comm);
284 @ assigns comm;
285 @ reads \nothing;
286 @*/
287$atomic_f void $comm_destroy($comm comm);
288/*@ pure;
289 @ depends_on \nothing;
290 @*/
291$atomic_f int $comm_size($comm comm);
292/*@ pure;
293 @ depends_on \nothing;
294 @ executes_when $true;
295 @*/
296$atomic_f int $comm_place($comm comm);
297/*@ depends_on \write(comm);
298 @ executes_when $true;
299 @*/
300$system[comm] void $comm_enqueue($comm comm, $message message);
301/*@ pure;
302 @ depends_on \write(comm);
303 @ executes_when $true;
304 @*/
305$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
306/*@ depends_on \write(comm);
307 @ executes_when $comm_probe(comm, source, tag);
308 @*/
309$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
310//====================== civl-mpi.cvh ======================
311typedef enum _mpi_state{
312 _MPI_UNINIT,
313 _MPI_INIT,
314 _MPI_FINALIZED
315} $mpi_state;
316typedef struct MPI_Comm MPI_Comm;
317typedef struct MPI_Status MPI_Status;
318typedef struct $mpi_gcomm $mpi_gcomm;
319int sizeofDatatype(MPI_Datatype);
320$mpi_gcomm $mpi_gcomm_create($scope, int);
321void $mpi_gcomm_destroy($mpi_gcomm);
322MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
323void $mpi_comm_destroy(MPI_Comm, $mpi_state);
324int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
325int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
326$system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
327//========================= mpi.cvl ========================
328struct MPI_Comm{
329 $comm p2p;
330 $comm col;
331 $collator collator;
332 $barrier barrier;
333 int gcommIndex;
334};
335//======================== civlc.cvh =======================
336/*@ depends_on \nothing;
337 @ executes_when $true;
338 @*/
339$system[civlc] void $assert(_Bool expr, ...);
340/*@ depends_on \nothing;
341 @ executes_when $true;
342 @*/
343$system[civlc] void $assume(_Bool expr);
344/*@ pure;
345 @ depends_on \nothing;
346 @ executes_when $true;
347 @*/
348$system[civlc] void $elaborate(int x);
349/*@ depends_on \nothing;
350 @ executes_when $true;
351 @*/
352$system[civlc] void* $malloc($scope s, int size);
353/*@ depends_on \write(p);
354 @ executes_when $true;
355 @*/
356$system[civlc] void $free(void* p);
357//======================= bundle.cvh =======================
358/*@ depends_on \write(ptr);
359 @ executes_when $true;
360 @*/
361$system[bundle] $bundle $bundle_pack(void* ptr, int size);
362/*@ depends_on \write(ptr);
363 @ executes_when $true;
364 @*/
365$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
366//===================== concurrency.cvh ====================
367/*@ depends_on \nothing;
368 @ assigns \nothing;
369 @ reads \nothing;
370 @*/
371$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
372/*@ depends_on \write(gbarrier);
373 @ reads \nothing;
374 @ assigns gbarrier;
375 @*/
376$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
377/*@ depends_on \nothing;
378 @ assigns gbarrier;
379 @ reads gbarrier;
380 @*/
381$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
382/*@ depends_on \write(barrier);
383 @ assigns barrier;
384 @ reads \nothing;
385 @*/
386$atomic_f void $barrier_destroy($barrier barrier);
387/*@ depends_on \nothing;
388 @ reads \nothing;
389 @ assigns \nothing;
390 @*/
391$atomic_f $gcollator $gcollator_create($scope scope);
392/*@ depends_on \write(gcollator);
393 @ assigns gcollator;
394 @ reads \nothing;
395 @*/
396$atomic_f int $gcollator_destroy($gcollator gcollator);
397/*@ depends_on \nothing;
398 @ executes_when $true;
399 @*/
400$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
401/*@ depends_on \write(collator);
402 @ executes_when $true;
403 @*/
404$atomic_f void $collator_destroy($collator collator);
405//========================= seq.cvh ========================
406/*@ depends_on \write(array);
407 @ executes_when $true;
408 @*/
409$system[seq] int $seq_length(void* array);
410/*@ depends_on \write(array, value);
411 @ executes_when $true;
412 @*/
413$system[seq] void $seq_init(void* array, int count, void* value);
414/*@ depends_on \write(array, values);
415 @ executes_when $true;
416 @*/
417$system[seq] void $seq_insert(void* array, int index, void* values, int count);
418/*@ depends_on \write(array, values);
419 @*/
420$atomic_f void $seq_append(void* array, void* values, int count);
421//===================== concurrency.cvl ====================
422struct _gbarrier{
423 int nprocs;
424 $proc proc_map[];
425 _Bool in_barrier[];
426 int num_in_barrier;
427};
428struct _barrier{
429 int place;
430 $gbarrier gbarrier;
431};
432struct _collator_entry{
433 $bundle entries;
434 _Bool marks[];
435 int numMarked;
436};
437struct _gcollator{
438 int length;
439 $collator_entry entries[];
440};
441struct _collator{
442 $gcollator gcollator;
443};
444/*@ depends_on \nothing;
445 @ assigns \nothing;
446 @ reads \nothing;
447 @*/
448$atomic_f $gbarrier $gbarrier_create($scope scope, int size)
449{
450 $gbarrier gbarrier = ($gbarrier)($malloc(scope, sizeof(struct _gbarrier)));
451 (gbarrier)->nprocs = size;
452 (gbarrier)->proc_map = ($proc[size]) $lambda (int i) $proc_null;
453 (gbarrier)->in_barrier = (_Bool[size]) $lambda (int i) $false;
454 (gbarrier)->num_in_barrier = 0;
455 return gbarrier;
456}
457/*@ depends_on \write(gbarrier);
458 @ reads \nothing;
459 @ assigns gbarrier;
460 @*/
461$atomic_f void $gbarrier_destroy($gbarrier gbarrier)
462{
463 $free(gbarrier);
464}
465/*@ depends_on \nothing;
466 @ assigns gbarrier;
467 @ reads gbarrier;
468 @*/
469$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place)
470{
471 $assert(((gbarrier)->proc_map[place]) == $proc_null, "the place %d in the global barrier has already been taken.", place);
472 $barrier barrier = ($barrier)($malloc(scope, sizeof(struct _barrier)));
473 (barrier)->place = place;
474 (barrier)->gbarrier = gbarrier;
475 (gbarrier)->proc_map[place] = $self;
476 return barrier;
477}
478/*@ depends_on \write(barrier);
479 @ assigns barrier;
480 @ reads \nothing;
481 @*/
482$atomic_f void $barrier_destroy($barrier barrier)
483{
484 $free(barrier);
485}
486/*@ depends_on \nothing;
487 @ reads \nothing;
488 @ assigns \nothing;
489 @*/
490$atomic_f $gcollator $gcollator_create($scope scope)
491{
492 $gcollator gcollator = ($gcollator)($malloc(scope, sizeof(struct _gcollator)));
493 (gcollator)->length = 0;
494 $seq_init(&((gcollator)->entries), 0, (void*)0);
495 return gcollator;
496}
497/*@ depends_on \write(gcollator);
498 @ assigns gcollator;
499 @ reads \nothing;
500 @*/
501$atomic_f int $gcollator_destroy($gcollator gcollator)
502{
503 int numRemaining = (gcollator)->length;
504 $free(gcollator);
505 return numRemaining;
506}
507/*@ depends_on \nothing;
508 @ executes_when $true;
509 @*/
510$atomic_f $collator $collator_create($scope scope, $gcollator gcollator)
511{
512 $collator collator = ($collator)($malloc(scope, sizeof(struct _collator)));
513 (collator)->gcollator = gcollator;
514 return collator;
515}
516/*@ depends_on \write(collator);
517 @ executes_when $true;
518 @*/
519$atomic_f void $collator_destroy($collator collator)
520{
521 $free(collator);
522}
523//======================== civlc.cvh =======================
524/*@ depends_on \nothing;
525 @ executes_when $true;
526 @*/
527$system[civlc] void $assert(_Bool expr, ...);
528/*@ depends_on \nothing;
529 @ executes_when $true;
530 @*/
531$system[civlc] void $assume(_Bool expr);
532/*@ pure;
533 @ depends_on \nothing;
534 @ executes_when $true;
535 @*/
536$system[civlc] void $elaborate(int x);
537/*@ depends_on \nothing;
538 @ executes_when $true;
539 @*/
540$system[civlc] void* $malloc($scope s, int size);
541/*@ depends_on \write(p);
542 @ executes_when $true;
543 @*/
544$system[civlc] void $free(void* p);
545//======================= bundle.cvh =======================
546/*@ depends_on \write(ptr);
547 @ executes_when $true;
548 @*/
549$system[bundle] $bundle $bundle_pack(void* ptr, int size);
550/*@ depends_on \write(ptr);
551 @ executes_when $true;
552 @*/
553$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
554//===================== concurrency.cvh ====================
555/*@ depends_on \nothing;
556 @ assigns \nothing;
557 @ reads \nothing;
558 @*/
559$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
560/*@ depends_on \write(gbarrier);
561 @ reads \nothing;
562 @ assigns gbarrier;
563 @*/
564$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
565/*@ depends_on \nothing;
566 @ assigns gbarrier;
567 @ reads gbarrier;
568 @*/
569$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
570/*@ depends_on \write(barrier);
571 @ assigns barrier;
572 @ reads \nothing;
573 @*/
574$atomic_f void $barrier_destroy($barrier barrier);
575/*@ depends_on \nothing;
576 @ reads \nothing;
577 @ assigns \nothing;
578 @*/
579$atomic_f $gcollator $gcollator_create($scope scope);
580/*@ depends_on \write(gcollator);
581 @ assigns gcollator;
582 @ reads \nothing;
583 @*/
584$atomic_f int $gcollator_destroy($gcollator gcollator);
585/*@ depends_on \nothing;
586 @ executes_when $true;
587 @*/
588$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
589/*@ depends_on \write(collator);
590 @ executes_when $true;
591 @*/
592$atomic_f void $collator_destroy($collator collator);
593//======================== comm.cvh ========================
594/*@ pure;
595 @ depends_on \nothing;
596 @ executes_when $true;
597 @*/
598$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
599/*@ pure;
600 @ depends_on \nothing;
601 @ executes_when $true;
602 @*/
603$atomic_f int $message_source($message message);
604/*@ pure;
605 @ depends_on \nothing;
606 @ executes_when $true;
607 @*/
608$atomic_f int $message_tag($message message);
609/*@ pure;
610 @ depends_on \nothing;
611 @ executes_when $true;
612 @*/
613$atomic_f int $message_dest($message message);
614/*@ pure;
615 @ depends_on \nothing;
616 @ executes_when $true;
617 @*/
618$atomic_f int $message_size($message message);
619/*@ depends_on \write(buf);
620 @ executes_when $true;
621 @*/
622$atomic_f void $message_unpack($message message, void* buf, int size);
623/*@ depends_on \nothing;
624 @ assigns \nothing;
625 @ reads \nothing;
626 @*/
627$atomic_f $gcomm $gcomm_create($scope scope, int size);
628/*@ depends_on \write(junkMsgs), \write(gcomm);
629 @ assigns junkMsgs, gcomm;
630 @*/
631$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
632$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
633/*@ depends_on \write(comm);
634 @ assigns comm;
635 @ reads \nothing;
636 @*/
637$atomic_f void $comm_destroy($comm comm);
638/*@ pure;
639 @ depends_on \nothing;
640 @*/
641$atomic_f int $comm_size($comm comm);
642/*@ pure;
643 @ depends_on \nothing;
644 @ executes_when $true;
645 @*/
646$atomic_f int $comm_place($comm comm);
647/*@ depends_on \write(comm);
648 @ executes_when $true;
649 @*/
650$system[comm] void $comm_enqueue($comm comm, $message message);
651/*@ pure;
652 @ depends_on \write(comm);
653 @ executes_when $true;
654 @*/
655$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
656/*@ depends_on \write(comm);
657 @ executes_when $comm_probe(comm, source, tag);
658 @*/
659$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
660//====================== civl-mpi.cvh ======================
661int sizeofDatatype(MPI_Datatype);
662$mpi_gcomm $mpi_gcomm_create($scope, int);
663void $mpi_gcomm_destroy($mpi_gcomm);
664MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
665void $mpi_comm_destroy(MPI_Comm, $mpi_state);
666int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
667int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
668$system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
669//========================= seq.cvh ========================
670/*@ depends_on \write(array);
671 @ executes_when $true;
672 @*/
673$system[seq] int $seq_length(void* array);
674/*@ depends_on \write(array, value);
675 @ executes_when $true;
676 @*/
677$system[seq] void $seq_init(void* array, int count, void* value);
678/*@ depends_on \write(array, values);
679 @ executes_when $true;
680 @*/
681$system[seq] void $seq_insert(void* array, int index, void* values, int count);
682/*@ depends_on \write(array, values);
683 @*/
684$atomic_f void $seq_append(void* array, void* values, int count);
685//====================== civl-mpi.cvl ======================
686char* getCoroutineName(int tag);
687struct $mpi_gcomm{
688 $gcomm p2p;
689 $gcomm col;
690 $gcollator gcollator;
691 $gbarrier gbarrier;
692};
693int sizeofDatatype(MPI_Datatype datatype)
694{
695 switch (datatype)
696 {
697 case MPI_INT:
698 return sizeof(int);
699 case MPI_2INT:
700 return sizeof(int) * 2;
701 case MPI_FLOAT:
702 return sizeof(float);
703 case MPI_DOUBLE:
704 return sizeof(double);
705 case MPI_CHAR:
706 return sizeof(char);
707 case MPI_BYTE:
708 return sizeof(char);
709 case MPI_SHORT:
710 return sizeof(short);
711 case MPI_LONG:
712 return sizeof(long);
713 case MPI_LONG_DOUBLE:
714 return sizeof(long double);
715 case MPI_LONG_LONG_INT:
716 return sizeof(long long);
717 case MPI_LONG_LONG:
718 return sizeof(long long);
719 case MPI_UNSIGNED_LONG_LONG:
720 return sizeof(unsigned long long);
721 default:
722 $assert(0, "Unreachable");
723 }
724}
725$mpi_gcomm $mpi_gcomm_create($scope scope, int size)
726{
727 $mpi_gcomm result;
728 result.p2p = $gcomm_create(scope, size);
729 result.col = $gcomm_create(scope, size);
730 result.gcollator = $gcollator_create(scope);
731 result.gbarrier = $gbarrier_create(scope, size);
732 return result;
733}
734void $mpi_gcomm_destroy($mpi_gcomm gc)
735{
736 int numJunkRecord;
737 int numJunkMsg;
738 $message junkMsgs[];
739 $seq_init(&(junkMsgs), 0, (void*)0);
740 numJunkMsg = $gcomm_destroy(gc.p2p, &(junkMsgs));
741 {
742 int i = 0;
743 for (; i < numJunkMsg; i = i + 1)
744 {
745 int src;
746 int dest;
747 int tag;
748 src = $message_source(junkMsgs[i]);
749 dest = $message_dest(junkMsgs[i]);
750 tag = $message_tag(junkMsgs[i]);
751 $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);
752 }
753 }
754 numJunkMsg = $gcomm_destroy(gc.col, &(junkMsgs));
755 {
756 int i = 0;
757 for (; i < numJunkMsg; i = i + 1)
758 {
759 int src;
760 int tag;
761 char* routine;
762 src = $message_source(junkMsgs[i]);
763 tag = $message_tag(junkMsgs[i]);
764 routine = getCoroutineName(tag);
765 $assert($false, "MPI message leak: There is a message sent by rank %d for collective routine %s that is never received.", src, routine);
766 }
767 }
768 numJunkRecord = $gcollator_destroy(gc.gcollator);
769 $gbarrier_destroy(gc.gbarrier);
770 $assert(numJunkRecord == 0, "MPI collective routines are called inappropriately because there are %d collective records still remaining the collective routine checker.", numJunkRecord);
771}
772MPI_Comm $mpi_comm_create($scope scope, $mpi_gcomm gc, int rank)
773{
774 MPI_Comm result;
775 result.p2p = $comm_create(scope, gc.p2p, rank);
776 result.col = $comm_create(scope, gc.col, rank);
777 result.collator = $collator_create(scope, gc.gcollator);
778 result.barrier = $barrier_create(scope, gc.gbarrier, rank);
779 result.gcommIndex = 0;
780 return result;
781}
782void $mpi_comm_destroy(MPI_Comm comm, $mpi_state mpi_state)
783{
784 if (comm.gcommIndex == 0)
785 $assert(mpi_state == _MPI_FINALIZED, "Process terminates without calling MPI_Finalize() first.");
786 $comm_destroy(comm.p2p);
787 $comm_destroy(comm.col);
788 $collator_destroy(comm.collator);
789 $barrier_destroy(comm.barrier);
790}
791int $mpi_send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm)
792{
793 if (dest >= 0)
794 {
795 int $sef$0 = sizeofDatatype(datatype);
796 int size = count * $sef$0;
797 int place = $comm_place(comm.p2p);
798 $message out = $message_pack(place, dest, tag, buf, size);
799 $comm_enqueue(comm.p2p, out);
800 }
801 return 0;
802}
803int $mpi_recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status)
804{
805 if ((source >= 0) || (source == (-1)))
806 {
807 $message in;
808 int place = $comm_place(comm.p2p);
809 int deterministicTag;
810 $assert((tag == (-2)) || (tag >= 0), "Illegal MPI message receive tag %d.\n", tag);
811 deterministicTag = tag < 0 ? -2 : tag;
812 $elaborate(source);
813 in = $comm_dequeue(comm.p2p, source, deterministicTag);
814 int $sef$1 = sizeofDatatype(datatype);
815 int size = count * $sef$1;
816 $message_unpack(in, buf, size);
817 if (status != (void*)0)
818 {
819 (status)->size = $message_size(in);
820 (status)->MPI_SOURCE = $message_source(in);
821 (status)->MPI_TAG = $message_tag(in);
822 (status)->MPI_ERROR = 0;
823 }
824 }
825 return 0;
826}
827char* getCoroutineName(int tag)
828{
829 switch (tag)
830 {
831 case 9999:
832 return "MPI_Bcast";
833 case 9998:
834 return "MPI_Reduce";
835 case 9997:
836 return "MPI_Allreduce";
837 case 9996:
838 return "MPI_Gather";
839 case 9995:
840 return "MPI_Scatter";
841 case 9994:
842 return "MPI_Gatherv";
843 case 9993:
844 return "MPI_Scatterv";
845 case 9992:
846 return "MPI_Allgather";
847 case 9991:
848 return "MPI_Reduce_scatter";
849 case 9990:
850 return "MPI_Alltoall";
851 case 9989:
852 return "MPI_Alltoallv";
853 case 9988:
854 return "MPI_Alltoallw";
855 case 9987:
856 return "MPI_Barrier";
857 case 9986:
858 return "MPI_Commdup";
859 case 9985:
860 return "MPI_Commfree";
861 default:
862 $assert($false, "Internal Error: Unexpected MPI routine tag:%d.\n", tag);
863 }
864}
865//======================== civlc.cvh =======================
866/*@ depends_on \nothing;
867 @ executes_when $true;
868 @*/
869$system[civlc] void $assert(_Bool expr, ...);
870/*@ depends_on \nothing;
871 @ executes_when $true;
872 @*/
873$system[civlc] void $assume(_Bool expr);
874/*@ pure;
875 @ depends_on \nothing;
876 @ executes_when $true;
877 @*/
878$system[civlc] void $elaborate(int x);
879/*@ depends_on \nothing;
880 @ executes_when $true;
881 @*/
882$system[civlc] void* $malloc($scope s, int size);
883/*@ depends_on \write(p);
884 @ executes_when $true;
885 @*/
886$system[civlc] void $free(void* p);
887//======================= bundle.cvh =======================
888/*@ depends_on \write(ptr);
889 @ executes_when $true;
890 @*/
891$system[bundle] $bundle $bundle_pack(void* ptr, int size);
892/*@ depends_on \write(ptr);
893 @ executes_when $true;
894 @*/
895$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
896//======================== comm.cvh ========================
897/*@ pure;
898 @ depends_on \nothing;
899 @ executes_when $true;
900 @*/
901$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
902/*@ pure;
903 @ depends_on \nothing;
904 @ executes_when $true;
905 @*/
906$atomic_f int $message_source($message message);
907/*@ pure;
908 @ depends_on \nothing;
909 @ executes_when $true;
910 @*/
911$atomic_f int $message_tag($message message);
912/*@ pure;
913 @ depends_on \nothing;
914 @ executes_when $true;
915 @*/
916$atomic_f int $message_dest($message message);
917/*@ pure;
918 @ depends_on \nothing;
919 @ executes_when $true;
920 @*/
921$atomic_f int $message_size($message message);
922/*@ depends_on \write(buf);
923 @ executes_when $true;
924 @*/
925$atomic_f void $message_unpack($message message, void* buf, int size);
926/*@ depends_on \nothing;
927 @ assigns \nothing;
928 @ reads \nothing;
929 @*/
930$atomic_f $gcomm $gcomm_create($scope scope, int size);
931/*@ depends_on \write(junkMsgs), \write(gcomm);
932 @ assigns junkMsgs, gcomm;
933 @*/
934$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
935$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
936/*@ depends_on \write(comm);
937 @ assigns comm;
938 @ reads \nothing;
939 @*/
940$atomic_f void $comm_destroy($comm comm);
941/*@ pure;
942 @ depends_on \nothing;
943 @*/
944$atomic_f int $comm_size($comm comm);
945/*@ pure;
946 @ depends_on \nothing;
947 @ executes_when $true;
948 @*/
949$atomic_f int $comm_place($comm comm);
950/*@ depends_on \write(comm);
951 @ executes_when $true;
952 @*/
953$system[comm] void $comm_enqueue($comm comm, $message message);
954/*@ pure;
955 @ depends_on \write(comm);
956 @ executes_when $true;
957 @*/
958$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
959/*@ depends_on \write(comm);
960 @ executes_when $comm_probe(comm, source, tag);
961 @*/
962$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
963//========================= seq.cvh ========================
964/*@ depends_on \write(array);
965 @ executes_when $true;
966 @*/
967$system[seq] int $seq_length(void* array);
968/*@ depends_on \write(array, value);
969 @ executes_when $true;
970 @*/
971$system[seq] void $seq_init(void* array, int count, void* value);
972/*@ depends_on \write(array, values);
973 @ executes_when $true;
974 @*/
975$system[seq] void $seq_insert(void* array, int index, void* values, int count);
976/*@ depends_on \write(array, values);
977 @*/
978$atomic_f void $seq_append(void* array, void* values, int count);
979//======================== comm.cvl ========================
980struct _queue{
981 int length;
982 $message messages[];
983};
984struct _gcomm{
985 int nprocs;
986 $proc procs[];
987 _Bool isInit[];
988 $queue buf[][];
989};
990struct _comm{
991 int place;
992 $gcomm gcomm;
993};
994/*@ depends_on \write(data);
995 @*/
996$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size)
997{
998 $message result;
999 result.source = source;
1000 result.dest = dest;
1001 result.tag = tag;
1002 result.data = $bundle_pack(data, size);
1003 result.size = size;
1004 return result;
1005}
1006int $message_source($message message)
1007{
1008 return message.source;
1009}
1010int $message_tag($message message)
1011{
1012 return message.tag;
1013}
1014int $message_dest($message message)
1015{
1016 return message.dest;
1017}
1018int $message_size($message message)
1019{
1020 return message.size;
1021}
1022/*@ depends_on \write(buf);
1023 @*/
1024$atomic_f void $message_unpack($message message, void* buf, int size)
1025{
1026 $bundle_unpack(message.data, buf);
1027 $assert(message.size <= size, "Message of size %d exceeds the specified size %d.", message.size, size);
1028}
1029/*@ depends_on \nothing;
1030 @ assigns \nothing;
1031 @ reads \nothing;
1032 @*/
1033$atomic_f $gcomm $gcomm_create($scope scope, int size)
1034{
1035 $gcomm gcomm = ($gcomm)($malloc(scope, sizeof(struct _gcomm)));
1036 $queue empty;
1037 empty.length = 0;
1038 $seq_init(&(empty.messages), 0, (void*)0);
1039 (gcomm)->nprocs = size;
1040 (gcomm)->procs = ($proc[size]) $lambda (int i) $proc_null;
1041 (gcomm)->isInit = (_Bool[size]) $lambda (int i) $false;
1042 (gcomm)->buf = (($queue[size][size]) $lambda (int i, j) empty);
1043 return gcomm;
1044}
1045/*@ depends_on \write(junkMsgs), \write(gcomm);
1046 @ assigns junkMsgs, gcomm;
1047 @ reads \nothing;
1048 @*/
1049$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs)
1050{
1051 int nprocs = (gcomm)->nprocs;
1052 int numJunks = 0;
1053 if (junkMsgs != (void*)0)
1054 {
1055 {
1056 int i = 0;
1057 for (; i < nprocs; i = i + 1)
1058 {
1059 int j = 0;
1060 for (; j < nprocs; j = j + 1)
1061 {
1062 $queue queue = (gcomm)->buf[i][j];
1063 if (queue.length > 0)
1064 $seq_append(junkMsgs, queue.messages, queue.length);
1065 }
1066 }
1067 }
1068 numJunks = $seq_length(junkMsgs);
1069 }
1070 $free(gcomm);
1071 return numJunks;
1072}
1073/*@ depends_on \nothing;
1074 @ reads gcomm;
1075 @ assigns gcomm;
1076 @*/
1077$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place)
1078{
1079 $assert(!((gcomm)->isInit[place]), "the place %d is already occupied in the global communicator!", place);
1080 $comm comm = ($comm)($malloc(scope, sizeof(struct _comm)));
1081 (gcomm)->procs[place] = $self;
1082 (gcomm)->isInit[place] = $true;
1083 (comm)->gcomm = gcomm;
1084 (comm)->place = place;
1085 return comm;
1086}
1087/*@ depends_on \write(comm);
1088 @ assigns comm;
1089 @ reads \nothing;
1090 @*/
1091$atomic_f void $comm_destroy($comm comm)
1092{
1093 $free(comm);
1094}
1095/*@ pure;
1096 @ depends_on \nothing;
1097 @*/
1098$atomic_f int $comm_place($comm comm)
1099{
1100 return (comm)->place;
1101}
1102/*@ pure;
1103 @ depends_on \nothing;
1104 @*/
1105$atomic_f int $comm_size($comm comm)
1106{
1107 return ((comm)->gcomm)->nprocs;
1108}
1109//======================== civlc.cvh =======================
1110/*@ depends_on \nothing;
1111 @ executes_when $true;
1112 @*/
1113$system[civlc] void $assert(_Bool expr, ...);
1114/*@ depends_on \nothing;
1115 @ executes_when $true;
1116 @*/
1117$system[civlc] void $assume(_Bool expr);
1118/*@ pure;
1119 @ depends_on \nothing;
1120 @ executes_when $true;
1121 @*/
1122$system[civlc] void $elaborate(int x);
1123/*@ depends_on \nothing;
1124 @ executes_when $true;
1125 @*/
1126$system[civlc] void* $malloc($scope s, int size);
1127/*@ depends_on \write(p);
1128 @ executes_when $true;
1129 @*/
1130$system[civlc] void $free(void* p);
1131//========================= seq.cvh ========================
1132/*@ depends_on \write(array);
1133 @ executes_when $true;
1134 @*/
1135$system[seq] int $seq_length(void* array);
1136/*@ depends_on \write(array, value);
1137 @ executes_when $true;
1138 @*/
1139$system[seq] void $seq_init(void* array, int count, void* value);
1140/*@ depends_on \write(array, values);
1141 @ executes_when $true;
1142 @*/
1143$system[seq] void $seq_insert(void* array, int index, void* values, int count);
1144/*@ depends_on \write(array, values);
1145 @*/
1146$atomic_f void $seq_append(void* array, void* values, int count);
1147//========================= seq.cvl ========================
1148/*@ depends_on \write(array, values);
1149 @*/
1150$atomic_f void $seq_append(void* array, void* values, int count)
1151{
1152 int length = $seq_length(array);
1153 $seq_insert(array, length, values, count);
1154}
1155//======================== civlc.cvh =======================
1156/*@ depends_on \nothing;
1157 @ executes_when $true;
1158 @*/
1159$system[civlc] void $assert(_Bool expr, ...);
1160/*@ depends_on \nothing;
1161 @ executes_when $true;
1162 @*/
1163$system[civlc] void $assume(_Bool expr);
1164/*@ pure;
1165 @ depends_on \nothing;
1166 @ executes_when $true;
1167 @*/
1168$system[civlc] void $elaborate(int x);
1169/*@ depends_on \nothing;
1170 @ executes_when $true;
1171 @*/
1172$system[civlc] void* $malloc($scope s, int size);
1173/*@ depends_on \write(p);
1174 @ executes_when $true;
1175 @*/
1176$system[civlc] void $free(void* p);
1177//======================= bundle.cvh =======================
1178/*@ depends_on \write(ptr);
1179 @ executes_when $true;
1180 @*/
1181$system[bundle] $bundle $bundle_pack(void* ptr, int size);
1182/*@ depends_on \write(ptr);
1183 @ executes_when $true;
1184 @*/
1185$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
1186//======================== civlc.cvh =======================
1187/*@ depends_on \nothing;
1188 @ executes_when $true;
1189 @*/
1190$system[civlc] void $assert(_Bool expr, ...);
1191/*@ depends_on \nothing;
1192 @ executes_when $true;
1193 @*/
1194$system[civlc] void $assume(_Bool expr);
1195/*@ pure;
1196 @ depends_on \nothing;
1197 @ executes_when $true;
1198 @*/
1199$system[civlc] void $elaborate(int x);
1200/*@ depends_on \nothing;
1201 @ executes_when $true;
1202 @*/
1203$system[civlc] void* $malloc($scope s, int size);
1204/*@ depends_on \write(p);
1205 @ executes_when $true;
1206 @*/
1207$system[civlc] void $free(void* p);
1208//========================= stdio.h ========================
1209$system[stdio] int printf(char* restrict format, ...);
1210//======================= sum_array.c ======================
1211$input int _civl_argc;
1212$assume(0 < _civl_argc);
1213$input char _civl_argv[_civl_argc][];
1214$input long NB = 20;
1215$input long N;
1216//===================== MPITransformer =====================
1217$input int _mpi_nprocs;
1218$input int _mpi_nprocs_lo = 1;
1219//======================= sum_array.c ======================
1220$input int _mpi_nprocs_hi = 8;
1221//===================== MPITransformer =====================
1222$assume((_mpi_nprocs_lo <= _mpi_nprocs) && (_mpi_nprocs <= _mpi_nprocs_hi));
1223$scope _mpi_root = $here;
1224$mpi_gcomm _mpi_gcomm;
1225$mpi_gcomm _mpi_gcomms[];
1226void _mpi_process(int _mpi_rank)
1227{
1228 MPI_Comm MPI_COMM_WORLD = $mpi_comm_create($here, _mpi_gcomm, _mpi_rank);
1229 $system[sum_array] void $assume(_Bool expression);
1230 $mpi_state _mpi_state = _MPI_UNINIT;
1231 int $mpi_init(void)
1232 {
1233 $assert(_mpi_state == _MPI_UNINIT, "Process can only call MPI_Init() at most once.");
1234 _mpi_state = _MPI_INIT;
1235 return 0;
1236 }
1237 int MPI_Finalize(void)
1238 {
1239 $assert(_mpi_state == _MPI_INIT, "Process can only call MPI_Finalize() after the MPI enviroment is created and before cleaned.");
1240 _mpi_state = _MPI_FINALIZED;
1241 return 0;
1242 }
1243 int MPI_Comm_size(MPI_Comm comm, int* size)
1244 {
1245 $assert(_mpi_state == _MPI_INIT, "MPI_Comm_size() cannot be invoked without MPI_Init() being called before.\n");
1246 *size = $comm_size(comm.p2p);
1247 return 0;
1248 }
1249 int MPI_Comm_rank(MPI_Comm comm, int* rank)
1250 {
1251 $assert(_mpi_state == _MPI_INIT, "MPI_Comm_rank() cannot be invoked without MPI_Init() being called before.\n");
1252 *rank = $comm_place(comm.p2p);
1253 return 0;
1254 }
1255 int MPI_Send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm)
1256 {
1257 $assert(_mpi_state == _MPI_INIT, "MPI_Send() cannot be invoked without MPI_Init() being called before.\n");
1258 $mpi_check_buffer(buf, count, datatype);
1259 int $sef$2 = $mpi_send(buf, count, datatype, dest, tag, comm);
1260 return $sef$2;
1261 }
1262 int MPI_Recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status)
1263 {
1264 $assert(_mpi_state == _MPI_INIT, "MPI_Recv() cannot be invoked without MPI_Init() being called before.\n");
1265 int $sef$3 = $mpi_recv(buf, count, datatype, source, tag, comm, status);
1266 return $sef$3;
1267 }
1268 int MPI_Get_count(MPI_Status* status, MPI_Datatype datatype, int* count)
1269 {
1270 $assert(_mpi_state == _MPI_INIT, "MPI_Get_count() cannot be invoked without MPI_Init() being called before.\n");
1271 int $sef$4 = sizeofDatatype(datatype);
1272 *count = $int_div((status)->size, $sef$4);
1273 return 0;
1274 }
1275 $assume((0 < N) && (N <= NB));
1276 double oracle;
1277 void master(void);
1278 void slave(void);
1279 int _civl_main(int argc, char** argv)
1280 {
1281 int myrank;
1282 $mpi_init();
1283 MPI_Comm_rank(MPI_COMM_WORLD, &(myrank));
1284 if (!myrank)
1285 master();
1286 else
1287 slave();
1288 MPI_Finalize();
1289 return 0;
1290 }
1291 void master(void)
1292 {
1293 float array[N];
1294 double mysum;
1295 double tmpsum;
1296 unsigned long long step;
1297 unsigned long long i;
1298 int size;
1299 MPI_Status status;
1300 for (i = 0; i < N; i = i + 1)
1301 array[i] = i + 1;
1302 oracle = 0.0;
1303 for (i = 0; i < N; i = i + 1)
1304 oracle = oracle + (array[i]);
1305 MPI_Comm_size(MPI_COMM_WORLD, &(size));
1306 if (size != 1)
1307 step = $int_div(N, size - 1);
1308 else
1309 step = N;
1310 for (i = 0; i < (size - 1); i = i + 1)
1311 MPI_Send(array + (i * step), step, MPI_FLOAT, i + 1, 100, MPI_COMM_WORLD);
1312 {
1313 i = (size - 1) * step;
1314 mysum = 0;
1315 for (; i < N; i = i + 1)
1316 mysum = mysum + (array[i]);
1317 }
1318 for (i = 1; i < size; )
1319 {
1320 MPI_Recv(&(tmpsum), 1, MPI_DOUBLE, -1, 101, MPI_COMM_WORLD, &(status));
1321 mysum = mysum + tmpsum;
1322 i = i + 1;
1323 }
1324 $assert(oracle == mysum, "The sum of %d array elements is %f but the expected one is %f.\n", N, mysum, oracle);
1325 printf("%lf\n", mysum);
1326 }
1327 void slave(void)
1328 {
1329 float array[N];
1330 double sum;
1331 unsigned long long i;
1332 int count;
1333 MPI_Status status;
1334 MPI_Recv(array, N, MPI_FLOAT, 0, 100, MPI_COMM_WORLD, &(status));
1335 MPI_Get_count(&(status), MPI_FLOAT, &(count));
1336 {
1337 i = 0;
1338 sum = 0;
1339 for (; i < count; i = i + 1)
1340 sum = sum + (array[i]);
1341 }
1342 MPI_Send(&(sum), 1, MPI_DOUBLE, 0, 101, MPI_COMM_WORLD);
1343 }
1344 {
1345 _civl_main(_civl_argc, (char*[_civl_argc]) $lambda (int i) _civl_argv[i]);
1346 }
1347 $mpi_comm_destroy(MPI_COMM_WORLD, _mpi_state);
1348}
1349int main()
1350{
1351 _mpi_gcomm = $mpi_gcomm_create(_mpi_root, _mpi_nprocs);
1352 $seq_init(&(_mpi_gcomms), 1, &(_mpi_gcomm));
1353 $parfor (int i: 0 .. _mpi_nprocs - 1)
1354 _mpi_process(i);
1355 $mpi_gcomm_destroy(_mpi_gcomm);
1356}
1357
Note: See TracBrowser for help on using the repository browser.