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

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

added tests for symoblic constants.

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