Context Navigation

auto_allgather.c@ 8b2639d

1.23 2.0 acw/focus-triggers main test-branch

Last change on this file since 8b2639d was 68c784e, checked in by Ziqing Luo <ziqing@…>, 10 years ago

implement the contract transformer

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@3429 fb995dde-84ed-4084-dfe6-e5aef3e2452c

Property mode set to 100644

File size: 145.9 KB

Line
1	CIVL v1.7.1 of 2016-05-31 -- http://vsl.cis.udel.edu/civl
2	//========================== op.h ==========================
3	typedef enum Operation{
4	_NO_OP,
5	_MAX,
6	_MIN,
7	_SUM,
8	_PROD,
9	_LAND,
10	_BAND,
11	_LOR,
12	_BOR,
13	_LXOR,
14	_BXOR,
15	_MINLOC,
16	_MAXLOC,
17	_REPLACE
18	} Operation;
19	//========================== mpi.h =========================
20	typedef enum Operation MPI_Op;
21	typedef enum MPI_Datatype{
22	MPI_CHAR,
23	MPI_CHARACTER,
24	MPI_SIGNED_CHAR,
25	MPI_UNSIGNED_CHAR,
26	MPI_BYTE,
27	MPI_WCHAR,
28	MPI_SHORT,
29	MPI_UNSIGNED_SHORT,
30	MPI_INT,
31	MPI_INT16_T,
32	MPI_INT32_T,
33	MPI_INT64_T,
34	MPI_INT8_T,
35	MPI_INTEGER,
36	MPI_INTEGER1,
37	MPI_INTEGER16,
38	MPI_INTEGER2,
39	MPI_INTEGER4,
40	MPI_INTEGER8,
41	MPI_UNSIGNED,
42	MPI_LONG,
43	MPI_UNSIGNED_LONG,
44	MPI_FLOAT,
45	MPI_DOUBLE,
46	MPI_LONG_DOUBLE,
47	MPI_LONG_LONG_INT,
48	MPI_UNSIGNED_LONG_LONG,
49	MPI_LONG_LONG,
50	MPI_PACKED,
51	MPI_LB,
52	MPI_UB,
53	MPI_UINT16_T,
54	MPI_UINT32_T,
55	MPI_UINT64_T,
56	MPI_UINT8_T,
57	MPI_FLOAT_INT,
58	MPI_DOUBLE_INT,
59	MPI_LONG_INT,
60	MPI_SHORT_INT,
61	MPI_2INT,
62	MPI_LONG_DOUBLE_INT,
63	MPI_AINT,
64	MPI_OFFSET,
65	MPI_2DOUBLE_PRECISION,
66	MPI_2INTEGER,
67	MPI_2REAL,
68	MPI_C_BOOL,
69	MPI_C_COMPLEX,
70	MPI_C_DOUBLE_COMPLEX,
71	MPI_C_FLOAT_COMPLEX,
72	MPI_C_LONG_DOUBLE_COMPLEX,
73	MPI_COMPLEX,
74	MPI_COMPLEX16,
75	MPI_COMPLEX32,
76	MPI_COMPLEX4,
77	MPI_COMPLEX8,
78	MPI_REAL,
79	MPI_REAL16,
80	MPI_REAL2,
81	MPI_REAL4,
82	MPI_REAL8
83	} MPI_Datatype;
84	typedef long MPI_Aint;
85	typedef int MPI_Fint;
86	typedef struct MPI_Comm MPI_Comm;
87	typedef struct MPI_Group MPI_Group;
88	typedef struct MPI_Request* MPI_Request;
89	typedef struct MPIX_Message MPIX_Message;
90	typedef struct MPI_File MPI_File;
91	typedef struct MPI_Errhandler MPI_Errhandler;
92	typedef struct MPI_User_function MPI_User_function;
93	typedef struct MPI_Copy_function MPI_Copy_function;
94	typedef struct MPI_Delete_function MPI_Delete_function;
95	typedef int MPI_Win;
96	typedef int MPI_Info;
97	typedef long long MPI_Offset;
98	typedef enum MPIR_Topo_type{
99	MPI_GRAPH=1,
100	MPI_CART=2,
101	MPI_DIST_GRAPH=3
102	} MPIR_Topo_type;
103	typedef enum MPIR_Combiner_enum{
104	MPI_COMBINER_NAMED=1,
105	MPI_COMBINER_DUP=2,
106	MPI_COMBINER_CONTIGUOUS=3,
107	MPI_COMBINER_VECTOR=4,
108	MPI_COMBINER_HVECTOR_INTEGER=5,
109	MPI_COMBINER_HVECTOR=6,
110	MPI_COMBINER_INDEXED=7,
111	MPI_COMBINER_HINDEXED_INTEGER=8,
112	MPI_COMBINER_HINDEXED=9,
113	MPI_COMBINER_INDEXED_BLOCK=10,
114	MPIX_COMBINER_HINDEXED_BLOCK=11,
115	MPI_COMBINER_STRUCT_INTEGER=12,
116	MPI_COMBINER_STRUCT=13,
117	MPI_COMBINER_SUBARRAY=14,
118	MPI_COMBINER_DARRAY=15,
119	MPI_COMBINER_F90_REAL=16,
120	MPI_COMBINER_F90_COMPLEX=17,
121	MPI_COMBINER_F90_INTEGER=18,
122	MPI_COMBINER_RESIZED=19
123	} MPIR_Combiner_enum;
124	typedef (void (MPI_Comm, int)) MPI_Handler_function;
125	typedef (int (MPI_Comm, int, void, void, void, int)) MPI_Comm_copy_attr_function;
126	typedef (int (MPI_Comm, int, void, void)) MPI_Comm_delete_attr_function;
127	typedef (int (MPI_Datatype, int, void, void, void, int)) MPI_Type_copy_attr_function;
128	typedef (int (MPI_Datatype, int, void, void)) MPI_Type_delete_attr_function;
129	typedef (int (MPI_Win, int, void, void, void, int)) MPI_Win_copy_attr_function;
130	typedef (int (MPI_Win, int, void, void)) MPI_Win_delete_attr_function;
131	typedef (void (MPI_Comm, int)) MPI_Comm_errhandler_function;
132	typedef (void (MPI_File, int)) MPI_File_errhandler_function;
133	typedef (void (MPI_Win, int)) MPI_Win_errhandler_function;
134	typedef MPI_Comm_errhandler_function MPI_Comm_errhandler_fn;
135	typedef MPI_File_errhandler_function MPI_File_errhandler_fn;
136	typedef MPI_Win_errhandler_function MPI_Win_errhandler_fn;
137	typedef (int (void, MPI_Datatype, int, void, MPI_Offset, void*)) MPI_Datarep_conversion_function;
138	typedef (int (MPI_Datatype datatype, MPI_Aint, void)) MPI_Datarep_extent_function;
139	typedef struct MPI_Status{
140	int MPI_SOURCE;
141	int MPI_TAG;
142	int MPI_ERROR;
143	int size;
144	} MPI_Status;
145	typedef (int (void*, int)) MPI_Grequest_cancel_function;
146	typedef (int (void*)) MPI_Grequest_free_function;
147	typedef (int (void, MPI_Status)) MPI_Grequest_query_function;
148	MPI_Comm MPI_COMM_WORLD;
149	MPI_Comm MPI_COMM_SELF;
150	MPI_Comm MPI_COMM_PARENT;
151	MPI_Comm MPI_COMM_TYPE_SHARED;
152	int MPI_Send(void*, int, MPI_Datatype, int, int, MPI_Comm);
153	int MPI_Recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
154	int MPI_Get_count(MPI_Status, MPI_Datatype, int);
155	int MPI_Bsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
156	int MPI_Ssend(void*, int, MPI_Datatype, int, int, MPI_Comm);
157	int MPI_Rsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
158	int MPI_Buffer_attach(void*, int);
159	int MPI_Buffer_detach(void, int);
160	int MPI_Isend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
161	int MPI_Ibsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
162	int MPI_Issend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
163	int MPI_Irsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
164	int MPI_Irecv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
165	int MPI_Wait(MPI_Request, MPI_Status);
166	int MPI_Test(MPI_Request, int, MPI_Status*);
167	int MPI_Request_free(MPI_Request*);
168	int MPI_Waitany(int, MPI_Request, int, MPI_Status*);
169	int MPI_Testany(int, MPI_Request, int, int, MPI_Status);
170	int MPI_Waitall(int, MPI_Request, MPI_Status);
171	int MPI_Testall(int, MPI_Request, int, MPI_Status*);
172	int MPI_Waitsome(int, MPI_Request, int, int, MPI_Status);
173	int MPI_Testsome(int, MPI_Request, int, int, MPI_Status);
174	int MPI_Iprobe(int, int, MPI_Comm, int, MPI_Status);
175	int MPI_Probe(int, int, MPI_Comm, MPI_Status*);
176	int MPI_Cancel(MPI_Request*);
177	int MPI_Test_cancelled(MPI_Status, int);
178	int MPI_Send_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
179	int MPI_Bsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
180	int MPI_Ssend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
181	int MPI_Rsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
182	int MPI_Recv_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
183	int MPI_Start(MPI_Request*);
184	int MPI_Startall(int, MPI_Request*);
185	int MPI_Sendrecv(void, int, MPI_Datatype, int, int, void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
186	int MPI_Sendrecv_replace(void, int, MPI_Datatype, int, int, int, int, MPI_Comm, MPI_Status);
187	int MPI_Type_contiguous(int, MPI_Datatype, MPI_Datatype*);
188	int MPI_Type_vector(int, int, int, MPI_Datatype, MPI_Datatype*);
189	int MPI_Type_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
190	int MPI_Type_indexed(int, int, int, MPI_Datatype, MPI_Datatype*);
191	int MPI_Type_hindexed(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
192	int MPI_Type_struct(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype);
193	int MPI_Address(void, MPI_Aint);
194	int MPI_Type_extent(MPI_Datatype, MPI_Aint*);
195	int MPI_Type_size(MPI_Datatype, int*);
196	int MPI_Type_lb(MPI_Datatype, MPI_Aint*);
197	int MPI_Type_ub(MPI_Datatype, MPI_Aint*);
198	int MPI_Type_commit(MPI_Datatype*);
199	int MPI_Type_free(MPI_Datatype*);
200	int MPI_Get_elements(MPI_Status, MPI_Datatype, int);
201	int MPI_Pack(void, int, MPI_Datatype, void, int, int*, MPI_Comm);
202	int MPI_Unpack(void, int, int, void*, int, MPI_Datatype, MPI_Comm);
203	int MPI_Pack_size(int, MPI_Datatype, MPI_Comm, int*);
204	int MPI_Barrier(MPI_Comm);
205	int MPI_Bcast(void*, int, MPI_Datatype, int, MPI_Comm);
206	int MPI_Gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
207	int MPI_Gatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, int, MPI_Comm);
208	int MPI_Scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
209	int MPI_Scatterv(void, int, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
210	int MPI_Allgather(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
211	int MPI_Allgatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
212	int MPI_Alltoall(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
213	int MPI_Alltoallv(void, int, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
214	int MPI_Reduce(void, void, int, MPI_Datatype, MPI_Op, int, MPI_Comm);
215	int MPI_Op_create(MPI_User_function, int, MPI_Op);
216	int MPI_Op_free(MPI_Op*);
217	int MPI_Allreduce(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
218	int MPI_Reduce_scatter(void, void, int*, MPI_Datatype, MPI_Op, MPI_Comm);
219	int MPI_Scan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
220	int MPI_Group_size(MPI_Group, int*);
221	int MPI_Group_rank(MPI_Group, int*);
222	int MPI_Group_translate_ranks(MPI_Group, int, int, MPI_Group, int);
223	int MPI_Group_compare(MPI_Group, MPI_Group, int*);
224	int MPI_Comm_group(MPI_Comm, MPI_Group*);
225	int MPI_Group_union(MPI_Group, MPI_Group, MPI_Group*);
226	int MPI_Group_intersection(MPI_Group, MPI_Group, MPI_Group*);
227	int MPI_Group_difference(MPI_Group, MPI_Group, MPI_Group*);
228	int MPI_Group_incl(MPI_Group, int, int, MPI_Group);
229	int MPI_Group_excl(MPI_Group, int, int, MPI_Group);
230	int MPI_Group_range_incl(MPI_Group, int, int [][3], MPI_Group*);
231	int MPI_Group_range_excl(MPI_Group, int, int [][3], MPI_Group*);
232	int MPI_Group_free(MPI_Group*);
233	int MPI_Comm_size(MPI_Comm, int*);
234	int MPI_Comm_rank(MPI_Comm, int*);
235	int MPI_Comm_compare(MPI_Comm, MPI_Comm, int*);
236	int MPI_Comm_dup(MPI_Comm, MPI_Comm*);
237	int MPI_Comm_create(MPI_Comm, MPI_Group, MPI_Comm*);
238	int MPI_Comm_split(MPI_Comm, int, int, MPI_Comm*);
239	int MPI_Comm_free(MPI_Comm*);
240	int MPI_Comm_test_inter(MPI_Comm, int*);
241	int MPI_Comm_remote_size(MPI_Comm, int*);
242	int MPI_Comm_remote_group(MPI_Comm, MPI_Group*);
243	int MPI_Intercomm_create(MPI_Comm, int, MPI_Comm, int, int, MPI_Comm*);
244	int MPI_Intercomm_merge(MPI_Comm, int, MPI_Comm*);
245	int MPI_Keyval_create(MPI_Copy_function, MPI_Delete_function, int, void);
246	int MPI_Keyval_free(int*);
247	int MPI_Attr_put(MPI_Comm, int, void*);
248	int MPI_Attr_get(MPI_Comm, int, void, int);
249	int MPI_Attr_delete(MPI_Comm, int);
250	int MPI_Topo_test(MPI_Comm, int*);
251	int MPI_Cart_create(MPI_Comm, int, int, int, int, MPI_Comm*);
252	int MPI_Dims_create(int, int, int*);
253	int MPI_Graph_create(MPI_Comm, int, int, int, int, MPI_Comm*);
254	int MPI_Graphdims_get(MPI_Comm, int, int);
255	int MPI_Graph_get(MPI_Comm, int, int, int, int);
256	int MPI_Cartdim_get(MPI_Comm, int*);
257	int MPI_Cart_get(MPI_Comm, int, int, int, int*);
258	int MPI_Cart_rank(MPI_Comm, int, int);
259	int MPI_Cart_coords(MPI_Comm, int, int, int*);
260	int MPI_Graph_neighbors_count(MPI_Comm, int, int*);
261	int MPI_Graph_neighbors(MPI_Comm, int, int, int*);
262	int MPI_Cart_shift(MPI_Comm, int, int, int, int);
263	int MPI_Cart_sub(MPI_Comm, int, MPI_Comm);
264	int MPI_Cart_map(MPI_Comm, int, int, int, int*);
265	int MPI_Graph_map(MPI_Comm, int, int, int, int*);
266	int MPI_Get_processor_name(char, int);
267	int MPI_Get_version(int, int);
268	int MPI_Errhandler_create(MPI_Handler_function, MPI_Errhandler);
269	int MPI_Errhandler_set(MPI_Comm, MPI_Errhandler);
270	int MPI_Errhandler_get(MPI_Comm, MPI_Errhandler*);
271	int MPI_Errhandler_free(MPI_Errhandler*);
272	int MPI_Error_string(int, char, int);
273	int MPI_Error_class(int, int*);
274	double MPI_Wtime(void);
275	double MPI_Wtick(void);
276	int MPI_Init(int, char**);
277	int MPI_Finalize(void);
278	int MPI_Initialized(int*);
279	$system[mpi] int MPI_Abort(MPI_Comm, int);
280	int MPI_Pcontrol(const int, ...);
281	int MPI_DUP_FN(MPI_Comm, int, void, void, void, int);
282	int MPI_Close_port(char*);
283	int MPI_Comm_accept(char, MPI_Info, int, MPI_Comm, MPI_Comm);
284	int MPI_Comm_connect(char, MPI_Info, int, MPI_Comm, MPI_Comm);
285	int MPI_Comm_disconnect(MPI_Comm*);
286	int MPI_Comm_get_parent(MPI_Comm*);
287	int MPI_Comm_join(int, MPI_Comm*);
288	int MPI_Comm_spawn(char, char [], int, MPI_Info, int, MPI_Comm, MPI_Comm*, int []);
289	int MPI_Comm_spawn_multiple(int, char* [], char** [], int [], MPI_Info [], int, MPI_Comm, MPI_Comm*, int []);
290	int MPI_Lookup_name(char, MPI_Info, char);
291	int MPI_Open_port(MPI_Info, char*);
292	int MPI_Publish_name(char, MPI_Info, char);
293	int MPI_Unpublish_name(char, MPI_Info, char);
294	int MPI_Accumulate(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Op, MPI_Win);
295	int MPI_Get(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
296	int MPI_Put(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
297	int MPI_Win_complete(MPI_Win);
298	int MPI_Win_create(void, MPI_Aint, int, MPI_Info, MPI_Comm, MPI_Win);
299	int MPI_Win_fence(int, MPI_Win);
300	int MPI_Win_free(MPI_Win*);
301	int MPI_Win_get_group(MPI_Win, MPI_Group*);
302	int MPI_Win_lock(int, int, int, MPI_Win);
303	int MPI_Win_post(MPI_Group, int, MPI_Win);
304	int MPI_Win_start(MPI_Group, int, MPI_Win);
305	int MPI_Win_test(MPI_Win, int*);
306	int MPI_Win_unlock(int, MPI_Win);
307	int MPI_Win_wait(MPI_Win);
308	int MPI_Alltoallw(void, int [], int [], MPI_Datatype [], void, int [], int [], MPI_Datatype [], MPI_Comm);
309	int MPI_Exscan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
310	int MPI_Add_error_class(int*);
311	int MPI_Add_error_code(int, int*);
312	int MPI_Add_error_string(int, char*);
313	int MPI_Comm_call_errhandler(MPI_Comm, int);
314	int MPI_Comm_create_keyval(MPI_Comm_copy_attr_function, MPI_Comm_delete_attr_function, int, void);
315	int MPI_Comm_delete_attr(MPI_Comm, int);
316	int MPI_Comm_free_keyval(int*);
317	int MPI_Comm_get_attr(MPI_Comm, int, void, int);
318	int MPI_Comm_get_name(MPI_Comm, char, int);
319	int MPI_Comm_set_attr(MPI_Comm, int, void*);
320	int MPI_Comm_set_name(MPI_Comm, char*);
321	int MPI_File_call_errhandler(MPI_File, int);
322	int MPI_Grequest_complete(MPI_Request);
323	int MPI_Grequest_start(MPI_Grequest_query_function, MPI_Grequest_free_function, MPI_Grequest_cancel_function, void, MPI_Request*);
324	int MPI_Init_thread(int, char*, int, int);
325	int MPI_Is_thread_main(int*);
326	int MPI_Query_thread(int*);
327	int MPI_Status_set_cancelled(MPI_Status*, int);
328	int MPI_Status_set_elements(MPI_Status*, MPI_Datatype, int);
329	int MPI_Type_create_keyval(MPI_Type_copy_attr_function, MPI_Type_delete_attr_function, int, void);
330	int MPI_Type_delete_attr(MPI_Datatype, int);
331	int MPI_Type_dup(MPI_Datatype, MPI_Datatype*);
332	int MPI_Type_free_keyval(int*);
333	int MPI_Type_get_attr(MPI_Datatype, int, void, int);
334	int MPI_Type_get_contents(MPI_Datatype, int, int, int, int [], MPI_Aint [], MPI_Datatype []);
335	int MPI_Type_get_envelope(MPI_Datatype, int, int, int, int);
336	int MPI_Type_get_name(MPI_Datatype, char, int);
337	int MPI_Type_set_attr(MPI_Datatype, int, void*);
338	int MPI_Type_set_name(MPI_Datatype, char*);
339	int MPI_Type_match_size(int, int, MPI_Datatype*);
340	int MPI_Win_call_errhandler(MPI_Win, int);
341	int MPI_Win_create_keyval(MPI_Win_copy_attr_function, MPI_Win_delete_attr_function, int, void);
342	int MPI_Win_delete_attr(MPI_Win, int);
343	int MPI_Win_free_keyval(int*);
344	int MPI_Win_get_attr(MPI_Win, int, void, int);
345	int MPI_Win_get_name(MPI_Win, char, int);
346	int MPI_Win_set_attr(MPI_Win, int, void*);
347	int MPI_Win_set_name(MPI_Win, char*);
348	MPI_Comm MPI_Comm_f2c(MPI_Fint);
349	MPI_Datatype MPI_Type_f2c(MPI_Fint);
350	MPI_File MPI_File_f2c(MPI_Fint);
351	MPI_Fint MPI_Comm_c2f(MPI_Comm);
352	MPI_Fint MPI_File_c2f(MPI_File);
353	MPI_Fint MPI_Group_c2f(MPI_Group);
354	MPI_Fint MPI_Info_c2f(MPI_Info);
355	MPI_Fint MPI_Op_c2f(MPI_Op);
356	MPI_Fint MPI_Request_c2f(MPI_Request);
357	MPI_Fint MPI_Type_c2f(MPI_Datatype);
358	MPI_Fint MPI_Win_c2f(MPI_Win);
359	MPI_Group MPI_Group_f2c(MPI_Fint);
360	MPI_Info MPI_Info_f2c(MPI_Fint);
361	MPI_Op MPI_Op_f2c(MPI_Fint);
362	MPI_Request MPI_Request_f2c(MPI_Fint);
363	MPI_Win MPI_Win_f2c(MPI_Fint);
364	int MPI_Alloc_mem(MPI_Aint, MPI_Info info, void* baseptr);
365	int MPI_Comm_create_errhandler(MPI_Comm_errhandler_function, MPI_Errhandler);
366	int MPI_Comm_get_errhandler(MPI_Comm, MPI_Errhandler*);
367	int MPI_Comm_set_errhandler(MPI_Comm, MPI_Errhandler);
368	int MPI_File_create_errhandler(MPI_File_errhandler_function, MPI_Errhandler);
369	int MPI_File_get_errhandler(MPI_File, MPI_Errhandler*);
370	int MPI_File_set_errhandler(MPI_File, MPI_Errhandler);
371	int MPI_Finalized(int*);
372	int MPI_Free_mem(void*);
373	int MPI_Get_address(void, MPI_Aint);
374	int MPI_Info_create(MPI_Info*);
375	int MPI_Info_delete(MPI_Info, char*);
376	int MPI_Info_dup(MPI_Info, MPI_Info*);
377	int MPI_Info_free(MPI_Info* info);
378	int MPI_Info_get(MPI_Info, char, int, char, int*);
379	int MPI_Info_get_nkeys(MPI_Info, int*);
380	int MPI_Info_get_nthkey(MPI_Info, int, char*);
381	int MPI_Info_get_valuelen(MPI_Info, char, int, int*);
382	int MPI_Info_set(MPI_Info, char, char);
383	int MPI_Pack_external(char, void, int, MPI_Datatype, void, MPI_Aint, MPI_Aint);
384	int MPI_Pack_external_size(char, int, MPI_Datatype, MPI_Aint);
385	int MPI_Request_get_status(MPI_Request, int, MPI_Status);
386	int MPI_Status_c2f(MPI_Status, MPI_Fint);
387	int MPI_Status_f2c(MPI_Fint, MPI_Status);
388	int MPI_Type_create_darray(int, int, int, int [], int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
389	int MPI_Type_create_hindexed(int, int [], MPI_Aint [], MPI_Datatype, MPI_Datatype*);
390	int MPI_Type_create_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
391	int MPI_Type_create_indexed_block(int, int, int [], MPI_Datatype, MPI_Datatype*);
392	int MPIX_Type_create_hindexed_block(int, int, MPI_Aint [], MPI_Datatype, MPI_Datatype*);
393	int MPI_Type_create_resized(MPI_Datatype, MPI_Aint, MPI_Aint, MPI_Datatype*);
394	int MPI_Type_create_struct(int, int [], MPI_Aint [], MPI_Datatype [], MPI_Datatype*);
395	int MPI_Type_create_subarray(int, int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
396	int MPI_Type_get_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
397	int MPI_Type_get_true_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
398	int MPI_Unpack_external(char, void, MPI_Aint, MPI_Aint, void, int, MPI_Datatype);
399	int MPI_Win_create_errhandler(MPI_Win_errhandler_function, MPI_Errhandler);
400	int MPI_Win_get_errhandler(MPI_Win, MPI_Errhandler*);
401	int MPI_Win_set_errhandler(MPI_Win, MPI_Errhandler);
402	int MPI_Type_create_f90_integer(int, MPI_Datatype*);
403	int MPI_Type_create_f90_real(int, int, MPI_Datatype*);
404	int MPI_Type_create_f90_complex(int, int, MPI_Datatype*);
405	int MPI_Reduce_local(void* inbuf, void* inoutbuf, int count, MPI_Datatype datatype, MPI_Op op);
406	int MPI_Op_commutative(MPI_Op op, int* commute);
407	int MPI_Reduce_scatter_block(void* sendbuf, void* recvbuf, int recvcount, MPI_Datatype datatype, MPI_Op op, MPI_Comm comm);
408	int MPI_Dist_graph_create_adjacent(MPI_Comm comm_old, int indegree, int [], int [], int outdegree, int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
409	int MPI_Dist_graph_create(MPI_Comm comm_old, int n, int [], int [], int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
410	int MPI_Dist_graph_neighbors_count(MPI_Comm comm, int* indegree, int* outdegree, int* weighted);
411	int MPI_Dist_graph_neighbors(MPI_Comm comm, int maxindegree, int [], int [], int maxoutdegree, int [], int []);
412	const extern int* MPI_UNWEIGHTED;
413	extern MPI_Fint* MPI_F_STATUS_IGNORE;
414	extern MPI_Fint* MPI_F_STATUSES_IGNORE;
415	const extern struct MPIR_T_pvar_handle* MPI_T_PVAR_ALL_HANDLES;
416	typedef enum MPIR_T_verbosity_t{
417	MPI_T_VERBOSITY_INVALID=0,
418	MPI_T_VERBOSITY_USER_BASIC=221,
419	MPI_T_VERBOSITY_USER_DETAIL,
420	MPI_T_VERBOSITY_USER_ALL,
421	MPI_T_VERBOSITY_TUNER_BASIC,
422	MPI_T_VERBOSITY_TUNER_DETAIL,
423	MPI_T_VERBOSITY_TUNER_ALL,
424	MPI_T_VERBOSITY_MPIDEV_BASIC,
425	MPI_T_VERBOSITY_MPIDEV_DETAIL,
426	MPI_T_VERBOSITY_MPIDEV_ALL
427	} MPIR_T_verbosity_t;
428	typedef enum MPIR_T_bind_t{
429	MPI_T_BIND_INVALID=0,
430	MPI_T_BIND_NO_OBJECT=9700,
431	MPI_T_BIND_MPI_COMM,
432	MPI_T_BIND_MPI_DATATYPE,
433	MPI_T_BIND_MPI_ERRHANDLER,
434	MPI_T_BIND_MPI_FILE,
435	MPI_T_BIND_MPI_GROUP,
436	MPI_T_BIND_MPI_OP,
437	MPI_T_BIND_MPI_REQUEST,
438	MPI_T_BIND_MPI_WIN,
439	MPI_T_BIND_MPI_MESSAGE,
440	MPI_T_BIND_MPI_INFO
441	} MPIR_T_bind_t;
442	typedef enum MPIR_T_scope_t{
443	MPI_T_SCOPE_INVALID=0,
444	MPI_T_SCOPE_READONLY=60439,
445	MPI_T_SCOPE_LOCAL,
446	MPI_T_SCOPE_GROUP,
447	MPI_T_SCOPE_GROUP_EQ,
448	MPI_T_SCOPE_ALL,
449	MPI_T_SCOPE_ALL_EQ
450	} MPIR_T_scope_t;
451	typedef enum MPIR_T_pvar_class_t{
452	MPI_T_PVAR_CLASS_INVALID=0,
453	MPI_T_PVAR_CLASS_STATE=240,
454	MPI_T_PVAR_CLASS_LEVEL,
455	MPI_T_PVAR_CLASS_SIZE,
456	MPI_T_PVAR_CLASS_PERCENTAGE,
457	MPI_T_PVAR_CLASS_HIGHWATERMARK,
458	MPI_T_PVAR_CLASS_LOWWATERMARK,
459	MPI_T_PVAR_CLASS_COUNTER,
460	MPI_T_PVAR_CLASS_AGGREGATE,
461	MPI_T_PVAR_CLASS_TIMER,
462	MPI_T_PVAR_CLASS_GENERIC
463	} MPIR_T_pvar_class_t;
464	//======================== civlc.cvh =======================
465	typedef unsigned long size_t;
466	typedef struct $proc $proc;
467	typedef struct $scope $scope;
468	typedef struct $dynamic $dynamic;
469	typedef enum Operation $operation;
470	$system[civlc] void $wait($proc p);
471	$system[civlc] void $waitall($proc* procs, int numProcs);
472	/*@ depends_on \nothing;
473	@ executes_when $true;
474	@*/
475	$system[civlc] void $exit(void);
476	/*@ depends_on \nothing;
477	@ executes_when $true;
478	@*/
479	$system[civlc] int $choose_int(int n);
480	/*@ depends_on \nothing;
481	@ executes_when $true;
482	@*/
483	$system[civlc] void $assert(_Bool expr, ...);
484	/*@ depends_on \nothing;
485	@ executes_when $true;
486	@*/
487	$system[civlc] void $assume(_Bool expr);
488	/*@ pure;
489	@ depends_on \nothing;
490	@ executes_when $true;
491	@*/
492	$system[civlc] void $elaborate(int x);
493	/*@ depends_on \nothing;
494	@ executes_when $true;
495	@*/
496	$system[civlc] int $next_time_count(void);
497	/*@ pure;
498	@ depends_on \nothing;
499	@ executes_when $true;
500	@*/
501	$system[civlc] void $pathCondition(void);
502	/*@ pure;
503	@ depends_on \nothing;
504	@ executes_when $true;
505	@*/
506	$system[civlc] _Bool $is_concrete_int(int value);
507	/*@ depends_on \nothing;
508	@ executes_when $true;
509	@*/
510	$system[civlc] void* $malloc($scope s, int size);
511	/*@ depends_on \write(p);
512	@ executes_when $true;
513	@*/
514	$system[civlc] void $free(void* p);
515	/*@ depends_on \write(ptr);
516	@ executes_when $true;
517	@*/
518	$system[civlc] void $havoc(void* ptr);
519	/*@ pure;
520	@ depends_on \nothing;
521	@ executes_when $true;
522	@*/
523	$system[civlc] double $pow(double base, double exp);
524	//======================= bundle.cvh =======================
525	typedef struct _bundle $bundle;
526	/*@ depends_on \nothing;
527	@ executes_when $true;
528	@*/
529	$system[bundle] int $bundle_size($bundle b);
530	/*@ depends_on \write(ptr);
531	@ executes_when $true;
532	@*/
533	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
534	/*@ depends_on \write(ptr);
535	@ executes_when $true;
536	@*/
537	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
538	/*@ depends_on \write(buf);
539	@ executes_when $true;
540	@*/
541	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
542	//======================== comm.cvh ========================
543	typedef struct _message{
544	int source;
545	int dest;
546	int tag;
547	$bundle data;
548	int size;
549	} $message;
550	typedef struct _queue $queue;
551	typedef struct _gcomm* $gcomm;
552	typedef struct _comm* $comm;
553	/*@ pure;
554	@ depends_on \nothing;
555	@ executes_when $true;
556	@*/
557	$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
558	/*@ pure;
559	@ depends_on \nothing;
560	@ executes_when $true;
561	@*/
562	$atomic_f int $message_source($message message);
563	/*@ pure;
564	@ depends_on \nothing;
565	@ executes_when $true;
566	@*/
567	$atomic_f int $message_tag($message message);
568	/*@ pure;
569	@ depends_on \nothing;
570	@ executes_when $true;
571	@*/
572	$atomic_f int $message_dest($message message);
573	/*@ pure;
574	@ depends_on \nothing;
575	@ executes_when $true;
576	@*/
577	$atomic_f int $message_size($message message);
578	/*@ depends_on \write(buf);
579	@ executes_when $true;
580	@*/
581	$atomic_f void $message_unpack($message message, void* buf, int size);
582	/*@ depends_on \nothing;
583	@ assigns \nothing;
584	@ reads \nothing;
585	@*/
586	$atomic_f $gcomm $gcomm_create($scope scope, int size);
587	/*@ depends_on \write(junkMsgs), \write(gcomm);
588	@ assigns junkMsgs, gcomm;
589	@*/
590	$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
591	/*@ depends_on \nothing;
592	@ executes_when $true;
593	@*/
594	$system[comm] void $gcomm_dup($comm comm, $comm newcomm);
595	$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
596	/*@ depends_on \write(comm);
597	@ assigns comm;
598	@ reads \nothing;
599	@*/
600	$atomic_f void $comm_destroy($comm comm);
601	/*@ pure;
602	@ depends_on \nothing;
603	@*/
604	$atomic_f int $comm_size($comm comm);
605	/*@ pure;
606	@ depends_on \nothing;
607	@ executes_when $true;
608	@*/
609	$atomic_f int $comm_place($comm comm);
610	/*@ depends_on \write(comm);
611	@ executes_when $true;
612	@*/
613	$system[comm] void $comm_enqueue($comm comm, $message message);
614	/*@ pure;
615	@ depends_on \write(comm);
616	@ executes_when $true;
617	@*/
618	$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
619	/*@ pure;
620	@ depends_on \write(comm);
621	@ executes_when $true;
622	@*/
623	$system[comm] $message $comm_seek($comm comm, int source, int tag);
624	/*@ depends_on \write(comm);
625	@ executes_when $comm_probe(comm, source, tag);
626	@*/
627	$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
628	//===================== concurrency.cvh ====================
629	typedef struct _gbarrier* $gbarrier;
630	typedef struct _barrier* $barrier;
631	/*@ depends_on \nothing;
632	@ assigns \nothing;
633	@ reads \nothing;
634	@*/
635	$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
636	/*@ depends_on \write(gbarrier);
637	@ reads \nothing;
638	@ assigns gbarrier;
639	@*/
640	$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
641	/*@ depends_on \nothing;
642	@ assigns gbarrier;
643	@ reads gbarrier;
644	@*/
645	$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
646	/*@ depends_on \write(barrier);
647	@ assigns barrier;
648	@ reads \nothing;
649	@*/
650	$atomic_f void $barrier_destroy($barrier barrier);
651	void $barrier_call($barrier barrier);
652	typedef struct _collator_entry $collator_entry;
653	typedef struct _gcollator* $gcollator;
654	typedef struct _collator* $collator;
655	/*@ depends_on \nothing;
656	@ reads \nothing;
657	@ assigns \nothing;
658	@*/
659	$atomic_f $gcollator $gcollator_create($scope scope);
660	/*@ depends_on \write(gcollator);
661	@ assigns gcollator;
662	@ reads \nothing;
663	@*/
664	$atomic_f int $gcollator_destroy($gcollator gcollator);
665	/*@ depends_on \nothing;
666	@ executes_when $true;
667	@*/
668	$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
669	/*@ depends_on \write(collator);
670	@ executes_when $true;
671	@*/
672	$atomic_f void $collator_destroy($collator collator);
673	/*@ depends_on \write(collator);
674	@ executes_when $true;
675	@*/
676	$system[concurrency] $bundle $collator_check($collator collator, int place, int nprocs, $bundle entries);
677	//======================= collate.cvh ======================
678	typedef struct _gcollator* $gcollator;
679	typedef struct _collator* $collator;
680	typedef struct _gcollate_state* $gcollate_state;
681	typedef struct _collate_state* $collate_state;
682	$gcollator gcollator_create($scope scope, int nprocs);
683	$collator collator_create($gcollator gcollator, int place);
684	$collate_state $collate_snapshot($collator c);
685	$collate_state $collate_unsnapshot($collator c);
686	/*@ pure;
687	@*/
688	$system[collate] _Bool $collate_arrived($collate_state cp, $range r);
689	/*@ pure;
690	@*/
691	$system[collate] _Bool $collate_complete($collate_state cp);
692	//====================== civl-mpi.cvh ======================
693	typedef enum _mpi_state{
694	_MPI_UNINIT,
695	_MPI_INIT,
696	_MPI_FINALIZED
697	} $mpi_state;
698	typedef struct MPI_Comm MPI_Comm;
699	typedef struct MPI_Status MPI_Status;
700	typedef struct $mpi_gcomm $mpi_gcomm;
701	int sizeofDatatype(MPI_Datatype);
702	$abstract double $mpi_time(int i);
703	$mpi_gcomm $mpi_gcomm_create($scope, int);
704	void $mpi_gcomm_destroy($mpi_gcomm);
705	MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
706	void $mpi_comm_destroy(MPI_Comm, $mpi_state);
707	int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
708	int $mpi_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
709	int $mpi_sendrecv(void* sendbuf, int sendcount, MPI_Datatype sendtype, int dest, int sendtag, void* recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status* status);
710	int $mpi_collective_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
711	int $mpi_collective_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status, char*);
712	int $mpi_bcast(void, int, MPI_Datatype, int, int, MPI_Comm, char);
713	int $mpi_reduce(void, void, int, MPI_Datatype, MPI_Op, int, int, MPI_Comm, char*);
714	int $mpi_gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
715	int $mpi_gatherv(void, int, MPI_Datatype, void, int [], int [], MPI_Datatype, int, int, MPI_Comm, char*);
716	int $mpi_scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
717	int $mpi_scatterv(void, int [], int [], MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
718	void* $mpi_pointer_add(void*, int, MPI_Datatype);
719	$system[mpi] int $mpi_new_gcomm($scope, $mpi_gcomm);
720	$system[mpi] $mpi_gcomm $mpi_get_gcomm($scope, int);
721	int $mpi_comm_dup($scope, MPI_Comm, MPI_Comm, char);
722	int $mpi_comm_free(MPI_Comm*, $mpi_state);
723	$system[mpi] $scope $mpi_root_scope($comm);
724	$system[mpi] $scope $mpi_proc_scope($comm);
725	$system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
726	$bundle $mpi_create_coroutine_entry(int routineTag, int root, int op, int numDatatypes, int* datatypes);
727	void $mpi_diff_coroutine_entries($bundle specEntry, $bundle mineEntry, int rank);
728	void $mpi_coassert(MPI_Comm, _Bool);
729	_Bool $mpi_isRecvBufEmpty(int x);
730	/*@ depends_on \nothing;
731	@*/
732	$system[mpi] void $mpi_p2pSendShot(int commID, $message msg, int place);
733	/*@ depends_on \nothing;
734	@*/
735	$system[mpi] void $mpi_colSendShot(int commID, $message msg, int place);
736	/*@ depends_on \nothing;
737	@*/
738	$system[mpi] void $mpi_p2pRecvShot(int commID, int source, int dest, int tag);
739	/*@ depends_on \nothing;
740	@*/
741	$system[mpi] void $mpi_colRecvShot(int commID, int source, int dest, int tag);
742	//======================== stddef.h ========================
743	typedef long ptrdiff_t;
744	typedef unsigned long size_t;
745	typedef struct max_align_t max_align_t;
746	typedef long wchar_t;
747	//======================== string.h ========================
748	void* memcpy(void* p, void* q, size_t size);
749	void* memmove(void* dest, void* src, size_t n);
750	$system[string] void* memset(void* s, int c, size_t n);
751	int memcmp(void* s1, void* s2, size_t n);
752	void* memchr(void* s, int c, size_t n);
753	$system[string] char* strcpy(char* restrict s1, char* restrict s2);
754	char* strncpy(char* dest, char* src, size_t n);
755	char* strcat(char* dest, char* src);
756	char* strncat(char* dest, char* src, size_t n);
757	$system[string] int strcmp(char* s1, char* s2);
758	int strncmp(char* s1, char* s2, size_t n);
759	int strcoll(char* s1, char* s2);
760	size_t strxfrm(char* dest, char* src, size_t n);
761	char* strchr(char* s, int c);
762	char* strrchr(char* s, int c);
763	size_t strcspn(char* s, char* reject);
764	size_t strspn(char* s, char* accept);
765	char* strpbrk(char* s, char* accept);
766	char* strstr(char* s1, char* s2);
767	char* strtok(char* s, char* delim);
768	$system[string] size_t strlen(char* s);
769	char* strerror(int errnum);
770	//======================== civlc.cvh =======================
771	$system[civlc] void $wait($proc p);
772	$system[civlc] void $waitall($proc* procs, int numProcs);
773	/*@ depends_on \nothing;
774	@ executes_when $true;
775	@*/
776	$system[civlc] void $exit(void);
777	/*@ depends_on \nothing;
778	@ executes_when $true;
779	@*/
780	$system[civlc] int $choose_int(int n);
781	/*@ depends_on \nothing;
782	@ executes_when $true;
783	@*/
784	$system[civlc] void $assert(_Bool expr, ...);
785	/*@ depends_on \nothing;
786	@ executes_when $true;
787	@*/
788	$system[civlc] void $assume(_Bool expr);
789	/*@ pure;
790	@ depends_on \nothing;
791	@ executes_when $true;
792	@*/
793	$system[civlc] void $elaborate(int x);
794	/*@ depends_on \nothing;
795	@ executes_when $true;
796	@*/
797	$system[civlc] int $next_time_count(void);
798	/*@ pure;
799	@ depends_on \nothing;
800	@ executes_when $true;
801	@*/
802	$system[civlc] void $pathCondition(void);
803	/*@ pure;
804	@ depends_on \nothing;
805	@ executes_when $true;
806	@*/
807	$system[civlc] _Bool $is_concrete_int(int value);
808	/*@ depends_on \nothing;
809	@ executes_when $true;
810	@*/
811	$system[civlc] void* $malloc($scope s, int size);
812	/*@ depends_on \write(p);
813	@ executes_when $true;
814	@*/
815	$system[civlc] void $free(void* p);
816	/*@ depends_on \write(ptr);
817	@ executes_when $true;
818	@*/
819	$system[civlc] void $havoc(void* ptr);
820	/*@ pure;
821	@ depends_on \nothing;
822	@ executes_when $true;
823	@*/
824	$system[civlc] double $pow(double base, double exp);
825	//======================= bundle.cvh =======================
826	/*@ depends_on \nothing;
827	@ executes_when $true;
828	@*/
829	$system[bundle] int $bundle_size($bundle b);
830	/*@ depends_on \write(ptr);
831	@ executes_when $true;
832	@*/
833	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
834	/*@ depends_on \write(ptr);
835	@ executes_when $true;
836	@*/
837	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
838	/*@ depends_on \write(buf);
839	@ executes_when $true;
840	@*/
841	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
842	//===================== concurrency.cvh ====================
843	/*@ depends_on \nothing;
844	@ assigns \nothing;
845	@ reads \nothing;
846	@*/
847	$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
848	/*@ depends_on \write(gbarrier);
849	@ reads \nothing;
850	@ assigns gbarrier;
851	@*/
852	$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
853	/*@ depends_on \nothing;
854	@ assigns gbarrier;
855	@ reads gbarrier;
856	@*/
857	$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
858	/*@ depends_on \write(barrier);
859	@ assigns barrier;
860	@ reads \nothing;
861	@*/
862	$atomic_f void $barrier_destroy($barrier barrier);
863	void $barrier_call($barrier barrier);
864	/*@ depends_on \nothing;
865	@ reads \nothing;
866	@ assigns \nothing;
867	@*/
868	$atomic_f $gcollator $gcollator_create($scope scope);
869	/*@ depends_on \write(gcollator);
870	@ assigns gcollator;
871	@ reads \nothing;
872	@*/
873	$atomic_f int $gcollator_destroy($gcollator gcollator);
874	/*@ depends_on \nothing;
875	@ executes_when $true;
876	@*/
877	$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
878	/*@ depends_on \write(collator);
879	@ executes_when $true;
880	@*/
881	$atomic_f void $collator_destroy($collator collator);
882	/*@ depends_on \write(collator);
883	@ executes_when $true;
884	@*/
885	$system[concurrency] $bundle $collator_check($collator collator, int place, int nprocs, $bundle entries);
886	//========================== mpi.h =========================
887	MPI_Comm MPI_COMM_WORLD;
888	MPI_Comm MPI_COMM_SELF;
889	MPI_Comm MPI_COMM_PARENT;
890	MPI_Comm MPI_COMM_TYPE_SHARED;
891	int MPI_Send(void*, int, MPI_Datatype, int, int, MPI_Comm);
892	int MPI_Recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
893	int MPI_Get_count(MPI_Status, MPI_Datatype, int);
894	int MPI_Bsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
895	int MPI_Ssend(void*, int, MPI_Datatype, int, int, MPI_Comm);
896	int MPI_Rsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
897	int MPI_Buffer_attach(void*, int);
898	int MPI_Buffer_detach(void, int);
899	int MPI_Isend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
900	int MPI_Ibsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
901	int MPI_Issend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
902	int MPI_Irsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
903	int MPI_Irecv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
904	int MPI_Wait(MPI_Request, MPI_Status);
905	int MPI_Test(MPI_Request, int, MPI_Status*);
906	int MPI_Request_free(MPI_Request*);
907	int MPI_Waitany(int, MPI_Request, int, MPI_Status*);
908	int MPI_Testany(int, MPI_Request, int, int, MPI_Status);
909	int MPI_Waitall(int, MPI_Request, MPI_Status);
910	int MPI_Testall(int, MPI_Request, int, MPI_Status*);
911	int MPI_Waitsome(int, MPI_Request, int, int, MPI_Status);
912	int MPI_Testsome(int, MPI_Request, int, int, MPI_Status);
913	int MPI_Iprobe(int, int, MPI_Comm, int, MPI_Status);
914	int MPI_Probe(int, int, MPI_Comm, MPI_Status*);
915	int MPI_Cancel(MPI_Request*);
916	int MPI_Test_cancelled(MPI_Status, int);
917	int MPI_Send_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
918	int MPI_Bsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
919	int MPI_Ssend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
920	int MPI_Rsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
921	int MPI_Recv_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
922	int MPI_Start(MPI_Request*);
923	int MPI_Startall(int, MPI_Request*);
924	int MPI_Sendrecv(void, int, MPI_Datatype, int, int, void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
925	int MPI_Sendrecv_replace(void, int, MPI_Datatype, int, int, int, int, MPI_Comm, MPI_Status);
926	int MPI_Type_contiguous(int, MPI_Datatype, MPI_Datatype*);
927	int MPI_Type_vector(int, int, int, MPI_Datatype, MPI_Datatype*);
928	int MPI_Type_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
929	int MPI_Type_indexed(int, int, int, MPI_Datatype, MPI_Datatype*);
930	int MPI_Type_hindexed(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
931	int MPI_Type_struct(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype);
932	int MPI_Address(void, MPI_Aint);
933	int MPI_Type_extent(MPI_Datatype, MPI_Aint*);
934	int MPI_Type_size(MPI_Datatype, int*);
935	int MPI_Type_lb(MPI_Datatype, MPI_Aint*);
936	int MPI_Type_ub(MPI_Datatype, MPI_Aint*);
937	int MPI_Type_commit(MPI_Datatype*);
938	int MPI_Type_free(MPI_Datatype*);
939	int MPI_Get_elements(MPI_Status, MPI_Datatype, int);
940	int MPI_Pack(void, int, MPI_Datatype, void, int, int*, MPI_Comm);
941	int MPI_Unpack(void, int, int, void*, int, MPI_Datatype, MPI_Comm);
942	int MPI_Pack_size(int, MPI_Datatype, MPI_Comm, int*);
943	int MPI_Barrier(MPI_Comm);
944	int MPI_Bcast(void*, int, MPI_Datatype, int, MPI_Comm);
945	int MPI_Gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
946	int MPI_Gatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, int, MPI_Comm);
947	int MPI_Scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
948	int MPI_Scatterv(void, int, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
949	int MPI_Allgather(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
950	int MPI_Allgatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
951	int MPI_Alltoall(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
952	int MPI_Alltoallv(void, int, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
953	int MPI_Reduce(void, void, int, MPI_Datatype, MPI_Op, int, MPI_Comm);
954	int MPI_Op_create(MPI_User_function, int, MPI_Op);
955	int MPI_Op_free(MPI_Op*);
956	int MPI_Allreduce(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
957	int MPI_Reduce_scatter(void, void, int*, MPI_Datatype, MPI_Op, MPI_Comm);
958	int MPI_Scan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
959	int MPI_Group_size(MPI_Group, int*);
960	int MPI_Group_rank(MPI_Group, int*);
961	int MPI_Group_translate_ranks(MPI_Group, int, int, MPI_Group, int);
962	int MPI_Group_compare(MPI_Group, MPI_Group, int*);
963	int MPI_Comm_group(MPI_Comm, MPI_Group*);
964	int MPI_Group_union(MPI_Group, MPI_Group, MPI_Group*);
965	int MPI_Group_intersection(MPI_Group, MPI_Group, MPI_Group*);
966	int MPI_Group_difference(MPI_Group, MPI_Group, MPI_Group*);
967	int MPI_Group_incl(MPI_Group, int, int, MPI_Group);
968	int MPI_Group_excl(MPI_Group, int, int, MPI_Group);
969	int MPI_Group_range_incl(MPI_Group, int, int [][3], MPI_Group*);
970	int MPI_Group_range_excl(MPI_Group, int, int [][3], MPI_Group*);
971	int MPI_Group_free(MPI_Group*);
972	int MPI_Comm_size(MPI_Comm, int*);
973	int MPI_Comm_rank(MPI_Comm, int*);
974	int MPI_Comm_compare(MPI_Comm, MPI_Comm, int*);
975	int MPI_Comm_dup(MPI_Comm, MPI_Comm*);
976	int MPI_Comm_create(MPI_Comm, MPI_Group, MPI_Comm*);
977	int MPI_Comm_split(MPI_Comm, int, int, MPI_Comm*);
978	int MPI_Comm_free(MPI_Comm*);
979	int MPI_Comm_test_inter(MPI_Comm, int*);
980	int MPI_Comm_remote_size(MPI_Comm, int*);
981	int MPI_Comm_remote_group(MPI_Comm, MPI_Group*);
982	int MPI_Intercomm_create(MPI_Comm, int, MPI_Comm, int, int, MPI_Comm*);
983	int MPI_Intercomm_merge(MPI_Comm, int, MPI_Comm*);
984	int MPI_Keyval_create(MPI_Copy_function, MPI_Delete_function, int, void);
985	int MPI_Keyval_free(int*);
986	int MPI_Attr_put(MPI_Comm, int, void*);
987	int MPI_Attr_get(MPI_Comm, int, void, int);
988	int MPI_Attr_delete(MPI_Comm, int);
989	int MPI_Topo_test(MPI_Comm, int*);
990	int MPI_Cart_create(MPI_Comm, int, int, int, int, MPI_Comm*);
991	int MPI_Dims_create(int, int, int*);
992	int MPI_Graph_create(MPI_Comm, int, int, int, int, MPI_Comm*);
993	int MPI_Graphdims_get(MPI_Comm, int, int);
994	int MPI_Graph_get(MPI_Comm, int, int, int, int);
995	int MPI_Cartdim_get(MPI_Comm, int*);
996	int MPI_Cart_get(MPI_Comm, int, int, int, int*);
997	int MPI_Cart_rank(MPI_Comm, int, int);
998	int MPI_Cart_coords(MPI_Comm, int, int, int*);
999	int MPI_Graph_neighbors_count(MPI_Comm, int, int*);
1000	int MPI_Graph_neighbors(MPI_Comm, int, int, int*);
1001	int MPI_Cart_shift(MPI_Comm, int, int, int, int);
1002	int MPI_Cart_sub(MPI_Comm, int, MPI_Comm);
1003	int MPI_Cart_map(MPI_Comm, int, int, int, int*);
1004	int MPI_Graph_map(MPI_Comm, int, int, int, int*);
1005	int MPI_Get_processor_name(char, int);
1006	int MPI_Get_version(int, int);
1007	int MPI_Errhandler_create(MPI_Handler_function, MPI_Errhandler);
1008	int MPI_Errhandler_set(MPI_Comm, MPI_Errhandler);
1009	int MPI_Errhandler_get(MPI_Comm, MPI_Errhandler*);
1010	int MPI_Errhandler_free(MPI_Errhandler*);
1011	int MPI_Error_string(int, char, int);
1012	int MPI_Error_class(int, int*);
1013	double MPI_Wtime(void);
1014	double MPI_Wtick(void);
1015	int MPI_Init(int, char**);
1016	int MPI_Finalize(void);
1017	int MPI_Initialized(int*);
1018	$system[mpi] int MPI_Abort(MPI_Comm, int);
1019	int MPI_Pcontrol(const int, ...);
1020	int MPI_DUP_FN(MPI_Comm, int, void, void, void, int);
1021	int MPI_Close_port(char*);
1022	int MPI_Comm_accept(char, MPI_Info, int, MPI_Comm, MPI_Comm);
1023	int MPI_Comm_connect(char, MPI_Info, int, MPI_Comm, MPI_Comm);
1024	int MPI_Comm_disconnect(MPI_Comm*);
1025	int MPI_Comm_get_parent(MPI_Comm*);
1026	int MPI_Comm_join(int, MPI_Comm*);
1027	int MPI_Comm_spawn(char, char [], int, MPI_Info, int, MPI_Comm, MPI_Comm*, int []);
1028	int MPI_Comm_spawn_multiple(int, char* [], char** [], int [], MPI_Info [], int, MPI_Comm, MPI_Comm*, int []);
1029	int MPI_Lookup_name(char, MPI_Info, char);
1030	int MPI_Open_port(MPI_Info, char*);
1031	int MPI_Publish_name(char, MPI_Info, char);
1032	int MPI_Unpublish_name(char, MPI_Info, char);
1033	int MPI_Accumulate(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Op, MPI_Win);
1034	int MPI_Get(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
1035	int MPI_Put(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
1036	int MPI_Win_complete(MPI_Win);
1037	int MPI_Win_create(void, MPI_Aint, int, MPI_Info, MPI_Comm, MPI_Win);
1038	int MPI_Win_fence(int, MPI_Win);
1039	int MPI_Win_free(MPI_Win*);
1040	int MPI_Win_get_group(MPI_Win, MPI_Group*);
1041	int MPI_Win_lock(int, int, int, MPI_Win);
1042	int MPI_Win_post(MPI_Group, int, MPI_Win);
1043	int MPI_Win_start(MPI_Group, int, MPI_Win);
1044	int MPI_Win_test(MPI_Win, int*);
1045	int MPI_Win_unlock(int, MPI_Win);
1046	int MPI_Win_wait(MPI_Win);
1047	int MPI_Alltoallw(void, int [], int [], MPI_Datatype [], void, int [], int [], MPI_Datatype [], MPI_Comm);
1048	int MPI_Exscan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
1049	int MPI_Add_error_class(int*);
1050	int MPI_Add_error_code(int, int*);
1051	int MPI_Add_error_string(int, char*);
1052	int MPI_Comm_call_errhandler(MPI_Comm, int);
1053	int MPI_Comm_create_keyval(MPI_Comm_copy_attr_function, MPI_Comm_delete_attr_function, int, void);
1054	int MPI_Comm_delete_attr(MPI_Comm, int);
1055	int MPI_Comm_free_keyval(int*);
1056	int MPI_Comm_get_attr(MPI_Comm, int, void, int);
1057	int MPI_Comm_get_name(MPI_Comm, char, int);
1058	int MPI_Comm_set_attr(MPI_Comm, int, void*);
1059	int MPI_Comm_set_name(MPI_Comm, char*);
1060	int MPI_File_call_errhandler(MPI_File, int);
1061	int MPI_Grequest_complete(MPI_Request);
1062	int MPI_Grequest_start(MPI_Grequest_query_function, MPI_Grequest_free_function, MPI_Grequest_cancel_function, void, MPI_Request*);
1063	int MPI_Init_thread(int, char*, int, int);
1064	int MPI_Is_thread_main(int*);
1065	int MPI_Query_thread(int*);
1066	int MPI_Status_set_cancelled(MPI_Status*, int);
1067	int MPI_Status_set_elements(MPI_Status*, MPI_Datatype, int);
1068	int MPI_Type_create_keyval(MPI_Type_copy_attr_function, MPI_Type_delete_attr_function, int, void);
1069	int MPI_Type_delete_attr(MPI_Datatype, int);
1070	int MPI_Type_dup(MPI_Datatype, MPI_Datatype*);
1071	int MPI_Type_free_keyval(int*);
1072	int MPI_Type_get_attr(MPI_Datatype, int, void, int);
1073	int MPI_Type_get_contents(MPI_Datatype, int, int, int, int [], MPI_Aint [], MPI_Datatype []);
1074	int MPI_Type_get_envelope(MPI_Datatype, int, int, int, int);
1075	int MPI_Type_get_name(MPI_Datatype, char, int);
1076	int MPI_Type_set_attr(MPI_Datatype, int, void*);
1077	int MPI_Type_set_name(MPI_Datatype, char*);
1078	int MPI_Type_match_size(int, int, MPI_Datatype*);
1079	int MPI_Win_call_errhandler(MPI_Win, int);
1080	int MPI_Win_create_keyval(MPI_Win_copy_attr_function, MPI_Win_delete_attr_function, int, void);
1081	int MPI_Win_delete_attr(MPI_Win, int);
1082	int MPI_Win_free_keyval(int*);
1083	int MPI_Win_get_attr(MPI_Win, int, void, int);
1084	int MPI_Win_get_name(MPI_Win, char, int);
1085	int MPI_Win_set_attr(MPI_Win, int, void*);
1086	int MPI_Win_set_name(MPI_Win, char*);
1087	MPI_Comm MPI_Comm_f2c(MPI_Fint);
1088	MPI_Datatype MPI_Type_f2c(MPI_Fint);
1089	MPI_File MPI_File_f2c(MPI_Fint);
1090	MPI_Fint MPI_Comm_c2f(MPI_Comm);
1091	MPI_Fint MPI_File_c2f(MPI_File);
1092	MPI_Fint MPI_Group_c2f(MPI_Group);
1093	MPI_Fint MPI_Info_c2f(MPI_Info);
1094	MPI_Fint MPI_Op_c2f(MPI_Op);
1095	MPI_Fint MPI_Request_c2f(MPI_Request);
1096	MPI_Fint MPI_Type_c2f(MPI_Datatype);
1097	MPI_Fint MPI_Win_c2f(MPI_Win);
1098	MPI_Group MPI_Group_f2c(MPI_Fint);
1099	MPI_Info MPI_Info_f2c(MPI_Fint);
1100	MPI_Op MPI_Op_f2c(MPI_Fint);
1101	MPI_Request MPI_Request_f2c(MPI_Fint);
1102	MPI_Win MPI_Win_f2c(MPI_Fint);
1103	int MPI_Alloc_mem(MPI_Aint, MPI_Info info, void* baseptr);
1104	int MPI_Comm_create_errhandler(MPI_Comm_errhandler_function, MPI_Errhandler);
1105	int MPI_Comm_get_errhandler(MPI_Comm, MPI_Errhandler*);
1106	int MPI_Comm_set_errhandler(MPI_Comm, MPI_Errhandler);
1107	int MPI_File_create_errhandler(MPI_File_errhandler_function, MPI_Errhandler);
1108	int MPI_File_get_errhandler(MPI_File, MPI_Errhandler*);
1109	int MPI_File_set_errhandler(MPI_File, MPI_Errhandler);
1110	int MPI_Finalized(int*);
1111	int MPI_Free_mem(void*);
1112	int MPI_Get_address(void, MPI_Aint);
1113	int MPI_Info_create(MPI_Info*);
1114	int MPI_Info_delete(MPI_Info, char*);
1115	int MPI_Info_dup(MPI_Info, MPI_Info*);
1116	int MPI_Info_free(MPI_Info* info);
1117	int MPI_Info_get(MPI_Info, char, int, char, int*);
1118	int MPI_Info_get_nkeys(MPI_Info, int*);
1119	int MPI_Info_get_nthkey(MPI_Info, int, char*);
1120	int MPI_Info_get_valuelen(MPI_Info, char, int, int*);
1121	int MPI_Info_set(MPI_Info, char, char);
1122	int MPI_Pack_external(char, void, int, MPI_Datatype, void, MPI_Aint, MPI_Aint);
1123	int MPI_Pack_external_size(char, int, MPI_Datatype, MPI_Aint);
1124	int MPI_Request_get_status(MPI_Request, int, MPI_Status);
1125	int MPI_Status_c2f(MPI_Status, MPI_Fint);
1126	int MPI_Status_f2c(MPI_Fint, MPI_Status);
1127	int MPI_Type_create_darray(int, int, int, int [], int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
1128	int MPI_Type_create_hindexed(int, int [], MPI_Aint [], MPI_Datatype, MPI_Datatype*);
1129	int MPI_Type_create_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
1130	int MPI_Type_create_indexed_block(int, int, int [], MPI_Datatype, MPI_Datatype*);
1131	int MPIX_Type_create_hindexed_block(int, int, MPI_Aint [], MPI_Datatype, MPI_Datatype*);
1132	int MPI_Type_create_resized(MPI_Datatype, MPI_Aint, MPI_Aint, MPI_Datatype*);
1133	int MPI_Type_create_struct(int, int [], MPI_Aint [], MPI_Datatype [], MPI_Datatype*);
1134	int MPI_Type_create_subarray(int, int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
1135	int MPI_Type_get_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
1136	int MPI_Type_get_true_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
1137	int MPI_Unpack_external(char, void, MPI_Aint, MPI_Aint, void, int, MPI_Datatype);
1138	int MPI_Win_create_errhandler(MPI_Win_errhandler_function, MPI_Errhandler);
1139	int MPI_Win_get_errhandler(MPI_Win, MPI_Errhandler*);
1140	int MPI_Win_set_errhandler(MPI_Win, MPI_Errhandler);
1141	int MPI_Type_create_f90_integer(int, MPI_Datatype*);
1142	int MPI_Type_create_f90_real(int, int, MPI_Datatype*);
1143	int MPI_Type_create_f90_complex(int, int, MPI_Datatype*);
1144	int MPI_Reduce_local(void* inbuf, void* inoutbuf, int count, MPI_Datatype datatype, MPI_Op op);
1145	int MPI_Op_commutative(MPI_Op op, int* commute);
1146	int MPI_Reduce_scatter_block(void* sendbuf, void* recvbuf, int recvcount, MPI_Datatype datatype, MPI_Op op, MPI_Comm comm);
1147	int MPI_Dist_graph_create_adjacent(MPI_Comm comm_old, int indegree, int [], int [], int outdegree, int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
1148	int MPI_Dist_graph_create(MPI_Comm comm_old, int n, int [], int [], int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
1149	int MPI_Dist_graph_neighbors_count(MPI_Comm comm, int* indegree, int* outdegree, int* weighted);
1150	int MPI_Dist_graph_neighbors(MPI_Comm comm, int maxindegree, int [], int [], int maxoutdegree, int [], int []);
1151	const extern int* MPI_UNWEIGHTED;
1152	extern MPI_Fint* MPI_F_STATUS_IGNORE;
1153	extern MPI_Fint* MPI_F_STATUSES_IGNORE;
1154	const extern struct MPIR_T_pvar_handle* MPI_T_PVAR_ALL_HANDLES;
1155	//======================== comm.cvh ========================
1156	/*@ pure;
1157	@ depends_on \nothing;
1158	@ executes_when $true;
1159	@*/
1160	$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
1161	/*@ pure;
1162	@ depends_on \nothing;
1163	@ executes_when $true;
1164	@*/
1165	$atomic_f int $message_source($message message);
1166	/*@ pure;
1167	@ depends_on \nothing;
1168	@ executes_when $true;
1169	@*/
1170	$atomic_f int $message_tag($message message);
1171	/*@ pure;
1172	@ depends_on \nothing;
1173	@ executes_when $true;
1174	@*/
1175	$atomic_f int $message_dest($message message);
1176	/*@ pure;
1177	@ depends_on \nothing;
1178	@ executes_when $true;
1179	@*/
1180	$atomic_f int $message_size($message message);
1181	/*@ depends_on \write(buf);
1182	@ executes_when $true;
1183	@*/
1184	$atomic_f void $message_unpack($message message, void* buf, int size);
1185	/*@ depends_on \nothing;
1186	@ assigns \nothing;
1187	@ reads \nothing;
1188	@*/
1189	$atomic_f $gcomm $gcomm_create($scope scope, int size);
1190	/*@ depends_on \write(junkMsgs), \write(gcomm);
1191	@ assigns junkMsgs, gcomm;
1192	@*/
1193	$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
1194	/*@ depends_on \nothing;
1195	@ executes_when $true;
1196	@*/
1197	$system[comm] void $gcomm_dup($comm comm, $comm newcomm);
1198	$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
1199	/*@ depends_on \write(comm);
1200	@ assigns comm;
1201	@ reads \nothing;
1202	@*/
1203	$atomic_f void $comm_destroy($comm comm);
1204	/*@ pure;
1205	@ depends_on \nothing;
1206	@*/
1207	$atomic_f int $comm_size($comm comm);
1208	/*@ pure;
1209	@ depends_on \nothing;
1210	@ executes_when $true;
1211	@*/
1212	$atomic_f int $comm_place($comm comm);
1213	/*@ depends_on \write(comm);
1214	@ executes_when $true;
1215	@*/
1216	$system[comm] void $comm_enqueue($comm comm, $message message);
1217	/*@ pure;
1218	@ depends_on \write(comm);
1219	@ executes_when $true;
1220	@*/
1221	$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
1222	/*@ pure;
1223	@ depends_on \write(comm);
1224	@ executes_when $true;
1225	@*/
1226	$system[comm] $message $comm_seek($comm comm, int source, int tag);
1227	/*@ depends_on \write(comm);
1228	@ executes_when $comm_probe(comm, source, tag);
1229	@*/
1230	$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
1231	//====================== civl-mpi.cvh ======================
1232	int sizeofDatatype(MPI_Datatype);
1233	$abstract double $mpi_time(int i);
1234	$mpi_gcomm $mpi_gcomm_create($scope, int);
1235	void $mpi_gcomm_destroy($mpi_gcomm);
1236	MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
1237	void $mpi_comm_destroy(MPI_Comm, $mpi_state);
1238	int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
1239	int $mpi_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
1240	int $mpi_sendrecv(void* sendbuf, int sendcount, MPI_Datatype sendtype, int dest, int sendtag, void* recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status* status);
1241	int $mpi_collective_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
1242	int $mpi_collective_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status, char*);
1243	int $mpi_bcast(void, int, MPI_Datatype, int, int, MPI_Comm, char);
1244	int $mpi_reduce(void, void, int, MPI_Datatype, MPI_Op, int, int, MPI_Comm, char*);
1245	int $mpi_gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
1246	int $mpi_gatherv(void, int, MPI_Datatype, void, int [], int [], MPI_Datatype, int, int, MPI_Comm, char*);
1247	int $mpi_scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
1248	int $mpi_scatterv(void, int [], int [], MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
1249	void* $mpi_pointer_add(void*, int, MPI_Datatype);
1250	$system[mpi] int $mpi_new_gcomm($scope, $mpi_gcomm);
1251	$system[mpi] $mpi_gcomm $mpi_get_gcomm($scope, int);
1252	int $mpi_comm_dup($scope, MPI_Comm, MPI_Comm, char);
1253	int $mpi_comm_free(MPI_Comm*, $mpi_state);
1254	$system[mpi] $scope $mpi_root_scope($comm);
1255	$system[mpi] $scope $mpi_proc_scope($comm);
1256	$system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
1257	$bundle $mpi_create_coroutine_entry(int routineTag, int root, int op, int numDatatypes, int* datatypes);
1258	void $mpi_diff_coroutine_entries($bundle specEntry, $bundle mineEntry, int rank);
1259	void $mpi_coassert(MPI_Comm, _Bool);
1260	_Bool $mpi_isRecvBufEmpty(int x);
1261	/*@ depends_on \nothing;
1262	@*/
1263	$system[mpi] void $mpi_p2pSendShot(int commID, $message msg, int place);
1264	/*@ depends_on \nothing;
1265	@*/
1266	$system[mpi] void $mpi_colSendShot(int commID, $message msg, int place);
1267	/*@ depends_on \nothing;
1268	@*/
1269	$system[mpi] void $mpi_p2pRecvShot(int commID, int source, int dest, int tag);
1270	/*@ depends_on \nothing;
1271	@*/
1272	$system[mpi] void $mpi_colRecvShot(int commID, int source, int dest, int tag);
1273	//======================== stdlib.h ========================
1274	typedef struct _div_t{
1275	int quot;
1276	int rem;
1277	} div_t;
1278	typedef struct _ldiv_t{
1279	long quot;
1280	long rem;
1281	} ldiv_t;
1282	typedef struct _lldiv_t{
1283	long long quot;
1284	long long rem;
1285	} lldiv_t;
1286	double atof(char* nptr);
1287	int atoi(char* nptr);
1288	long atol(char* nptr);
1289	long long atoll(char* nptr);
1290	double strtod(char* restrict nptr, char** restrict endptr);
1291	float strtof(char* restrict nptr, char** restrict endptr);
1292	long double strtold(char* restrict nptr, char** restrict endptr);
1293	long strtol(char* restrict nptr, char** restrict endptr, int base);
1294	long long strtoll(char* restrict nptr, char** restrict endptr, int base);
1295	unsigned long strtoul(char* restrict nptr, char** restrict endptr, int base);
1296	unsigned long long strtoull(char* restrict nptr, char** restrict endptr, int base);
1297	$system[stdlib] int rand(void);
1298	$system[stdlib] void srand(unsigned seed);
1299	$system[stdlib] long random(void);
1300	$system[stdlib] void srandom(unsigned seed);
1301	void* aligned_alloc(size_t alignment, size_t size);
1302	void* calloc(size_t nmemb, size_t size);
1303	$system[stdlib] void free(void* ptr);
1304	$system[stdlib] void* malloc(size_t size);
1305	void* realloc(void* ptr, size_t size);
1306	_Noreturn void abort(void);
1307	int atexit( (void (void))* func);
1308	int at_quick_exit( (void (void))* func);
1309	$system[stdlib] void exit(int status);
1310	_Noreturn void _Exit(int status);
1311	char* getenv(char* name);
1312	_Noreturn void quick_exit(int status);
1313	int system(char* string);
1314	void* bsearch(void* key, void* base, size_t nmemb, size_t size, (int (void, void))* compar);
1315	void qsort(void* base, size_t nmemb, size_t size, (int (void, void))* compar);
1316	int abs(int j);
1317	long labs(long j);
1318	long long llabs(long long j);
1319	div_t div(int numer, int denom);
1320	ldiv_t ldiv(long numer, long denom);
1321	lldiv_t lldiv(long long numer, long long denom);
1322	int mblen(char* s, size_t n);
1323	int mbtowc(wchar_t* restrict pwc, char* restrict s, size_t n);
1324	int wctomb(char* s, wchar_t wchar);
1325	size_t mbstowcs(wchar_t* restrict pwcs, char* restrict s, size_t n);
1326	size_t wcstombs(char* restrict s, wchar_t* restrict pwcs, size_t n);
1327	typedef int errno_t;
1328	typedef size_t rsize_t;
1329	typedef (void (char* restrict msg, void* restrict ptr, errno_t error))* constraint_handler_t;
1330	constraint_handler_t set_constraint_handler_s(constraint_handler_t handler);
1331	void abort_handler_s(char* restrict msg, void* restrict ptr, errno_t error);
1332	void ignore_handler_s(char* restrict msg, void* restrict ptr, errno_t error);
1333	errno_t getenv_s(size_t* restrict len, char* restrict value, rsize_t maxsize, char* restrict name);
1334	void* bsearch_s(void* key, void* base, rsize_t nmemb, rsize_t size, (int (void* k, void* y, void* context))* compar, void* context);
1335	errno_t qsort_s(void* base, rsize_t nmemb, rsize_t size, (int (void* x, void* y, void* context))* compar, void* context);
1336	errno_t wctomb_s(int* restrict status, char* restrict s, rsize_t smax, wchar_t wc);
1337	errno_t mbstowcs_s(size_t* restrict retval, wchar_t* restrict dst, rsize_t dstmax, char* restrict src, rsize_t len);
1338	errno_t wcstombs_s(size_t* restrict retval, char* restrict dst, rsize_t dstmax, wchar_t* restrict src, rsize_t len);
1339	//======================= pointer.cvh ======================
1340	/*@ depends_on \write(obj);
1341	@ executes_when $true;
1342	@*/
1343	$system[pointer] void $set_default(void* obj);
1344	/*@ depends_on \write(obj1, obj2, result);
1345	@ executes_when $true;
1346	@*/
1347	$system[pointer] void $apply(void* obj1, $operation op, void* obj2, void* result);
1348	/*@ depends_on \write(x, y);
1349	@ executes_when $true;
1350	@*/
1351	$system[pointer] _Bool $equals(void* x, void* y);
1352	/*@ depends_on \write(x, y);
1353	@ executes_when $true;
1354	@*/
1355	$system[pointer] void $assert_equals(void* x, void* y, ...);
1356	/*@ depends_on \write(obj1, obj2);
1357	@ executes_when $true;
1358	@*/
1359	$system[pointer] _Bool $contains(void* obj1, void* obj2);
1360	/*@ depends_on \nothing;
1361	@ executes_when $true;
1362	@*/
1363	$system[pointer] void* $translate_ptr(void* ptr, void* obj);
1364	/*@ depends_on \write(ptr, value);
1365	@ executes_when $true;
1366	@*/
1367	$system[pointer] void $copy(void* ptr, void* value);
1368	/*@ depends_on \write(array);
1369	@ executes_when $true;
1370	@*/
1371	$system[pointer] void $leaf_node_ptrs(void* array, void* obj);
1372	/*@ depends_on \nothing;
1373	@ executes_when $true;
1374	@*/
1375	$system[pointer] _Bool $is_identity_ref(void* obj);
1376	/*@ depends_on \write(obj);
1377	@ executes_when $true;
1378	@*/
1379	$system[pointer] void $set_leaf_nodes(void* obj, int value);
1380	/*@ depends_on \write(obj);
1381	@ executes_when $true;
1382	@*/
1383	$system[pointer] _Bool $leaf_nodes_equal_to(void* obj, int value);
1384	/*@ depends_on \write(obj);
1385	@ executes_when $true;
1386	@*/
1387	$system[pointer] _Bool $has_leaf_node_equal_to(void* obj, int value);
1388	/*@ depends_on \nothing;
1389	@ executes_when $true;
1390	@*/
1391	$system[pointer] _Bool $is_derefable_pointer(void* ptr);
1392	/*@ depends_on \nothing;
1393	@ executes_when $true;
1394	@*/
1395	$system[pointer] void* $pointer_add(void* ptr, int offset, int type_size);
1396	//========================= mpi.cvl ========================
1397	struct MPI_Request{
1398	MPI_Status status;
1399	_Bool isSend;
1400	};
1401	struct MPI_Comm{
1402	$comm p2p;
1403	$comm col;
1404	$collator collator;
1405	$barrier barrier;
1406	int gcommIndex;
1407	};
1408	$mpi_state _mpi_state = _MPI_UNINIT;
1409	int $mpi_init(void)
1410	{
1411	$assert(_mpi_state == _MPI_UNINIT, "Process can only call MPI_Init() at most once.");
1412	_mpi_state = _MPI_INIT;
1413	return 0;
1414	}
1415	int MPI_Finalize(void)
1416	{
1417	$assert(_mpi_state == _MPI_INIT, "Process can only call MPI_Finalize() after the MPI enviroment is created and before cleaned.");
1418	_mpi_state = _MPI_FINALIZED;
1419	return 0;
1420	}
1421	double MPI_Wtime()
1422	{
1423	double result;
1424	int CMPI_time_count = $next_time_count();
1425	$assert(_mpi_state == _MPI_INIT, "MPI_Wtime() cannot be invoked without MPI_Init() being called before.\n");
1426	result = $mpi_time(CMPI_time_count);
1427	if (CMPI_time_count > 0)
1428	{
1429	$assume(result > $mpi_time(CMPI_time_count - 1));
1430	}
1431	else
1432	{
1433	$assume(result > 0);
1434	}
1435	return result;
1436	}
1437	int MPI_Comm_size(MPI_Comm comm, int* size)
1438	{
1439	$assert(_mpi_state == _MPI_INIT, "MPI_Comm_size() cannot be invoked without MPI_Init() being called before.\n");
1440	*size = $comm_size(comm.p2p);
1441	return 0;
1442	}
1443	int MPI_Comm_rank(MPI_Comm comm, int* rank)
1444	{
1445	$assert(_mpi_state == _MPI_INIT, "MPI_Comm_rank() cannot be invoked without MPI_Init() being called before.\n");
1446	*rank = $comm_place(comm.p2p);
1447	return 0;
1448	}
1449	int MPI_Send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm)
1450	{
1451	$assert(_mpi_state == _MPI_INIT, "MPI_Send() cannot be invoked without MPI_Init() being called before.\n");
1452	$mpi_check_buffer(buf, count, datatype);
1453	return $mpi_send(buf, count, datatype, dest, tag, comm);
1454	}
1455	int MPI_Recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status)
1456	{
1457	$assert(_mpi_state == _MPI_INIT, "MPI_Recv() cannot be invoked without MPI_Init() being called before.\n");
1458	return $mpi_recv(buf, count, datatype, source, tag, comm, status);
1459	}
1460	int MPI_Get_count(MPI_Status* status, MPI_Datatype datatype, int* count)
1461	{
1462	$assert(_mpi_state == _MPI_INIT, "MPI_Get_count() cannot be invoked without MPI_Init() being called before.\n");
1463	*count = (status)->size / sizeofDatatype(datatype);
1464	return 0;
1465	}
1466	int MPI_Get_processor_name(char* name, int* resultlen)
1467	{
1468	$abstract int MPI_GET_PROCESSOR_NAME(char, int);
1469	return MPI_GET_PROCESSOR_NAME(name, resultlen);
1470	}
1471	int MPI_Sendrecv(void* sendbuf, int sendcount, MPI_Datatype sendtype, int dest, int sendtag, void* recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status* status)
1472	{
1473	$assert(_mpi_state == _MPI_INIT, "MPI_Sendrecv() cannot be invoked without MPI_Init() being called before.\n");
1474	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1475	$mpi_sendrecv(sendbuf, sendcount, sendtype, dest, sendtag, recvbuf, recvcount, recvtype, source, recvtag, comm, status);
1476	return 0;
1477	}
1478	int MPI_Bcast(void* buf, int count, MPI_Datatype datatype, int root, MPI_Comm comm)
1479	{
1480	int place = $comm_place(comm.col);
1481	int nprocs = $comm_size(comm.col);
1482	int datatypes[1] = {(int)datatype};
1483	$bundle checkerEntry;
1484	$bundle specEntry;
1485	$assert(_mpi_state == _MPI_INIT, "MPI_Bcast() cannot be invoked without MPI_Init() being called before.\n");
1486	if (place == root)
1487	$mpi_check_buffer(buf, count, datatype);
1488	checkerEntry = $mpi_create_coroutine_entry(9999, root, -1, 1, datatypes);
1489	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1490	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1491	$mpi_bcast(buf, count, datatype, root, 9999, comm, "MPI_Bcast()");
1492	return 0;
1493	}
1494	int MPI_Reduce(void* sendbuf, void* recvbuf, int count, MPI_Datatype datatype, MPI_Op op, int root, MPI_Comm comm)
1495	{
1496	int place = $comm_place(comm.col);
1497	int nprocs = $comm_size(comm.col);
1498	int datatypes[1] = {(int)datatype};
1499	$bundle checkerEntry;
1500	$bundle specEntry;
1501	$assert(_mpi_state == _MPI_INIT, "MPI_Reduce() cannot be invoked without MPI_Init() being called before.\n");
1502	checkerEntry = $mpi_create_coroutine_entry(9998, root, (int)op, 1, datatypes);
1503	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1504	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1505	$mpi_check_buffer(sendbuf, count, datatype);
1506	$mpi_reduce(sendbuf, recvbuf, count, datatype, op, root, 9998, comm, "MPI_Reduce()");
1507	return 0;
1508	}
1509	int MPI_Allreduce(void* sendbuf, void* recvbuf, int count, MPI_Datatype datatype, MPI_Op op, MPI_Comm comm)
1510	{
1511	int root = 0;
1512	int place = $comm_place(comm.col);
1513	int nprocs = $comm_size(comm.col);
1514	int datatypes[1] = {(int)datatype};
1515	MPI_Status status;
1516	$bundle checkerEntry;
1517	$bundle specEntry;
1518	$assert(_mpi_state == _MPI_INIT, "MPI_Allreduce() cannot be invoked without MPI_Init() being called before.\n");
1519	$mpi_check_buffer(sendbuf, count, datatype);
1520	checkerEntry = $mpi_create_coroutine_entry(9997, root, (int)op, 1, datatypes);
1521	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1522	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1523	$mpi_reduce(sendbuf, recvbuf, count, datatype, op, root, 9997, comm, "MPI_Allreduce()");
1524	$mpi_bcast(recvbuf, count, datatype, root, 9997, comm, "MPI_Allreduce()");
1525	return 0;
1526	}
1527	int MPI_Barrier(MPI_Comm comm)
1528	{
1529	int place = $comm_place(comm.col);
1530	int nprocs = $comm_size(comm.col);
1531	$bundle checkerEntry;
1532	$bundle specEntry;
1533	$assert(_mpi_state == _MPI_INIT, "MPI_Barrier() cannot be invoked without MPI_Init() being called before.\n");
1534	checkerEntry = $mpi_create_coroutine_entry(9987, 0, -1, 0, (void*)0);
1535	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1536	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1537	$barrier_call(comm.barrier);
1538	return 0;
1539	}
1540	int MPI_Gather(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, MPI_Comm comm)
1541	{
1542	int place = $comm_place(comm.col);
1543	int nprocs = $comm_size(comm.col);
1544	int datatypes[2] = {(int)sendtype, (int)recvtype};
1545	$bundle checkerEntry;
1546	$bundle specEntry;
1547	$assert(_mpi_state == _MPI_INIT, "MPI_Gather() cannot be invoked without MPI_Init() being called before.\n");
1548	if (sendbuf != (void*)(-1))
1549	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1550	checkerEntry = $mpi_create_coroutine_entry(9996, root, -1, 2, datatypes);
1551	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1552	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1553	$mpi_gather(sendbuf, sendcount, sendtype, recvbuf, recvcount, recvtype, root, 9996, comm, "MPI_Gather()");
1554	return 0;
1555	}
1556	int MPI_Scatter(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, MPI_Comm comm)
1557	{
1558	int place = $comm_place(comm.col);
1559	int nprocs = $comm_size(comm.col);
1560	int datatypes[2] = {(int)sendtype, (int)recvtype};
1561	$bundle checkerEntry;
1562	$bundle specEntry;
1563	$assert(_mpi_state == _MPI_INIT, "MPI_Scatter() cannot be invoked without MPI_Init() being called before.\n");
1564	if (place == root)
1565	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1566	checkerEntry = $mpi_create_coroutine_entry(9995, root, -1, 2, datatypes);
1567	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1568	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1569	$mpi_scatter(sendbuf, sendcount, sendtype, recvbuf, recvcount, recvtype, root, 9995, comm, "MPI_Scatter()");
1570	return 0;
1571	}
1572	int MPI_Gatherv(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcounts[], int displs[], MPI_Datatype recvtype, int root, MPI_Comm comm)
1573	{
1574	int place = $comm_place(comm.col);
1575	int nprocs = $comm_size(comm.col);
1576	int datatypes[2] = {(int)sendtype, (int)recvtype};
1577	int recvcount = 0;
1578	$bundle checkerEntry;
1579	$bundle specEntry;
1580	$assert(_mpi_state == _MPI_INIT, "MPI_Gatherv() cannot be invoked without MPI_Init() being called before.\n");
1581	if (sendbuf != (void*)(-1))
1582	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1583	checkerEntry = $mpi_create_coroutine_entry(9994, root, -1, 2, datatypes);
1584	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1585	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1586	$mpi_gatherv(sendbuf, sendcount, sendtype, recvbuf, recvcounts, displs, recvtype, root, 9994, comm, "MPI_Gatherv()");
1587	return 0;
1588	}
1589	int MPI_Scatterv(void* sendbuf, int sendcounts[], int displs[], MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, MPI_Comm comm)
1590	{
1591	int place = $comm_place(comm.col);
1592	int nprocs = $comm_size(comm.col);
1593	int datatypes[2] = {(int)sendtype, (int)recvtype};
1594	int sendcount = 0;
1595	$bundle checkerEntry;
1596	$bundle specEntry;
1597	$assert(_mpi_state == _MPI_INIT, "MPI_Scatterv() cannot be invoked without MPI_Init() being called before.\n");
1598	if (place == root)
1599	{
1600	for (int i = 0; i < nprocs; i++)
1601	sendcount += sendcounts[i];
1602	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1603	}
1604	checkerEntry = $mpi_create_coroutine_entry(9993, root, -1, 2, datatypes);
1605	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1606	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1607	$mpi_scatterv(sendbuf, sendcounts, displs, sendtype, recvbuf, recvcount, recvtype, root, 9993, comm, "MPI_Scatterv()");
1608	return 0;
1609	}
1610	int MPI_Allgather(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, MPI_Comm comm)
1611	{
1612	int place = $comm_place(comm.col);
1613	int nprocs = $comm_size(comm.col);
1614	int datatypes[2] = {(int)sendtype, (int)recvtype};
1615	$bundle checkerEntry;
1616	$bundle specEntry;
1617	$assert(_mpi_state == _MPI_INIT, "MPI_Allgather() cannot be invoked without MPI_Init() being called before.\n");
1618	if (sendbuf != (void*)(-1))
1619	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1620	checkerEntry = $mpi_create_coroutine_entry(9992, 0, -1, 2, datatypes);
1621	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1622	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1623	$mpi_gather(sendbuf, sendcount, sendtype, recvbuf, recvcount, recvtype, 0, 9992, comm, "MPI_Allgather()");
1624	$mpi_bcast(recvbuf, recvcount * nprocs, recvtype, 0, 9992, comm, "MPI_Allgather()");
1625	return 0;
1626	}
1627	int MPI_Reduce_scatter(void* sendbuf, void* recvbuf, int recvcount[], MPI_Datatype datatype, MPI_Op op, MPI_Comm comm)
1628	{
1629	int total_count;
1630	int i;
1631	int nprocs = $comm_size(comm.col);
1632	int rank = $comm_place(comm.col);
1633	int root = 0;
1634	int displs[nprocs];
1635	int datatypes[1] = {(int)datatype};
1636	$bundle checkerEntry;
1637	$bundle specEntry;
1638	$assert(_mpi_state == _MPI_INIT, "MPI_Reduce_scatter() cannot be invoked without MPI_Init() being called before.\n");
1639	$mpi_check_buffer(sendbuf, recvcount[rank], datatype);
1640	for (total_count = 0, i = 0; i < nprocs; i++)
1641	{
1642	displs[i] = total_count;
1643	total_count += recvcount[i];
1644	}
1645	checkerEntry = $mpi_create_coroutine_entry(9991, root, (int)op, 1, datatypes);
1646	specEntry = $collator_check(comm.collator, rank, nprocs, checkerEntry);
1647	$mpi_diff_coroutine_entries(specEntry, checkerEntry, rank);
1648	$mpi_reduce(sendbuf, sendbuf, total_count, datatype, op, root, 9991, comm, "MPI_Reduce_scatter()");
1649	$mpi_scatterv(sendbuf, recvcount, displs, datatype, recvbuf, recvcount[rank], datatype, root, 9991, comm, "MPI_Reduce_scatter()");
1650	return 0;
1651	}
1652	int MPI_Alltoall(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, MPI_Comm comm)
1653	{
1654	int nprocs = $comm_size(comm.col);
1655	int rank = $comm_place(comm.col);
1656	int root = 0;
1657	int displs[nprocs];
1658	int sendcounts[nprocs];
1659	int datatypes[2] = {(int)sendtype, (int)recvtype};
1660	$bundle checkerEntry;
1661	$bundle specEntry;
1662	for (int i = 0; i < nprocs; i++)
1663	{
1664	sendcounts[i] = sendcount;
1665	displs[i] = i == 0 ? 0 : (displs[i - 1]) + sendcount;
1666	}
1667	$assert(_mpi_state == _MPI_INIT, "MPI_Alltoall() cannot be invoked without MPI_Init() being called before.\n");
1668	$mpi_check_buffer(sendbuf, sendcount * nprocs, sendtype);
1669	checkerEntry = $mpi_create_coroutine_entry(9990, root, -1, 2, datatypes);
1670	specEntry = $collator_check(comm.collator, rank, nprocs, checkerEntry);
1671	$mpi_diff_coroutine_entries(specEntry, checkerEntry, rank);
1672	for (int i = 0; i < nprocs; i++)
1673	{
1674	void* ptr = $mpi_pointer_add(recvbuf, i * sendcount, recvtype);
1675	$mpi_scatterv(sendbuf, sendcounts, displs, sendtype, ptr, recvcount, recvtype, i, 9990, comm, "MPI_Alltoall()");
1676	}
1677	return 0;
1678	}
1679	int MPI_Alltoallv(void* sendbuf, int sendcounts[], int sdispls[], MPI_Datatype sendtype, void* recvbuf, int recvcounts[], int rdispls[], MPI_Datatype recvtype, MPI_Comm comm)
1680	{
1681	int nprocs = $comm_size(comm.col);
1682	int place = $comm_place(comm.col);
1683	int datatypes[2] = {(int)sendtype, (int)recvtype};
1684	int sendcount = 0;
1685	int recvcount = 0;
1686	$bundle checkerEntry;
1687	$bundle specEntry;
1688	$assert(_mpi_state == _MPI_INIT, "MPI_Alltoallv() cannot be invoked without MPI_Init() being called before.\n");
1689	for (int i = 0; i < nprocs; i++)
1690	{
1691	sendcount += sendcounts[i];
1692	recvcount += recvcounts[i];
1693	}
1694	$mpi_check_buffer(sendbuf, sendcount, sendtype);
1695	checkerEntry = $mpi_create_coroutine_entry(9989, 0, -1, 2, datatypes);
1696	specEntry = $collator_check(comm.collator, place, nprocs, checkerEntry);
1697	$mpi_diff_coroutine_entries(specEntry, checkerEntry, place);
1698	for (int i = 0; i < nprocs; i++)
1699	{
1700	void* ptr = $mpi_pointer_add(recvbuf, rdispls[i], recvtype);
1701	$mpi_scatterv(sendbuf, sendcounts, sdispls, sendtype, ptr, recvcounts[i], recvtype, i, 9989, comm, "MPI_Alltoallv()");
1702	}
1703	return 0;
1704	}
1705	int MPI_Alltoallw(void* sendbuf, int sendcounts[], int sdispls[], MPI_Datatype sendtypes[], void* recvbuf, int recvcounts[], int rdispls[], MPI_Datatype recvtypes[], MPI_Comm comm)
1706	{
1707	int nprocs = $comm_size(comm.col);
1708	int place = $comm_place(comm.col);
1709	$assert(_mpi_state == _MPI_INIT, "MPI_Alltoallw() cannot be invoked without MPI_Init() being called before.\n");
1710	for (int i = 0; i < nprocs; i++)
1711	{
1712	void* ptr = $mpi_pointer_add(recvbuf, rdispls[i], recvtypes[i]);
1713	void* sendptr = $mpi_pointer_add(sendbuf, sdispls[i], sendtypes[i]);
1714	$mpi_check_buffer(sendptr, sendcounts[i], sendtypes[i]);
1715	$mpi_scatterv(sendbuf, sendcounts, sdispls, sendtypes[i], ptr, recvcounts[i], recvtypes[i], i, 9988, comm, "MPI_Alltoallw()");
1716	}
1717	return 0;
1718	}
1719	int MPI_Comm_dup(MPI_Comm comm, MPI_Comm* newcomm)
1720	{
1721	$scope CMPI_PROC_SCOPE = $mpi_proc_scope(comm.col);
1722	$assert(_mpi_state == _MPI_INIT, "MPI_Comm_dup() cannot be invoked without MPI_Init() being called before.\n");
1723	$mpi_comm_dup(CMPI_PROC_SCOPE, comm, newcomm, "MPI_Comm_dup");
1724	return 0;
1725	}
1726	int MPI_Comm_free(MPI_Comm* comm)
1727	{
1728	$assert(_mpi_state == _MPI_INIT, "MPI_Comm_free() cannot be invoked without MPI_Init() being called before.\n");
1729	$assert($is_derefable_pointer(comm), "The argument of MPI_Comm_free is NULL.");
1730	$mpi_comm_free(comm, _mpi_state);
1731	return 0;
1732	}
1733	int MPI_Init_thread(int* argc, char*** argv, int required, int* provided)
1734	{
1735	_mpi_state = _MPI_INIT;
1736	*provided = 3;
1737	return 0;
1738	}
1739	//======================== civlc.cvh =======================
1740	$system[civlc] void $wait($proc p);
1741	$system[civlc] void $waitall($proc* procs, int numProcs);
1742	/*@ depends_on \nothing;
1743	@ executes_when $true;
1744	@*/
1745	$system[civlc] void $exit(void);
1746	/*@ depends_on \nothing;
1747	@ executes_when $true;
1748	@*/
1749	$system[civlc] int $choose_int(int n);
1750	/*@ depends_on \nothing;
1751	@ executes_when $true;
1752	@*/
1753	$system[civlc] void $assert(_Bool expr, ...);
1754	/*@ depends_on \nothing;
1755	@ executes_when $true;
1756	@*/
1757	$system[civlc] void $assume(_Bool expr);
1758	/*@ pure;
1759	@ depends_on \nothing;
1760	@ executes_when $true;
1761	@*/
1762	$system[civlc] void $elaborate(int x);
1763	/*@ depends_on \nothing;
1764	@ executes_when $true;
1765	@*/
1766	$system[civlc] int $next_time_count(void);
1767	/*@ pure;
1768	@ depends_on \nothing;
1769	@ executes_when $true;
1770	@*/
1771	$system[civlc] void $pathCondition(void);
1772	/*@ pure;
1773	@ depends_on \nothing;
1774	@ executes_when $true;
1775	@*/
1776	$system[civlc] _Bool $is_concrete_int(int value);
1777	/*@ depends_on \nothing;
1778	@ executes_when $true;
1779	@*/
1780	$system[civlc] void* $malloc($scope s, int size);
1781	/*@ depends_on \write(p);
1782	@ executes_when $true;
1783	@*/
1784	$system[civlc] void $free(void* p);
1785	/*@ depends_on \write(ptr);
1786	@ executes_when $true;
1787	@*/
1788	$system[civlc] void $havoc(void* ptr);
1789	/*@ pure;
1790	@ depends_on \nothing;
1791	@ executes_when $true;
1792	@*/
1793	$system[civlc] double $pow(double base, double exp);
1794	//======================= bundle.cvh =======================
1795	/*@ depends_on \nothing;
1796	@ executes_when $true;
1797	@*/
1798	$system[bundle] int $bundle_size($bundle b);
1799	/*@ depends_on \write(ptr);
1800	@ executes_when $true;
1801	@*/
1802	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
1803	/*@ depends_on \write(ptr);
1804	@ executes_when $true;
1805	@*/
1806	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
1807	/*@ depends_on \write(buf);
1808	@ executes_when $true;
1809	@*/
1810	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
1811	//===================== concurrency.cvh ====================
1812	/*@ depends_on \nothing;
1813	@ assigns \nothing;
1814	@ reads \nothing;
1815	@*/
1816	$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
1817	/*@ depends_on \write(gbarrier);
1818	@ reads \nothing;
1819	@ assigns gbarrier;
1820	@*/
1821	$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
1822	/*@ depends_on \nothing;
1823	@ assigns gbarrier;
1824	@ reads gbarrier;
1825	@*/
1826	$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
1827	/*@ depends_on \write(barrier);
1828	@ assigns barrier;
1829	@ reads \nothing;
1830	@*/
1831	$atomic_f void $barrier_destroy($barrier barrier);
1832	void $barrier_call($barrier barrier);
1833	/*@ depends_on \nothing;
1834	@ reads \nothing;
1835	@ assigns \nothing;
1836	@*/
1837	$atomic_f $gcollator $gcollator_create($scope scope);
1838	/*@ depends_on \write(gcollator);
1839	@ assigns gcollator;
1840	@ reads \nothing;
1841	@*/
1842	$atomic_f int $gcollator_destroy($gcollator gcollator);
1843	/*@ depends_on \nothing;
1844	@ executes_when $true;
1845	@*/
1846	$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
1847	/*@ depends_on \write(collator);
1848	@ executes_when $true;
1849	@*/
1850	$atomic_f void $collator_destroy($collator collator);
1851	/*@ depends_on \write(collator);
1852	@ executes_when $true;
1853	@*/
1854	$system[concurrency] $bundle $collator_check($collator collator, int place, int nprocs, $bundle entries);
1855	//======================== comm.cvh ========================
1856	/*@ pure;
1857	@ depends_on \nothing;
1858	@ executes_when $true;
1859	@*/
1860	$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
1861	/*@ pure;
1862	@ depends_on \nothing;
1863	@ executes_when $true;
1864	@*/
1865	$atomic_f int $message_source($message message);
1866	/*@ pure;
1867	@ depends_on \nothing;
1868	@ executes_when $true;
1869	@*/
1870	$atomic_f int $message_tag($message message);
1871	/*@ pure;
1872	@ depends_on \nothing;
1873	@ executes_when $true;
1874	@*/
1875	$atomic_f int $message_dest($message message);
1876	/*@ pure;
1877	@ depends_on \nothing;
1878	@ executes_when $true;
1879	@*/
1880	$atomic_f int $message_size($message message);
1881	/*@ depends_on \write(buf);
1882	@ executes_when $true;
1883	@*/
1884	$atomic_f void $message_unpack($message message, void* buf, int size);
1885	/*@ depends_on \nothing;
1886	@ assigns \nothing;
1887	@ reads \nothing;
1888	@*/
1889	$atomic_f $gcomm $gcomm_create($scope scope, int size);
1890	/*@ depends_on \write(junkMsgs), \write(gcomm);
1891	@ assigns junkMsgs, gcomm;
1892	@*/
1893	$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
1894	/*@ depends_on \nothing;
1895	@ executes_when $true;
1896	@*/
1897	$system[comm] void $gcomm_dup($comm comm, $comm newcomm);
1898	$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
1899	/*@ depends_on \write(comm);
1900	@ assigns comm;
1901	@ reads \nothing;
1902	@*/
1903	$atomic_f void $comm_destroy($comm comm);
1904	/*@ pure;
1905	@ depends_on \nothing;
1906	@*/
1907	$atomic_f int $comm_size($comm comm);
1908	/*@ pure;
1909	@ depends_on \nothing;
1910	@ executes_when $true;
1911	@*/
1912	$atomic_f int $comm_place($comm comm);
1913	/*@ depends_on \write(comm);
1914	@ executes_when $true;
1915	@*/
1916	$system[comm] void $comm_enqueue($comm comm, $message message);
1917	/*@ pure;
1918	@ depends_on \write(comm);
1919	@ executes_when $true;
1920	@*/
1921	$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
1922	/*@ pure;
1923	@ depends_on \write(comm);
1924	@ executes_when $true;
1925	@*/
1926	$system[comm] $message $comm_seek($comm comm, int source, int tag);
1927	/*@ depends_on \write(comm);
1928	@ executes_when $comm_probe(comm, source, tag);
1929	@*/
1930	$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
1931	//========================== mpi.h =========================
1932	MPI_Comm MPI_COMM_WORLD;
1933	MPI_Comm MPI_COMM_SELF;
1934	MPI_Comm MPI_COMM_PARENT;
1935	MPI_Comm MPI_COMM_TYPE_SHARED;
1936	int MPI_Send(void*, int, MPI_Datatype, int, int, MPI_Comm);
1937	int MPI_Recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
1938	int MPI_Get_count(MPI_Status, MPI_Datatype, int);
1939	int MPI_Bsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
1940	int MPI_Ssend(void*, int, MPI_Datatype, int, int, MPI_Comm);
1941	int MPI_Rsend(void*, int, MPI_Datatype, int, int, MPI_Comm);
1942	int MPI_Buffer_attach(void*, int);
1943	int MPI_Buffer_detach(void, int);
1944	int MPI_Isend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1945	int MPI_Ibsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1946	int MPI_Issend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1947	int MPI_Irsend(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1948	int MPI_Irecv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1949	int MPI_Wait(MPI_Request, MPI_Status);
1950	int MPI_Test(MPI_Request, int, MPI_Status*);
1951	int MPI_Request_free(MPI_Request*);
1952	int MPI_Waitany(int, MPI_Request, int, MPI_Status*);
1953	int MPI_Testany(int, MPI_Request, int, int, MPI_Status);
1954	int MPI_Waitall(int, MPI_Request, MPI_Status);
1955	int MPI_Testall(int, MPI_Request, int, MPI_Status*);
1956	int MPI_Waitsome(int, MPI_Request, int, int, MPI_Status);
1957	int MPI_Testsome(int, MPI_Request, int, int, MPI_Status);
1958	int MPI_Iprobe(int, int, MPI_Comm, int, MPI_Status);
1959	int MPI_Probe(int, int, MPI_Comm, MPI_Status*);
1960	int MPI_Cancel(MPI_Request*);
1961	int MPI_Test_cancelled(MPI_Status, int);
1962	int MPI_Send_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1963	int MPI_Bsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1964	int MPI_Ssend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1965	int MPI_Rsend_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1966	int MPI_Recv_init(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Request);
1967	int MPI_Start(MPI_Request*);
1968	int MPI_Startall(int, MPI_Request*);
1969	int MPI_Sendrecv(void, int, MPI_Datatype, int, int, void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
1970	int MPI_Sendrecv_replace(void, int, MPI_Datatype, int, int, int, int, MPI_Comm, MPI_Status);
1971	int MPI_Type_contiguous(int, MPI_Datatype, MPI_Datatype*);
1972	int MPI_Type_vector(int, int, int, MPI_Datatype, MPI_Datatype*);
1973	int MPI_Type_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
1974	int MPI_Type_indexed(int, int, int, MPI_Datatype, MPI_Datatype*);
1975	int MPI_Type_hindexed(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
1976	int MPI_Type_struct(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype);
1977	int MPI_Address(void, MPI_Aint);
1978	int MPI_Type_extent(MPI_Datatype, MPI_Aint*);
1979	int MPI_Type_size(MPI_Datatype, int*);
1980	int MPI_Type_lb(MPI_Datatype, MPI_Aint*);
1981	int MPI_Type_ub(MPI_Datatype, MPI_Aint*);
1982	int MPI_Type_commit(MPI_Datatype*);
1983	int MPI_Type_free(MPI_Datatype*);
1984	int MPI_Get_elements(MPI_Status, MPI_Datatype, int);
1985	int MPI_Pack(void, int, MPI_Datatype, void, int, int*, MPI_Comm);
1986	int MPI_Unpack(void, int, int, void*, int, MPI_Datatype, MPI_Comm);
1987	int MPI_Pack_size(int, MPI_Datatype, MPI_Comm, int*);
1988	int MPI_Barrier(MPI_Comm);
1989	int MPI_Bcast(void*, int, MPI_Datatype, int, MPI_Comm);
1990	int MPI_Gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
1991	int MPI_Gatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, int, MPI_Comm);
1992	int MPI_Scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
1993	int MPI_Scatterv(void, int, int, MPI_Datatype, void, int, MPI_Datatype, int, MPI_Comm);
1994	int MPI_Allgather(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
1995	int MPI_Allgatherv(void, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
1996	int MPI_Alltoall(void, int, MPI_Datatype, void, int, MPI_Datatype, MPI_Comm);
1997	int MPI_Alltoallv(void, int, int, MPI_Datatype, void, int, int, MPI_Datatype, MPI_Comm);
1998	int MPI_Reduce(void, void, int, MPI_Datatype, MPI_Op, int, MPI_Comm);
1999	int MPI_Op_create(MPI_User_function, int, MPI_Op);
2000	int MPI_Op_free(MPI_Op*);
2001	int MPI_Allreduce(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
2002	int MPI_Reduce_scatter(void, void, int*, MPI_Datatype, MPI_Op, MPI_Comm);
2003	int MPI_Scan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
2004	int MPI_Group_size(MPI_Group, int*);
2005	int MPI_Group_rank(MPI_Group, int*);
2006	int MPI_Group_translate_ranks(MPI_Group, int, int, MPI_Group, int);
2007	int MPI_Group_compare(MPI_Group, MPI_Group, int*);
2008	int MPI_Comm_group(MPI_Comm, MPI_Group*);
2009	int MPI_Group_union(MPI_Group, MPI_Group, MPI_Group*);
2010	int MPI_Group_intersection(MPI_Group, MPI_Group, MPI_Group*);
2011	int MPI_Group_difference(MPI_Group, MPI_Group, MPI_Group*);
2012	int MPI_Group_incl(MPI_Group, int, int, MPI_Group);
2013	int MPI_Group_excl(MPI_Group, int, int, MPI_Group);
2014	int MPI_Group_range_incl(MPI_Group, int, int [][3], MPI_Group*);
2015	int MPI_Group_range_excl(MPI_Group, int, int [][3], MPI_Group*);
2016	int MPI_Group_free(MPI_Group*);
2017	int MPI_Comm_size(MPI_Comm, int*);
2018	int MPI_Comm_rank(MPI_Comm, int*);
2019	int MPI_Comm_compare(MPI_Comm, MPI_Comm, int*);
2020	int MPI_Comm_dup(MPI_Comm, MPI_Comm*);
2021	int MPI_Comm_create(MPI_Comm, MPI_Group, MPI_Comm*);
2022	int MPI_Comm_split(MPI_Comm, int, int, MPI_Comm*);
2023	int MPI_Comm_free(MPI_Comm*);
2024	int MPI_Comm_test_inter(MPI_Comm, int*);
2025	int MPI_Comm_remote_size(MPI_Comm, int*);
2026	int MPI_Comm_remote_group(MPI_Comm, MPI_Group*);
2027	int MPI_Intercomm_create(MPI_Comm, int, MPI_Comm, int, int, MPI_Comm*);
2028	int MPI_Intercomm_merge(MPI_Comm, int, MPI_Comm*);
2029	int MPI_Keyval_create(MPI_Copy_function, MPI_Delete_function, int, void);
2030	int MPI_Keyval_free(int*);
2031	int MPI_Attr_put(MPI_Comm, int, void*);
2032	int MPI_Attr_get(MPI_Comm, int, void, int);
2033	int MPI_Attr_delete(MPI_Comm, int);
2034	int MPI_Topo_test(MPI_Comm, int*);
2035	int MPI_Cart_create(MPI_Comm, int, int, int, int, MPI_Comm*);
2036	int MPI_Dims_create(int, int, int*);
2037	int MPI_Graph_create(MPI_Comm, int, int, int, int, MPI_Comm*);
2038	int MPI_Graphdims_get(MPI_Comm, int, int);
2039	int MPI_Graph_get(MPI_Comm, int, int, int, int);
2040	int MPI_Cartdim_get(MPI_Comm, int*);
2041	int MPI_Cart_get(MPI_Comm, int, int, int, int*);
2042	int MPI_Cart_rank(MPI_Comm, int, int);
2043	int MPI_Cart_coords(MPI_Comm, int, int, int*);
2044	int MPI_Graph_neighbors_count(MPI_Comm, int, int*);
2045	int MPI_Graph_neighbors(MPI_Comm, int, int, int*);
2046	int MPI_Cart_shift(MPI_Comm, int, int, int, int);
2047	int MPI_Cart_sub(MPI_Comm, int, MPI_Comm);
2048	int MPI_Cart_map(MPI_Comm, int, int, int, int*);
2049	int MPI_Graph_map(MPI_Comm, int, int, int, int*);
2050	int MPI_Get_processor_name(char, int);
2051	int MPI_Get_version(int, int);
2052	int MPI_Errhandler_create(MPI_Handler_function, MPI_Errhandler);
2053	int MPI_Errhandler_set(MPI_Comm, MPI_Errhandler);
2054	int MPI_Errhandler_get(MPI_Comm, MPI_Errhandler*);
2055	int MPI_Errhandler_free(MPI_Errhandler*);
2056	int MPI_Error_string(int, char, int);
2057	int MPI_Error_class(int, int*);
2058	double MPI_Wtime(void);
2059	double MPI_Wtick(void);
2060	int MPI_Init(int, char**);
2061	int MPI_Finalize(void);
2062	int MPI_Initialized(int*);
2063	$system[mpi] int MPI_Abort(MPI_Comm, int);
2064	int MPI_Pcontrol(const int, ...);
2065	int MPI_DUP_FN(MPI_Comm, int, void, void, void, int);
2066	int MPI_Close_port(char*);
2067	int MPI_Comm_accept(char, MPI_Info, int, MPI_Comm, MPI_Comm);
2068	int MPI_Comm_connect(char, MPI_Info, int, MPI_Comm, MPI_Comm);
2069	int MPI_Comm_disconnect(MPI_Comm*);
2070	int MPI_Comm_get_parent(MPI_Comm*);
2071	int MPI_Comm_join(int, MPI_Comm*);
2072	int MPI_Comm_spawn(char, char [], int, MPI_Info, int, MPI_Comm, MPI_Comm*, int []);
2073	int MPI_Comm_spawn_multiple(int, char* [], char** [], int [], MPI_Info [], int, MPI_Comm, MPI_Comm*, int []);
2074	int MPI_Lookup_name(char, MPI_Info, char);
2075	int MPI_Open_port(MPI_Info, char*);
2076	int MPI_Publish_name(char, MPI_Info, char);
2077	int MPI_Unpublish_name(char, MPI_Info, char);
2078	int MPI_Accumulate(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Op, MPI_Win);
2079	int MPI_Get(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
2080	int MPI_Put(void*, int, MPI_Datatype, int, MPI_Aint, int, MPI_Datatype, MPI_Win);
2081	int MPI_Win_complete(MPI_Win);
2082	int MPI_Win_create(void, MPI_Aint, int, MPI_Info, MPI_Comm, MPI_Win);
2083	int MPI_Win_fence(int, MPI_Win);
2084	int MPI_Win_free(MPI_Win*);
2085	int MPI_Win_get_group(MPI_Win, MPI_Group*);
2086	int MPI_Win_lock(int, int, int, MPI_Win);
2087	int MPI_Win_post(MPI_Group, int, MPI_Win);
2088	int MPI_Win_start(MPI_Group, int, MPI_Win);
2089	int MPI_Win_test(MPI_Win, int*);
2090	int MPI_Win_unlock(int, MPI_Win);
2091	int MPI_Win_wait(MPI_Win);
2092	int MPI_Alltoallw(void, int [], int [], MPI_Datatype [], void, int [], int [], MPI_Datatype [], MPI_Comm);
2093	int MPI_Exscan(void, void, int, MPI_Datatype, MPI_Op, MPI_Comm);
2094	int MPI_Add_error_class(int*);
2095	int MPI_Add_error_code(int, int*);
2096	int MPI_Add_error_string(int, char*);
2097	int MPI_Comm_call_errhandler(MPI_Comm, int);
2098	int MPI_Comm_create_keyval(MPI_Comm_copy_attr_function, MPI_Comm_delete_attr_function, int, void);
2099	int MPI_Comm_delete_attr(MPI_Comm, int);
2100	int MPI_Comm_free_keyval(int*);
2101	int MPI_Comm_get_attr(MPI_Comm, int, void, int);
2102	int MPI_Comm_get_name(MPI_Comm, char, int);
2103	int MPI_Comm_set_attr(MPI_Comm, int, void*);
2104	int MPI_Comm_set_name(MPI_Comm, char*);
2105	int MPI_File_call_errhandler(MPI_File, int);
2106	int MPI_Grequest_complete(MPI_Request);
2107	int MPI_Grequest_start(MPI_Grequest_query_function, MPI_Grequest_free_function, MPI_Grequest_cancel_function, void, MPI_Request*);
2108	int MPI_Init_thread(int, char*, int, int);
2109	int MPI_Is_thread_main(int*);
2110	int MPI_Query_thread(int*);
2111	int MPI_Status_set_cancelled(MPI_Status*, int);
2112	int MPI_Status_set_elements(MPI_Status*, MPI_Datatype, int);
2113	int MPI_Type_create_keyval(MPI_Type_copy_attr_function, MPI_Type_delete_attr_function, int, void);
2114	int MPI_Type_delete_attr(MPI_Datatype, int);
2115	int MPI_Type_dup(MPI_Datatype, MPI_Datatype*);
2116	int MPI_Type_free_keyval(int*);
2117	int MPI_Type_get_attr(MPI_Datatype, int, void, int);
2118	int MPI_Type_get_contents(MPI_Datatype, int, int, int, int [], MPI_Aint [], MPI_Datatype []);
2119	int MPI_Type_get_envelope(MPI_Datatype, int, int, int, int);
2120	int MPI_Type_get_name(MPI_Datatype, char, int);
2121	int MPI_Type_set_attr(MPI_Datatype, int, void*);
2122	int MPI_Type_set_name(MPI_Datatype, char*);
2123	int MPI_Type_match_size(int, int, MPI_Datatype*);
2124	int MPI_Win_call_errhandler(MPI_Win, int);
2125	int MPI_Win_create_keyval(MPI_Win_copy_attr_function, MPI_Win_delete_attr_function, int, void);
2126	int MPI_Win_delete_attr(MPI_Win, int);
2127	int MPI_Win_free_keyval(int*);
2128	int MPI_Win_get_attr(MPI_Win, int, void, int);
2129	int MPI_Win_get_name(MPI_Win, char, int);
2130	int MPI_Win_set_attr(MPI_Win, int, void*);
2131	int MPI_Win_set_name(MPI_Win, char*);
2132	MPI_Comm MPI_Comm_f2c(MPI_Fint);
2133	MPI_Datatype MPI_Type_f2c(MPI_Fint);
2134	MPI_File MPI_File_f2c(MPI_Fint);
2135	MPI_Fint MPI_Comm_c2f(MPI_Comm);
2136	MPI_Fint MPI_File_c2f(MPI_File);
2137	MPI_Fint MPI_Group_c2f(MPI_Group);
2138	MPI_Fint MPI_Info_c2f(MPI_Info);
2139	MPI_Fint MPI_Op_c2f(MPI_Op);
2140	MPI_Fint MPI_Request_c2f(MPI_Request);
2141	MPI_Fint MPI_Type_c2f(MPI_Datatype);
2142	MPI_Fint MPI_Win_c2f(MPI_Win);
2143	MPI_Group MPI_Group_f2c(MPI_Fint);
2144	MPI_Info MPI_Info_f2c(MPI_Fint);
2145	MPI_Op MPI_Op_f2c(MPI_Fint);
2146	MPI_Request MPI_Request_f2c(MPI_Fint);
2147	MPI_Win MPI_Win_f2c(MPI_Fint);
2148	int MPI_Alloc_mem(MPI_Aint, MPI_Info info, void* baseptr);
2149	int MPI_Comm_create_errhandler(MPI_Comm_errhandler_function, MPI_Errhandler);
2150	int MPI_Comm_get_errhandler(MPI_Comm, MPI_Errhandler*);
2151	int MPI_Comm_set_errhandler(MPI_Comm, MPI_Errhandler);
2152	int MPI_File_create_errhandler(MPI_File_errhandler_function, MPI_Errhandler);
2153	int MPI_File_get_errhandler(MPI_File, MPI_Errhandler*);
2154	int MPI_File_set_errhandler(MPI_File, MPI_Errhandler);
2155	int MPI_Finalized(int*);
2156	int MPI_Free_mem(void*);
2157	int MPI_Get_address(void, MPI_Aint);
2158	int MPI_Info_create(MPI_Info*);
2159	int MPI_Info_delete(MPI_Info, char*);
2160	int MPI_Info_dup(MPI_Info, MPI_Info*);
2161	int MPI_Info_free(MPI_Info* info);
2162	int MPI_Info_get(MPI_Info, char, int, char, int*);
2163	int MPI_Info_get_nkeys(MPI_Info, int*);
2164	int MPI_Info_get_nthkey(MPI_Info, int, char*);
2165	int MPI_Info_get_valuelen(MPI_Info, char, int, int*);
2166	int MPI_Info_set(MPI_Info, char, char);
2167	int MPI_Pack_external(char, void, int, MPI_Datatype, void, MPI_Aint, MPI_Aint);
2168	int MPI_Pack_external_size(char, int, MPI_Datatype, MPI_Aint);
2169	int MPI_Request_get_status(MPI_Request, int, MPI_Status);
2170	int MPI_Status_c2f(MPI_Status, MPI_Fint);
2171	int MPI_Status_f2c(MPI_Fint, MPI_Status);
2172	int MPI_Type_create_darray(int, int, int, int [], int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
2173	int MPI_Type_create_hindexed(int, int [], MPI_Aint [], MPI_Datatype, MPI_Datatype*);
2174	int MPI_Type_create_hvector(int, int, MPI_Aint, MPI_Datatype, MPI_Datatype*);
2175	int MPI_Type_create_indexed_block(int, int, int [], MPI_Datatype, MPI_Datatype*);
2176	int MPIX_Type_create_hindexed_block(int, int, MPI_Aint [], MPI_Datatype, MPI_Datatype*);
2177	int MPI_Type_create_resized(MPI_Datatype, MPI_Aint, MPI_Aint, MPI_Datatype*);
2178	int MPI_Type_create_struct(int, int [], MPI_Aint [], MPI_Datatype [], MPI_Datatype*);
2179	int MPI_Type_create_subarray(int, int [], int [], int [], int, MPI_Datatype, MPI_Datatype*);
2180	int MPI_Type_get_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
2181	int MPI_Type_get_true_extent(MPI_Datatype, MPI_Aint, MPI_Aint);
2182	int MPI_Unpack_external(char, void, MPI_Aint, MPI_Aint, void, int, MPI_Datatype);
2183	int MPI_Win_create_errhandler(MPI_Win_errhandler_function, MPI_Errhandler);
2184	int MPI_Win_get_errhandler(MPI_Win, MPI_Errhandler*);
2185	int MPI_Win_set_errhandler(MPI_Win, MPI_Errhandler);
2186	int MPI_Type_create_f90_integer(int, MPI_Datatype*);
2187	int MPI_Type_create_f90_real(int, int, MPI_Datatype*);
2188	int MPI_Type_create_f90_complex(int, int, MPI_Datatype*);
2189	int MPI_Reduce_local(void* inbuf, void* inoutbuf, int count, MPI_Datatype datatype, MPI_Op op);
2190	int MPI_Op_commutative(MPI_Op op, int* commute);
2191	int MPI_Reduce_scatter_block(void* sendbuf, void* recvbuf, int recvcount, MPI_Datatype datatype, MPI_Op op, MPI_Comm comm);
2192	int MPI_Dist_graph_create_adjacent(MPI_Comm comm_old, int indegree, int [], int [], int outdegree, int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
2193	int MPI_Dist_graph_create(MPI_Comm comm_old, int n, int [], int [], int [], int [], MPI_Info info, int reorder, MPI_Comm* comm_dist_graph);
2194	int MPI_Dist_graph_neighbors_count(MPI_Comm comm, int* indegree, int* outdegree, int* weighted);
2195	int MPI_Dist_graph_neighbors(MPI_Comm comm, int maxindegree, int [], int [], int maxoutdegree, int [], int []);
2196	const extern int* MPI_UNWEIGHTED;
2197	extern MPI_Fint* MPI_F_STATUS_IGNORE;
2198	extern MPI_Fint* MPI_F_STATUSES_IGNORE;
2199	const extern struct MPIR_T_pvar_handle* MPI_T_PVAR_ALL_HANDLES;
2200	//====================== civl-mpi.cvh ======================
2201	int sizeofDatatype(MPI_Datatype);
2202	$abstract double $mpi_time(int i);
2203	$mpi_gcomm $mpi_gcomm_create($scope, int);
2204	void $mpi_gcomm_destroy($mpi_gcomm);
2205	MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
2206	void $mpi_comm_destroy(MPI_Comm, $mpi_state);
2207	int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
2208	int $mpi_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status);
2209	int $mpi_sendrecv(void* sendbuf, int sendcount, MPI_Datatype sendtype, int dest, int sendtag, void* recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status* status);
2210	int $mpi_collective_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
2211	int $mpi_collective_recv(void, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status, char*);
2212	int $mpi_bcast(void, int, MPI_Datatype, int, int, MPI_Comm, char);
2213	int $mpi_reduce(void, void, int, MPI_Datatype, MPI_Op, int, int, MPI_Comm, char*);
2214	int $mpi_gather(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
2215	int $mpi_gatherv(void, int, MPI_Datatype, void, int [], int [], MPI_Datatype, int, int, MPI_Comm, char*);
2216	int $mpi_scatter(void, int, MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
2217	int $mpi_scatterv(void, int [], int [], MPI_Datatype, void, int, MPI_Datatype, int, int, MPI_Comm, char*);
2218	void* $mpi_pointer_add(void*, int, MPI_Datatype);
2219	$system[mpi] int $mpi_new_gcomm($scope, $mpi_gcomm);
2220	$system[mpi] $mpi_gcomm $mpi_get_gcomm($scope, int);
2221	int $mpi_comm_dup($scope, MPI_Comm, MPI_Comm, char);
2222	int $mpi_comm_free(MPI_Comm*, $mpi_state);
2223	$system[mpi] $scope $mpi_root_scope($comm);
2224	$system[mpi] $scope $mpi_proc_scope($comm);
2225	$system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
2226	$bundle $mpi_create_coroutine_entry(int routineTag, int root, int op, int numDatatypes, int* datatypes);
2227	void $mpi_diff_coroutine_entries($bundle specEntry, $bundle mineEntry, int rank);
2228	void $mpi_coassert(MPI_Comm, _Bool);
2229	_Bool $mpi_isRecvBufEmpty(int x);
2230	/*@ depends_on \nothing;
2231	@*/
2232	$system[mpi] void $mpi_p2pSendShot(int commID, $message msg, int place);
2233	/*@ depends_on \nothing;
2234	@*/
2235	$system[mpi] void $mpi_colSendShot(int commID, $message msg, int place);
2236	/*@ depends_on \nothing;
2237	@*/
2238	$system[mpi] void $mpi_p2pRecvShot(int commID, int source, int dest, int tag);
2239	/*@ depends_on \nothing;
2240	@*/
2241	$system[mpi] void $mpi_colRecvShot(int commID, int source, int dest, int tag);
2242	//======================== string.h ========================
2243	void* memcpy(void* p, void* q, size_t size);
2244	void* memmove(void* dest, void* src, size_t n);
2245	$system[string] void* memset(void* s, int c, size_t n);
2246	int memcmp(void* s1, void* s2, size_t n);
2247	void* memchr(void* s, int c, size_t n);
2248	$system[string] char* strcpy(char* restrict s1, char* restrict s2);
2249	char* strncpy(char* dest, char* src, size_t n);
2250	char* strcat(char* dest, char* src);
2251	char* strncat(char* dest, char* src, size_t n);
2252	$system[string] int strcmp(char* s1, char* s2);
2253	int strncmp(char* s1, char* s2, size_t n);
2254	int strcoll(char* s1, char* s2);
2255	size_t strxfrm(char* dest, char* src, size_t n);
2256	char* strchr(char* s, int c);
2257	char* strrchr(char* s, int c);
2258	size_t strcspn(char* s, char* reject);
2259	size_t strspn(char* s, char* accept);
2260	char* strpbrk(char* s, char* accept);
2261	char* strstr(char* s1, char* s2);
2262	char* strtok(char* s, char* delim);
2263	$system[string] size_t strlen(char* s);
2264	char* strerror(int errnum);
2265	//======================= pointer.cvh ======================
2266	/*@ depends_on \write(obj);
2267	@ executes_when $true;
2268	@*/
2269	$system[pointer] void $set_default(void* obj);
2270	/*@ depends_on \write(obj1, obj2, result);
2271	@ executes_when $true;
2272	@*/
2273	$system[pointer] void $apply(void* obj1, $operation op, void* obj2, void* result);
2274	/*@ depends_on \write(x, y);
2275	@ executes_when $true;
2276	@*/
2277	$system[pointer] _Bool $equals(void* x, void* y);
2278	/*@ depends_on \write(x, y);
2279	@ executes_when $true;
2280	@*/
2281	$system[pointer] void $assert_equals(void* x, void* y, ...);
2282	/*@ depends_on \write(obj1, obj2);
2283	@ executes_when $true;
2284	@*/
2285	$system[pointer] _Bool $contains(void* obj1, void* obj2);
2286	/*@ depends_on \nothing;
2287	@ executes_when $true;
2288	@*/
2289	$system[pointer] void* $translate_ptr(void* ptr, void* obj);
2290	/*@ depends_on \write(ptr, value);
2291	@ executes_when $true;
2292	@*/
2293	$system[pointer] void $copy(void* ptr, void* value);
2294	/*@ depends_on \write(array);
2295	@ executes_when $true;
2296	@*/
2297	$system[pointer] void $leaf_node_ptrs(void* array, void* obj);
2298	/*@ depends_on \nothing;
2299	@ executes_when $true;
2300	@*/
2301	$system[pointer] _Bool $is_identity_ref(void* obj);
2302	/*@ depends_on \write(obj);
2303	@ executes_when $true;
2304	@*/
2305	$system[pointer] void $set_leaf_nodes(void* obj, int value);
2306	/*@ depends_on \write(obj);
2307	@ executes_when $true;
2308	@*/
2309	$system[pointer] _Bool $leaf_nodes_equal_to(void* obj, int value);
2310	/*@ depends_on \write(obj);
2311	@ executes_when $true;
2312	@*/
2313	$system[pointer] _Bool $has_leaf_node_equal_to(void* obj, int value);
2314	/*@ depends_on \nothing;
2315	@ executes_when $true;
2316	@*/
2317	$system[pointer] _Bool $is_derefable_pointer(void* ptr);
2318	/*@ depends_on \nothing;
2319	@ executes_when $true;
2320	@*/
2321	$system[pointer] void* $pointer_add(void* ptr, int offset, int type_size);
2322	//========================= seq.cvh ========================
2323	/*@ depends_on \write(array);
2324	@ executes_when $true;
2325	@*/
2326	$system[seq] int $seq_length(void* array);
2327	/*@ depends_on \write(array, value);
2328	@ executes_when $true;
2329	@*/
2330	$system[seq] void $seq_init(void* array, int count, void* value);
2331	/*@ depends_on \write(array, values);
2332	@ executes_when $true;
2333	@*/
2334	$system[seq] void $seq_insert(void* array, int index, void* values, int count);
2335	/*@ depends_on \write(array, values);
2336	@ executes_when $true;
2337	@*/
2338	$system[seq] void $seq_remove(void* array, int index, void* values, int count);
2339	/*@ depends_on \write(array, values);
2340	@*/
2341	$atomic_f void $seq_append(void* array, void* values, int count);
2342	//====================== civl-mpi.cvl ======================
2343	char* getCoroutineName(int tag);
2344	struct $mpi_gcomm{
2345	$gcomm p2p;
2346	$gcomm col;
2347	$gcollator gcollator;
2348	$gbarrier gbarrier;
2349	};
2350	int sizeofDatatype(MPI_Datatype datatype)
2351	{
2352	switch (datatype)
2353	{
2354	case MPI_INT:
2355	return sizeof(int);
2356	case MPI_2INT:
2357	return sizeof(int) * 2;
2358	case MPI_FLOAT:
2359	return sizeof(float);
2360	case MPI_DOUBLE:
2361	return sizeof(double);
2362	case MPI_CHAR:
2363	return sizeof(char);
2364	case MPI_BYTE:
2365	return sizeof(char);
2366	case MPI_SHORT:
2367	return sizeof(short);
2368	case MPI_LONG:
2369	return sizeof(long);
2370	case MPI_LONG_DOUBLE:
2371	return sizeof(long double);
2372	case MPI_LONG_LONG_INT:
2373	return sizeof(long long);
2374	case MPI_LONG_LONG:
2375	return sizeof(long long);
2376	case MPI_UNSIGNED_LONG_LONG:
2377	return sizeof(unsigned long long);
2378	default:
2379	$assert(0, "Unreachable");
2380	}
2381	}
2382	$mpi_gcomm $mpi_gcomm_create($scope scope, int size)
2383	{
2384	$mpi_gcomm result;
2385	result.p2p = $gcomm_create(scope, size);
2386	result.col = $gcomm_create(scope, size);
2387	result.gcollator = $gcollator_create(scope);
2388	result.gbarrier = $gbarrier_create(scope, size);
2389	return result;
2390	}
2391	void $mpi_gcomm_destroy($mpi_gcomm gc)
2392	{
2393	int numJunkRecord;
2394	int numJunkMsg;
2395	$message junkMsgs[];
2396	$seq_init(&(junkMsgs), 0, (void*)0);
2397	numJunkMsg = $gcomm_destroy(gc.p2p, &(junkMsgs));
2398	for (int i = 0; i < numJunkMsg; i++)
2399	{
2400	int src;
2401	int dest;
2402	int tag;
2403	src = $message_source(junkMsgs[i]);
2404	dest = $message_dest(junkMsgs[i]);
2405	tag = $message_tag(junkMsgs[i]);
2406	$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);
2407	}
2408	numJunkMsg = $gcomm_destroy(gc.col, &(junkMsgs));
2409	for (int i = 0; i < numJunkMsg; i++)
2410	{
2411	int src;
2412	int tag;
2413	char* routine;
2414	src = $message_source(junkMsgs[i]);
2415	tag = $message_tag(junkMsgs[i]);
2416	routine = getCoroutineName(tag);
2417	$assert($false, "MPI message leak: There is a message sent by rank %d for collective routine %s that is never received.", src, routine);
2418	}
2419	numJunkRecord = $gcollator_destroy(gc.gcollator);
2420	$gbarrier_destroy(gc.gbarrier);
2421	$assert(numJunkRecord == 0, "MPI collective routines are called inappropriately because there are %d collective records still remaining the collective routine checker.", numJunkRecord);
2422	}
2423	MPI_Comm $mpi_comm_create($scope scope, $mpi_gcomm gc, int rank)
2424	{
2425	MPI_Comm result;
2426	result.p2p = $comm_create(scope, gc.p2p, rank);
2427	result.col = $comm_create(scope, gc.col, rank);
2428	result.collator = $collator_create(scope, gc.gcollator);
2429	result.barrier = $barrier_create(scope, gc.gbarrier, rank);
2430	result.gcommIndex = 0;
2431	return result;
2432	}
2433	void $mpi_comm_destroy(MPI_Comm comm, $mpi_state mpi_state)
2434	{
2435	if (comm.gcommIndex == 0)
2436	$assert(mpi_state == _MPI_FINALIZED, "Process terminates without calling MPI_Finalize() first.");
2437	$comm_destroy(comm.p2p);
2438	$comm_destroy(comm.col);
2439	$collator_destroy(comm.collator);
2440	$barrier_destroy(comm.barrier);
2441	}
2442	void* $mpi_pointer_add(void* ptr, int offset, MPI_Datatype datatype)
2443	{
2444	int type_size = sizeofDatatype(datatype);
2445	return $pointer_add(ptr, offset, type_size);
2446	}
2447	int $mpi_send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm)
2448	{
2449	if (dest >= 0)
2450	{
2451	int size = count * sizeofDatatype(datatype);
2452	int place = $comm_place(comm.p2p);
2453	$message out = $message_pack(place, dest, tag, buf, size);
2454	$comm_enqueue(comm.p2p, out);
2455	}
2456	return 0;
2457	}
2458	int $mpi_recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status)
2459	{
2460	if ((source >= 0) \|\| (source == (-1)))
2461	{
2462	$message in;
2463	int place = $comm_place(comm.p2p);
2464	int deterministicTag;
2465	$assert((tag == (-2)) \|\| (tag >= 0), "Illegal MPI message receive tag %d.\n", tag);
2466	deterministicTag = tag < 0 ? -2 : tag;
2467	$elaborate(source);
2468	in = $comm_dequeue(comm.p2p, source, deterministicTag);
2469	int size = count * sizeofDatatype(datatype);
2470	$message_unpack(in, buf, size);
2471	if (status != (void*)0)
2472	{
2473	(status)->size = $message_size(in);
2474	(status)->MPI_SOURCE = $message_source(in);
2475	(status)->MPI_TAG = $message_tag(in);
2476	(status)->MPI_ERROR = 0;
2477	}
2478	}
2479	return 0;
2480	}
2481	int $mpi_sendrecv(void* sendbuf, int sendcount, MPI_Datatype sendtype, int dest, int sendtag, void* recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status* status)
2482	{
2483	int deterministicRecvTag;
2484	$assert(sendtag >= 0, "MPI sendtag should be greater than or equal to zero");
2485	$assert((recvtag == (-2)) \|\| (recvtag >= 0), "Illegal MPI message receive tag %d.\n", recvtag);
2486	deterministicRecvTag = recvtag < 0 ? -2 : recvtag;
2487	if ((dest >= 0) && ((source >= 0) \|\| (source == (-1))))
2488	{
2489	$message out;
2490	$message in;
2491	int size = sendcount * sizeofDatatype(sendtype);
2492	int place = $comm_place(comm.p2p);
2493	out = $message_pack(place, dest, sendtag, sendbuf, size);
2494	$elaborate(source);
2495	$choose{
2496	$when ($true)
2497	{
2498	$atomic
2499	{
2500	$comm_enqueue(comm.p2p, out);
2501	}
2502	$atomic
2503	{
2504	in = $comm_dequeue(comm.p2p, source, deterministicRecvTag);
2505	}
2506	}
2507	$when ($false)
2508	{
2509	in = $comm_dequeue(comm.p2p, source, deterministicRecvTag);
2510	$comm_enqueue(comm.p2p, out);
2511	}
2512	}
2513	size = recvcount * sizeofDatatype(recvtype);
2514	$message_unpack(in, recvbuf, size);
2515	if (status != (void*)0)
2516	{
2517	(status)->size = $message_size(in);
2518	(status)->MPI_SOURCE = $message_source(in);
2519	(status)->MPI_TAG = $message_tag(in);
2520	(status)->MPI_ERROR = 0;
2521	}
2522	}
2523	else
2524	if (dest >= 0)
2525	{
2526	$mpi_send(sendbuf, sendcount, sendtype, dest, sendtag, comm);
2527	}
2528	else
2529	if ((source >= 0) \|\| (source == (-1)))
2530	{
2531	$mpi_recv(recvbuf, recvcount, recvtype, source, deterministicRecvTag, comm, status);
2532	}
2533	return 0;
2534	}
2535	int $mpi_collective_send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm)
2536	{
2537	if (dest >= 0)
2538	{
2539	int size = count * sizeofDatatype(datatype);
2540	int place = $comm_place(comm.col);
2541	$message out = $message_pack(place, dest, tag, buf, size);
2542	$comm_enqueue(comm.col, out);
2543	}
2544	return 0;
2545	}
2546	int $mpi_collective_recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status, char* routName)
2547	{
2548	if ((source >= 0) \|\| (source == (-1)))
2549	{
2550	$elaborate(source);
2551	$message in = $comm_dequeue(comm.col, source, -2);
2552	int size = count * sizeofDatatype(datatype);
2553	int recvTag;
2554	recvTag = $message_tag(in);
2555	$assert(recvTag == tag, "Collective routine %s receives a message with a mismatched tag\n", routName);
2556	$message_unpack(in, buf, size);
2557	if (status != (void*)0)
2558	{
2559	(status)->size = $message_size(in);
2560	(status)->MPI_SOURCE = $message_source(in);
2561	(status)->MPI_TAG = recvTag;
2562	(status)->MPI_ERROR = 0;
2563	}
2564	}
2565	return 0;
2566	}
2567	int $mpi_bcast(void* buf, int count, MPI_Datatype datatype, int root, int tag, MPI_Comm comm, char* routName)
2568	{
2569	if ($comm_place(comm.col) == root)
2570	{
2571	int nprocs = $comm_size(comm.col);
2572	for (int i = 0; i < nprocs; i++)
2573	if (i != root)
2574	$mpi_collective_send(buf, count, datatype, i, tag, comm);
2575	}
2576	else
2577	$mpi_collective_recv(buf, count, datatype, root, tag, comm, (void*)0, routName);
2578	return 0;
2579	}
2580	int $mpi_reduce(void* sendbuf, void* recvbuf, int count, MPI_Datatype datatype, MPI_Op op, int root, int tag, MPI_Comm comm, char* routName)
2581	{
2582	int rank;
2583	rank = $comm_place(comm.col);
2584	if (rank != root)
2585	$mpi_collective_send(sendbuf, count, datatype, root, tag, comm);
2586	else
2587	{
2588	int nprocs = $comm_size(comm.col);
2589	int size;
2590	size = count * sizeofDatatype(datatype);
2591	memcpy(recvbuf, sendbuf, size);
2592	for (int i = 0; i < nprocs; i++)
2593	{
2594	if (i != root)
2595	{
2596	int colTag;
2597	$message in = $comm_dequeue(comm.col, i, -2);
2598	colTag = $message_tag(in);
2599	$assert(colTag == tag, "Collective routine %s receives a message with a mismatched tag\n", routName);
2600	$bundle_unpack_apply(in.data, recvbuf, count, op);
2601	$assert(in.size <= size, "Message of size %d exceeds the specified size %d.", in.size, size);
2602	}
2603	}
2604	}
2605	return 0;
2606	}
2607	int $mpi_gather(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, int tag, MPI_Comm comm, char* routName)
2608	{
2609	int rank;
2610	int nprocs;
2611	MPI_Status status;
2612	rank = $comm_place(comm.col);
2613	nprocs = $comm_size(comm.col);
2614	if (rank == root)
2615	$assert(sendtype == recvtype, "%s asks for equality between \'sendtype\' and \'recvtype\'.", routName);
2616	if (sendbuf == (void*)(-1))
2617	{
2618	$assert(root == rank, "Only root can replace 'sendbuf' with 'MPI_IN_PLACE'.");
2619	}
2620	else
2621	if (root == rank)
2622	{
2623	void* ptr;
2624	$assert(sendcount == recvcount, "Root process of routine %d without using MPI_IN_PLACE should give the same value for recvcount and sendcount", routName);
2625	ptr = $mpi_pointer_add(recvbuf, root * recvcount, recvtype);
2626	memcpy(ptr, sendbuf, recvcount * sizeofDatatype(recvtype));
2627	}
2628	else
2629	$mpi_collective_send(sendbuf, sendcount, sendtype, root, tag, comm);
2630	if (rank == root)
2631	{
2632	int real_recvcount;
2633	int offset;
2634	for (int i = 0; i < nprocs; i++)
2635	{
2636	if (i != root)
2637	{
2638	void* ptr;
2639	offset = i * recvcount;
2640	ptr = $mpi_pointer_add(recvbuf, offset, recvtype);
2641	$mpi_collective_recv(ptr, recvcount, recvtype, i, tag, comm, &(status), routName);
2642	real_recvcount = status.size / sizeofDatatype(recvtype);
2643	$assert(real_recvcount == recvcount, "%s asks for equality between the amount of data sent and the amount of data received.", routName);
2644	}
2645	}
2646	}
2647	return 0;
2648	}
2649	int $mpi_gatherv(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcounts[], int displs[], MPI_Datatype recvtype, int root, int tag, MPI_Comm comm, char* routName)
2650	{
2651	int rank;
2652	int nprocs;
2653	rank = $comm_place(comm.col);
2654	nprocs = $comm_size(comm.col);
2655	if (rank == root)
2656	$assert(sendtype == recvtype, "%s asks for equality between \'sendtype\' and \'recvtype\'.", routName);
2657	if (sendbuf == (void*)(-1))
2658	{
2659	$assert(root == rank, "Only root can replace 'sendbuf' with 'MPI_IN_PLACE'.");
2660	}
2661	else
2662	if (root == rank)
2663	{
2664	void* ptr;
2665	$assert(sendcount == (recvcounts[root]), "For routine %s, recvcounts[%d] should be same as the sendcount of the process with rank %d.\n", routName, root, root);
2666	ptr = $mpi_pointer_add(recvbuf, displs[rank], recvtype);
2667	memcpy(ptr, sendbuf, sendcount * sizeofDatatype(recvtype));
2668	}
2669	else
2670	{
2671	$mpi_collective_send(sendbuf, sendcount, sendtype, root, tag, comm);
2672	}
2673	if (rank == root)
2674	{
2675	int real_recvcount;
2676	MPI_Status status;
2677	for (int i = 0; i < nprocs; i++)
2678	{
2679	if (i != root)
2680	{
2681	void* ptr = $mpi_pointer_add(recvbuf, displs[i], recvtype);
2682	$mpi_collective_recv(ptr, recvcounts[i], recvtype, i, tag, comm, &(status), routName);
2683	real_recvcount = status.size / sizeofDatatype(recvtype);
2684	$assert(real_recvcount == (recvcounts[i]), "%s asks for equality between the amount of data sent and the amount of data received.", routName);
2685	}
2686	}
2687	}
2688	return 0;
2689	}
2690	int $mpi_scatter(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, int tag, MPI_Comm comm, char* routName)
2691	{
2692	int rank;
2693	int nprocs;
2694	rank = $comm_place(comm.col);
2695	nprocs = $comm_size(comm.col);
2696	if (rank == root)
2697	$assert(sendtype == recvtype, "MPI_Scatter() asks for equality between \'sendtype\' and \'recvtype\'.");
2698	if (recvbuf == (void*)(-1))
2699	{
2700	$assert(root == rank, "Only root can replace 'recvbuf' with 'MPI_IN_PLACE'.");
2701	}
2702	else
2703	if (rank == root)
2704	{
2705	void* ptr;
2706	$assert(sendcount == recvcount, "Root process of routine %d without using MPI_IN_PLACE should give the same value for recvcount and sendcount", routName);
2707	ptr = $mpi_pointer_add(sendbuf, root * recvcount, sendtype);
2708	memcpy(recvbuf, ptr, sizeofDatatype(recvtype) * recvcount);
2709	}
2710	if (rank == root)
2711	{
2712	int offset;
2713	for (int i = 0; i < nprocs; i++)
2714	{
2715	if (i != root)
2716	{
2717	void* ptr;
2718	offset = i * sendcount;
2719	ptr = $mpi_pointer_add(sendbuf, offset, sendtype);
2720	$mpi_collective_send(ptr, sendcount, sendtype, i, tag, comm);
2721	}
2722	}
2723	}
2724	if (!(root == rank))
2725	{
2726	int real_recvcount;
2727	MPI_Status status;
2728	$mpi_collective_recv(recvbuf, recvcount, recvtype, root, tag, comm, &(status), routName);
2729	real_recvcount = status.size / sizeofDatatype(recvtype);
2730	$assert(real_recvcount == recvcount, "%s asks for equality between the amount of data sent and the amount of data received.", routName);
2731	}
2732	return 0;
2733	}
2734	int $mpi_scatterv(void* sendbuf, int sendcounts[], int displs[], MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, int tag, MPI_Comm comm, char* routName)
2735	{
2736	int rank;
2737	int nprocs;
2738	rank = $comm_place(comm.col);
2739	nprocs = $comm_size(comm.col);
2740	if (rank == root)
2741	$assert(sendtype == recvtype, "%s asks for equality between \'sendtype\' and \'recvtype\'.", routName);
2742	if (recvbuf == (void*)(-1))
2743	{
2744	$assert(root == rank, "Only root can replace 'recvbuf' with 'MPI_IN_PLACE'.");
2745	}
2746	else
2747	if (rank == root)
2748	{
2749	void* ptr;
2750	$assert((sendcounts[root]) == recvcount, "For routine %s, sendcounts[%d] should be same as the recvcount of the process with rank %d.\n", routName, root, root);
2751	ptr = $mpi_pointer_add(sendbuf, displs[root], sendtype);
2752	memcpy(recvbuf, ptr, recvcount * sizeofDatatype(recvtype));
2753	}
2754	if (rank == root)
2755	{
2756	for (int i = 0; i < nprocs; i++)
2757	{
2758	if (i != root)
2759	{
2760	void* ptr = $mpi_pointer_add(sendbuf, displs[i], sendtype);
2761	$mpi_collective_send(ptr, sendcounts[i], sendtype, i, tag, comm);
2762	}
2763	}
2764	}
2765	if (!(root == rank))
2766	{
2767	MPI_Status status;
2768	int real_recvcount;
2769	$mpi_collective_recv(recvbuf, recvcount, recvtype, root, tag, comm, &(status), routName);
2770	real_recvcount = status.size / sizeofDatatype(recvtype);
2771	$assert(real_recvcount == recvcount, "Process rank:%d\n%s asks for equality between the amount of data sent (%d) and the amount of data received (%d).", rank, routName, real_recvcount, recvcount);
2772	}
2773	return 0;
2774	}
2775	int $mpi_comm_dup($scope scope, MPI_Comm comm, MPI_Comm* newcomm, char* routName)
2776	{
2777	int place = $comm_place(comm.col);
2778	$mpi_gcomm newgcomm;
2779	int idx;
2780	$scope CMPI_ROOT_SCOPE = $mpi_root_scope(comm.col);
2781	if (place == 0)
2782	{
2783	int size = $comm_size(comm.col);
2784	newgcomm = $mpi_gcomm_create(CMPI_ROOT_SCOPE, size);
2785	idx = $mpi_new_gcomm(CMPI_ROOT_SCOPE, newgcomm);
2786	}
2787	$mpi_bcast(&(idx), 1, MPI_INT, 0, 9986, comm, routName);
2788	newgcomm = $mpi_get_gcomm(CMPI_ROOT_SCOPE, idx);
2789	*newcomm = $mpi_comm_create(scope, newgcomm, place);
2790	(newcomm)->gcommIndex = idx;
2791	$barrier_call(comm.barrier);
2792	$gcomm_dup(comm.p2p, (newcomm)->p2p);
2793	$gcomm_dup(comm.col, (newcomm)->col);
2794	$barrier_call(comm.barrier);
2795	return 0;
2796	}
2797	int $mpi_comm_free(MPI_Comm* comm, $mpi_state mpi_state)
2798	{
2799	int place = $comm_place((comm)->col);
2800	int size = $comm_size((comm)->col);
2801	int buf[size];
2802	int gcommIndex = (comm)->gcommIndex;
2803	$scope CMPI_ROOT_SCOPE = $mpi_root_scope((comm)->col);
2804	$mpi_gather(&(place), 1, MPI_INT, buf, 1, MPI_INT, 0, 9985, *comm, "MPI_Comm_free synchronization.");
2805	$mpi_comm_destroy(*comm, mpi_state);
2806	if (place == 0)
2807	{
2808	$mpi_gcomm temp = $mpi_get_gcomm(CMPI_ROOT_SCOPE, gcommIndex);
2809	$mpi_gcomm_destroy(temp);
2810	}
2811	return 0;
2812	}
2813	$bundle $mpi_create_coroutine_entry(int routineTag, int root, int op, int numDatatypes, int* datatypes)
2814	{
2815	int zero = 0;
2816	$bundle bundledEntry;
2817	struct Entry{
2818	int routine_tag;
2819	int root;
2820	int op;
2821	int numTypes;
2822	int datatypes[];
2823	} entry;
2824	entry.routine_tag = routineTag;
2825	entry.root = root;
2826	entry.op = op;
2827	entry.numTypes = numDatatypes;
2828	$seq_init(&(entry.datatypes), numDatatypes, &(zero));
2829	for (int i = 0; i < numDatatypes; i++)
2830	entry.datatypes[i] = datatypes[i];
2831	bundledEntry = $bundle_pack(&(entry), sizeof(struct Entry));
2832	return bundledEntry;
2833	}
2834	void $mpi_diff_coroutine_entries($bundle specEntry, $bundle mineEntry, int rank)
2835	{
2836	struct Entry{
2837	int routine_tag;
2838	int root;
2839	int op;
2840	int numTypes;
2841	int datatypes[];
2842	} spec;
2843	struct Entry mine;
2844	char* routine;
2845	int numTypes;
2846	$bundle_unpack(specEntry, &(spec));
2847	$bundle_unpack(mineEntry, &(mine));
2848	routine = getCoroutineName(spec.routine_tag);
2849	if (spec.routine_tag != mine.routine_tag)
2850	{
2851	char* mineRoutine = getCoroutineName(mine.routine_tag);
2852	$assert($false, "Process with rank %d reaches an MPI collective routine %s while at least one of others are collectively reaching %s.", rank, mineRoutine, routine);
2853	}
2854	else
2855	if (spec.root != mine.root)
2856	{
2857	$assert($false, "Process with rank %d reaches an MPI collective routine %s which has a different root with at least one of others.", rank, routine);
2858	}
2859	else
2860	if (spec.op != mine.op)
2861	{
2862	$assert($false, "Process with rank %d reaches an MPI collective routine %s which has a different MPI_Op with at least one of others", rank, routine);
2863	}
2864	else
2865	if (spec.numTypes != mine.numTypes)
2866	{
2867	$assert($false, "Process with rank %d reaches an MPI collective routine %s which has an inconsistent datatype specification with at least one of others", rank, routine);
2868	}
2869	numTypes = spec.numTypes;
2870	for (int i = 0; i < numTypes; i++)
2871	if ((spec.datatypes[i]) != (mine.datatypes[i]))
2872	{
2873	$assert($false, "Process with rank %d reaches an MPI collective routine %s which has an inconsistent datatype specification with at least one of others", rank, routine);
2874	break;
2875	}
2876	}
2877	char* getCoroutineName(int tag)
2878	{
2879	switch (tag)
2880	{
2881	case 9999:
2882	return "MPI_Bcast";
2883	case 9998:
2884	return "MPI_Reduce";
2885	case 9997:
2886	return "MPI_Allreduce";
2887	case 9996:
2888	return "MPI_Gather";
2889	case 9995:
2890	return "MPI_Scatter";
2891	case 9994:
2892	return "MPI_Gatherv";
2893	case 9993:
2894	return "MPI_Scatterv";
2895	case 9992:
2896	return "MPI_Allgather";
2897	case 9991:
2898	return "MPI_Reduce_scatter";
2899	case 9990:
2900	return "MPI_Alltoall";
2901	case 9989:
2902	return "MPI_Alltoallv";
2903	case 9988:
2904	return "MPI_Alltoallw";
2905	case 9987:
2906	return "MPI_Barrier";
2907	case 9986:
2908	return "MPI_Commdup";
2909	case 9985:
2910	return "MPI_Commfree";
2911	default:
2912	$assert($false, "Internal Error: Unexpected MPI routine tag:%d.\n", tag);
2913	}
2914	}
2915	//======================== civlc.cvh =======================
2916	$system[civlc] void $wait($proc p);
2917	$system[civlc] void $waitall($proc* procs, int numProcs);
2918	/*@ depends_on \nothing;
2919	@ executes_when $true;
2920	@*/
2921	$system[civlc] void $exit(void);
2922	/*@ depends_on \nothing;
2923	@ executes_when $true;
2924	@*/
2925	$system[civlc] int $choose_int(int n);
2926	/*@ depends_on \nothing;
2927	@ executes_when $true;
2928	@*/
2929	$system[civlc] void $assert(_Bool expr, ...);
2930	/*@ depends_on \nothing;
2931	@ executes_when $true;
2932	@*/
2933	$system[civlc] void $assume(_Bool expr);
2934	/*@ pure;
2935	@ depends_on \nothing;
2936	@ executes_when $true;
2937	@*/
2938	$system[civlc] void $elaborate(int x);
2939	/*@ depends_on \nothing;
2940	@ executes_when $true;
2941	@*/
2942	$system[civlc] int $next_time_count(void);
2943	/*@ pure;
2944	@ depends_on \nothing;
2945	@ executes_when $true;
2946	@*/
2947	$system[civlc] void $pathCondition(void);
2948	/*@ pure;
2949	@ depends_on \nothing;
2950	@ executes_when $true;
2951	@*/
2952	$system[civlc] _Bool $is_concrete_int(int value);
2953	/*@ depends_on \nothing;
2954	@ executes_when $true;
2955	@*/
2956	$system[civlc] void* $malloc($scope s, int size);
2957	/*@ depends_on \write(p);
2958	@ executes_when $true;
2959	@*/
2960	$system[civlc] void $free(void* p);
2961	/*@ depends_on \write(ptr);
2962	@ executes_when $true;
2963	@*/
2964	$system[civlc] void $havoc(void* ptr);
2965	/*@ pure;
2966	@ depends_on \nothing;
2967	@ executes_when $true;
2968	@*/
2969	$system[civlc] double $pow(double base, double exp);
2970	//======================== civlc.cvl =======================
2971	struct $int_iter{
2972	int size;
2973	int content[];
2974	int index;
2975	};
2976	//======================== civlc.cvh =======================
2977	$system[civlc] void $wait($proc p);
2978	$system[civlc] void $waitall($proc* procs, int numProcs);
2979	/*@ depends_on \nothing;
2980	@ executes_when $true;
2981	@*/
2982	$system[civlc] void $exit(void);
2983	/*@ depends_on \nothing;
2984	@ executes_when $true;
2985	@*/
2986	$system[civlc] int $choose_int(int n);
2987	/*@ depends_on \nothing;
2988	@ executes_when $true;
2989	@*/
2990	$system[civlc] void $assert(_Bool expr, ...);
2991	/*@ depends_on \nothing;
2992	@ executes_when $true;
2993	@*/
2994	$system[civlc] void $assume(_Bool expr);
2995	/*@ pure;
2996	@ depends_on \nothing;
2997	@ executes_when $true;
2998	@*/
2999	$system[civlc] void $elaborate(int x);
3000	/*@ depends_on \nothing;
3001	@ executes_when $true;
3002	@*/
3003	$system[civlc] int $next_time_count(void);
3004	/*@ pure;
3005	@ depends_on \nothing;
3006	@ executes_when $true;
3007	@*/
3008	$system[civlc] void $pathCondition(void);
3009	/*@ pure;
3010	@ depends_on \nothing;
3011	@ executes_when $true;
3012	@*/
3013	$system[civlc] _Bool $is_concrete_int(int value);
3014	/*@ depends_on \nothing;
3015	@ executes_when $true;
3016	@*/
3017	$system[civlc] void* $malloc($scope s, int size);
3018	/*@ depends_on \write(p);
3019	@ executes_when $true;
3020	@*/
3021	$system[civlc] void $free(void* p);
3022	/*@ depends_on \write(ptr);
3023	@ executes_when $true;
3024	@*/
3025	$system[civlc] void $havoc(void* ptr);
3026	/*@ pure;
3027	@ depends_on \nothing;
3028	@ executes_when $true;
3029	@*/
3030	$system[civlc] double $pow(double base, double exp);
3031	//======================= bundle.cvh =======================
3032	/*@ depends_on \nothing;
3033	@ executes_when $true;
3034	@*/
3035	$system[bundle] int $bundle_size($bundle b);
3036	/*@ depends_on \write(ptr);
3037	@ executes_when $true;
3038	@*/
3039	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
3040	/*@ depends_on \write(ptr);
3041	@ executes_when $true;
3042	@*/
3043	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
3044	/*@ depends_on \write(buf);
3045	@ executes_when $true;
3046	@*/
3047	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
3048	//======================== comm.cvh ========================
3049	/*@ pure;
3050	@ depends_on \nothing;
3051	@ executes_when $true;
3052	@*/
3053	$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
3054	/*@ pure;
3055	@ depends_on \nothing;
3056	@ executes_when $true;
3057	@*/
3058	$atomic_f int $message_source($message message);
3059	/*@ pure;
3060	@ depends_on \nothing;
3061	@ executes_when $true;
3062	@*/
3063	$atomic_f int $message_tag($message message);
3064	/*@ pure;
3065	@ depends_on \nothing;
3066	@ executes_when $true;
3067	@*/
3068	$atomic_f int $message_dest($message message);
3069	/*@ pure;
3070	@ depends_on \nothing;
3071	@ executes_when $true;
3072	@*/
3073	$atomic_f int $message_size($message message);
3074	/*@ depends_on \write(buf);
3075	@ executes_when $true;
3076	@*/
3077	$atomic_f void $message_unpack($message message, void* buf, int size);
3078	/*@ depends_on \nothing;
3079	@ assigns \nothing;
3080	@ reads \nothing;
3081	@*/
3082	$atomic_f $gcomm $gcomm_create($scope scope, int size);
3083	/*@ depends_on \write(junkMsgs), \write(gcomm);
3084	@ assigns junkMsgs, gcomm;
3085	@*/
3086	$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
3087	/*@ depends_on \nothing;
3088	@ executes_when $true;
3089	@*/
3090	$system[comm] void $gcomm_dup($comm comm, $comm newcomm);
3091	$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
3092	/*@ depends_on \write(comm);
3093	@ assigns comm;
3094	@ reads \nothing;
3095	@*/
3096	$atomic_f void $comm_destroy($comm comm);
3097	/*@ pure;
3098	@ depends_on \nothing;
3099	@*/
3100	$atomic_f int $comm_size($comm comm);
3101	/*@ pure;
3102	@ depends_on \nothing;
3103	@ executes_when $true;
3104	@*/
3105	$atomic_f int $comm_place($comm comm);
3106	/*@ depends_on \write(comm);
3107	@ executes_when $true;
3108	@*/
3109	$system[comm] void $comm_enqueue($comm comm, $message message);
3110	/*@ pure;
3111	@ depends_on \write(comm);
3112	@ executes_when $true;
3113	@*/
3114	$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
3115	/*@ pure;
3116	@ depends_on \write(comm);
3117	@ executes_when $true;
3118	@*/
3119	$system[comm] $message $comm_seek($comm comm, int source, int tag);
3120	/*@ depends_on \write(comm);
3121	@ executes_when $comm_probe(comm, source, tag);
3122	@*/
3123	$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
3124	//========================= seq.cvh ========================
3125	/*@ depends_on \write(array);
3126	@ executes_when $true;
3127	@*/
3128	$system[seq] int $seq_length(void* array);
3129	/*@ depends_on \write(array, value);
3130	@ executes_when $true;
3131	@*/
3132	$system[seq] void $seq_init(void* array, int count, void* value);
3133	/*@ depends_on \write(array, values);
3134	@ executes_when $true;
3135	@*/
3136	$system[seq] void $seq_insert(void* array, int index, void* values, int count);
3137	/*@ depends_on \write(array, values);
3138	@ executes_when $true;
3139	@*/
3140	$system[seq] void $seq_remove(void* array, int index, void* values, int count);
3141	/*@ depends_on \write(array, values);
3142	@*/
3143	$atomic_f void $seq_append(void* array, void* values, int count);
3144	//======================== comm.cvl ========================
3145	struct _queue{
3146	int length;
3147	$message messages[];
3148	};
3149	struct _gcomm{
3150	int nprocs;
3151	$proc procs[];
3152	_Bool isInit[];
3153	$queue buf[][];
3154	};
3155	struct _comm{
3156	int place;
3157	$gcomm gcomm;
3158	};
3159	/*@ depends_on \write(data);
3160	@*/
3161	$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size)
3162	{
3163	$message result;
3164	result.source = source;
3165	result.dest = dest;
3166	result.tag = tag;
3167	result.data = $bundle_pack(data, size);
3168	result.size = size;
3169	return result;
3170	}
3171	int $message_source($message message)
3172	{
3173	return message.source;
3174	}
3175	int $message_tag($message message)
3176	{
3177	return message.tag;
3178	}
3179	int $message_dest($message message)
3180	{
3181	return message.dest;
3182	}
3183	int $message_size($message message)
3184	{
3185	return message.size;
3186	}
3187	/*@ depends_on \write(buf);
3188	@*/
3189	$atomic_f void $message_unpack($message message, void* buf, int size)
3190	{
3191	$bundle_unpack(message.data, buf);
3192	$assert(message.size <= size, "Message of size %d exceeds the specified size %d.", message.size, size);
3193	}
3194	/*@ depends_on \nothing;
3195	@ assigns \nothing;
3196	@ reads \nothing;
3197	@*/
3198	$atomic_f $gcomm $gcomm_create($scope scope, int size)
3199	{
3200	$gcomm gcomm = ($gcomm)($malloc(scope, sizeof(struct _gcomm)));
3201	$queue empty;
3202	empty.length = 0;
3203	$seq_init(&(empty.messages), 0, (void*)0);
3204	(gcomm)->nprocs = size;
3205	(gcomm)->procs = ($proc[size]) $lambda (int i) $proc_null;
3206	(gcomm)->isInit = (_Bool[size]) $lambda (int i) $false;
3207	(gcomm)->buf = ($queue[size][size]) $lambda (int i, j) empty;
3208	return gcomm;
3209	}
3210	/*@ depends_on \write(junkMsgs), \write(gcomm);
3211	@ assigns junkMsgs, gcomm;
3212	@ reads \nothing;
3213	@*/
3214	$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs)
3215	{
3216	int nprocs = (gcomm)->nprocs;
3217	int numJunks = 0;
3218	if (junkMsgs != (void*)0)
3219	{
3220	for (int i = 0; i < nprocs; i++)
3221	for (int j = 0; j < nprocs; j++)
3222	{
3223	$queue queue = (gcomm)->buf[i][j];
3224	if (queue.length > 0)
3225	$seq_append(junkMsgs, queue.messages, queue.length);
3226	}
3227	numJunks = $seq_length(junkMsgs);
3228	}
3229	$free(gcomm);
3230	return numJunks;
3231	}
3232	/*@ depends_on \nothing;
3233	@ reads gcomm;
3234	@ assigns gcomm;
3235	@*/
3236	$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place)
3237	{
3238	$assert(!((gcomm)->isInit[place]), "the place %d is already occupied in the global communicator!", place);
3239	$comm comm = ($comm)($malloc(scope, sizeof(struct _comm)));
3240	(gcomm)->procs[place] = $self;
3241	(gcomm)->isInit[place] = $true;
3242	(comm)->gcomm = gcomm;
3243	(comm)->place = place;
3244	return comm;
3245	}
3246	/*@ depends_on \write(comm);
3247	@ assigns comm;
3248	@ reads \nothing;
3249	@*/
3250	$atomic_f void $comm_destroy($comm comm)
3251	{
3252	$free(comm);
3253	}
3254	/*@ pure;
3255	@ depends_on \nothing;
3256	@*/
3257	$atomic_f int $comm_place($comm comm)
3258	{
3259	return (comm)->place;
3260	}
3261	/*@ pure;
3262	@ depends_on \nothing;
3263	@*/
3264	$atomic_f int $comm_size($comm comm)
3265	{
3266	return ((comm)->gcomm)->nprocs;
3267	}
3268	//======================== civlc.cvh =======================
3269	$system[civlc] void $wait($proc p);
3270	$system[civlc] void $waitall($proc* procs, int numProcs);
3271	/*@ depends_on \nothing;
3272	@ executes_when $true;
3273	@*/
3274	$system[civlc] void $exit(void);
3275	/*@ depends_on \nothing;
3276	@ executes_when $true;
3277	@*/
3278	$system[civlc] int $choose_int(int n);
3279	/*@ depends_on \nothing;
3280	@ executes_when $true;
3281	@*/
3282	$system[civlc] void $assert(_Bool expr, ...);
3283	/*@ depends_on \nothing;
3284	@ executes_when $true;
3285	@*/
3286	$system[civlc] void $assume(_Bool expr);
3287	/*@ pure;
3288	@ depends_on \nothing;
3289	@ executes_when $true;
3290	@*/
3291	$system[civlc] void $elaborate(int x);
3292	/*@ depends_on \nothing;
3293	@ executes_when $true;
3294	@*/
3295	$system[civlc] int $next_time_count(void);
3296	/*@ pure;
3297	@ depends_on \nothing;
3298	@ executes_when $true;
3299	@*/
3300	$system[civlc] void $pathCondition(void);
3301	/*@ pure;
3302	@ depends_on \nothing;
3303	@ executes_when $true;
3304	@*/
3305	$system[civlc] _Bool $is_concrete_int(int value);
3306	/*@ depends_on \nothing;
3307	@ executes_when $true;
3308	@*/
3309	$system[civlc] void* $malloc($scope s, int size);
3310	/*@ depends_on \write(p);
3311	@ executes_when $true;
3312	@*/
3313	$system[civlc] void $free(void* p);
3314	/*@ depends_on \write(ptr);
3315	@ executes_when $true;
3316	@*/
3317	$system[civlc] void $havoc(void* ptr);
3318	/*@ pure;
3319	@ depends_on \nothing;
3320	@ executes_when $true;
3321	@*/
3322	$system[civlc] double $pow(double base, double exp);
3323	//======================= bundle.cvh =======================
3324	/*@ depends_on \nothing;
3325	@ executes_when $true;
3326	@*/
3327	$system[bundle] int $bundle_size($bundle b);
3328	/*@ depends_on \write(ptr);
3329	@ executes_when $true;
3330	@*/
3331	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
3332	/*@ depends_on \write(ptr);
3333	@ executes_when $true;
3334	@*/
3335	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
3336	/*@ depends_on \write(buf);
3337	@ executes_when $true;
3338	@*/
3339	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
3340	//===================== concurrency.cvh ====================
3341	/*@ depends_on \nothing;
3342	@ assigns \nothing;
3343	@ reads \nothing;
3344	@*/
3345	$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
3346	/*@ depends_on \write(gbarrier);
3347	@ reads \nothing;
3348	@ assigns gbarrier;
3349	@*/
3350	$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
3351	/*@ depends_on \nothing;
3352	@ assigns gbarrier;
3353	@ reads gbarrier;
3354	@*/
3355	$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
3356	/*@ depends_on \write(barrier);
3357	@ assigns barrier;
3358	@ reads \nothing;
3359	@*/
3360	$atomic_f void $barrier_destroy($barrier barrier);
3361	void $barrier_call($barrier barrier);
3362	/*@ depends_on \nothing;
3363	@ reads \nothing;
3364	@ assigns \nothing;
3365	@*/
3366	$atomic_f $gcollator $gcollator_create($scope scope);
3367	/*@ depends_on \write(gcollator);
3368	@ assigns gcollator;
3369	@ reads \nothing;
3370	@*/
3371	$atomic_f int $gcollator_destroy($gcollator gcollator);
3372	/*@ depends_on \nothing;
3373	@ executes_when $true;
3374	@*/
3375	$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
3376	/*@ depends_on \write(collator);
3377	@ executes_when $true;
3378	@*/
3379	$atomic_f void $collator_destroy($collator collator);
3380	/*@ depends_on \write(collator);
3381	@ executes_when $true;
3382	@*/
3383	$system[concurrency] $bundle $collator_check($collator collator, int place, int nprocs, $bundle entries);
3384	//========================= seq.cvh ========================
3385	/*@ depends_on \write(array);
3386	@ executes_when $true;
3387	@*/
3388	$system[seq] int $seq_length(void* array);
3389	/*@ depends_on \write(array, value);
3390	@ executes_when $true;
3391	@*/
3392	$system[seq] void $seq_init(void* array, int count, void* value);
3393	/*@ depends_on \write(array, values);
3394	@ executes_when $true;
3395	@*/
3396	$system[seq] void $seq_insert(void* array, int index, void* values, int count);
3397	/*@ depends_on \write(array, values);
3398	@ executes_when $true;
3399	@*/
3400	$system[seq] void $seq_remove(void* array, int index, void* values, int count);
3401	/*@ depends_on \write(array, values);
3402	@*/
3403	$atomic_f void $seq_append(void* array, void* values, int count);
3404	//===================== concurrency.cvl ====================
3405	struct _gbarrier{
3406	int nprocs;
3407	$proc proc_map[];
3408	_Bool in_barrier[];
3409	int num_in_barrier;
3410	};
3411	struct _barrier{
3412	int place;
3413	$gbarrier gbarrier;
3414	};
3415	struct _collator_entry{
3416	$bundle entries;
3417	_Bool marks[];
3418	int numMarked;
3419	};
3420	struct _gcollator{
3421	int length;
3422	$collator_entry entries[];
3423	};
3424	struct _collator{
3425	$gcollator gcollator;
3426	};
3427	/*@ depends_on \write(barrier);
3428	@ assigns \nothing;
3429	@ executes_when $true;
3430	@*/
3431	$system[concurrency] void $barrier_enter($barrier barrier);
3432	/*@ depends_on \write(barrier);
3433	@ assigns \nothing;
3434	@*/
3435	$system[concurrency] void $barrier_exit($barrier barrier);
3436	void $barrier_call($barrier barrier)
3437	{
3438	$barrier_enter(barrier);
3439	$barrier_exit(barrier);
3440	}
3441	/*@ depends_on \nothing;
3442	@ assigns \nothing;
3443	@ reads \nothing;
3444	@*/
3445	$atomic_f $gbarrier $gbarrier_create($scope scope, int size)
3446	{
3447	$gbarrier gbarrier = ($gbarrier)($malloc(scope, sizeof(struct _gbarrier)));
3448	(gbarrier)->nprocs = size;
3449	(gbarrier)->proc_map = ($proc[size]) $lambda (int i) $proc_null;
3450	(gbarrier)->in_barrier = (_Bool[size]) $lambda (int i) $false;
3451	(gbarrier)->num_in_barrier = 0;
3452	return gbarrier;
3453	}
3454	/*@ depends_on \write(gbarrier);
3455	@ reads \nothing;
3456	@ assigns gbarrier;
3457	@*/
3458	$atomic_f void $gbarrier_destroy($gbarrier gbarrier)
3459	{
3460	$free(gbarrier);
3461	}
3462	/*@ depends_on \nothing;
3463	@ assigns gbarrier;
3464	@ reads gbarrier;
3465	@*/
3466	$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place)
3467	{
3468	$assert(((gbarrier)->proc_map[place]) == $proc_null, "the place %d in the global barrier has already been taken.", place);
3469	$barrier barrier = ($barrier)($malloc(scope, sizeof(struct _barrier)));
3470	(barrier)->place = place;
3471	(barrier)->gbarrier = gbarrier;
3472	(gbarrier)->proc_map[place] = $self;
3473	return barrier;
3474	}
3475	/*@ depends_on \write(barrier);
3476	@ assigns barrier;
3477	@ reads \nothing;
3478	@*/
3479	$atomic_f void $barrier_destroy($barrier barrier)
3480	{
3481	$free(barrier);
3482	}
3483	/*@ depends_on \nothing;
3484	@ reads \nothing;
3485	@ assigns \nothing;
3486	@*/
3487	$atomic_f $gcollator $gcollator_create($scope scope)
3488	{
3489	$gcollator gcollator = ($gcollator)($malloc(scope, sizeof(struct _gcollator)));
3490	(gcollator)->length = 0;
3491	$seq_init(&((gcollator)->entries), 0, (void*)0);
3492	return gcollator;
3493	}
3494	/*@ depends_on \write(gcollator);
3495	@ assigns gcollator;
3496	@ reads \nothing;
3497	@*/
3498	$atomic_f int $gcollator_destroy($gcollator gcollator)
3499	{
3500	int numRemaining = (gcollator)->length;
3501	$free(gcollator);
3502	return numRemaining;
3503	}
3504	/*@ depends_on \nothing;
3505	@ executes_when $true;
3506	@*/
3507	$atomic_f $collator $collator_create($scope scope, $gcollator gcollator)
3508	{
3509	$collator collator = ($collator)($malloc(scope, sizeof(struct _collator)));
3510	(collator)->gcollator = gcollator;
3511	return collator;
3512	}
3513	/*@ depends_on \write(collator);
3514	@ executes_when $true;
3515	@*/
3516	$atomic_f void $collator_destroy($collator collator)
3517	{
3518	$free(collator);
3519	}
3520	//======================== civlc.cvh =======================
3521	$system[civlc] void $wait($proc p);
3522	$system[civlc] void $waitall($proc* procs, int numProcs);
3523	/*@ depends_on \nothing;
3524	@ executes_when $true;
3525	@*/
3526	$system[civlc] void $exit(void);
3527	/*@ depends_on \nothing;
3528	@ executes_when $true;
3529	@*/
3530	$system[civlc] int $choose_int(int n);
3531	/*@ depends_on \nothing;
3532	@ executes_when $true;
3533	@*/
3534	$system[civlc] void $assert(_Bool expr, ...);
3535	/*@ depends_on \nothing;
3536	@ executes_when $true;
3537	@*/
3538	$system[civlc] void $assume(_Bool expr);
3539	/*@ pure;
3540	@ depends_on \nothing;
3541	@ executes_when $true;
3542	@*/
3543	$system[civlc] void $elaborate(int x);
3544	/*@ depends_on \nothing;
3545	@ executes_when $true;
3546	@*/
3547	$system[civlc] int $next_time_count(void);
3548	/*@ pure;
3549	@ depends_on \nothing;
3550	@ executes_when $true;
3551	@*/
3552	$system[civlc] void $pathCondition(void);
3553	/*@ pure;
3554	@ depends_on \nothing;
3555	@ executes_when $true;
3556	@*/
3557	$system[civlc] _Bool $is_concrete_int(int value);
3558	/*@ depends_on \nothing;
3559	@ executes_when $true;
3560	@*/
3561	$system[civlc] void* $malloc($scope s, int size);
3562	/*@ depends_on \write(p);
3563	@ executes_when $true;
3564	@*/
3565	$system[civlc] void $free(void* p);
3566	/*@ depends_on \write(ptr);
3567	@ executes_when $true;
3568	@*/
3569	$system[civlc] void $havoc(void* ptr);
3570	/*@ pure;
3571	@ depends_on \nothing;
3572	@ executes_when $true;
3573	@*/
3574	$system[civlc] double $pow(double base, double exp);
3575	//======================== string.h ========================
3576	void* memcpy(void* p, void* q, size_t size);
3577	void* memmove(void* dest, void* src, size_t n);
3578	$system[string] void* memset(void* s, int c, size_t n);
3579	int memcmp(void* s1, void* s2, size_t n);
3580	void* memchr(void* s, int c, size_t n);
3581	$system[string] char* strcpy(char* restrict s1, char* restrict s2);
3582	char* strncpy(char* dest, char* src, size_t n);
3583	char* strcat(char* dest, char* src);
3584	char* strncat(char* dest, char* src, size_t n);
3585	$system[string] int strcmp(char* s1, char* s2);
3586	int strncmp(char* s1, char* s2, size_t n);
3587	int strcoll(char* s1, char* s2);
3588	size_t strxfrm(char* dest, char* src, size_t n);
3589	char* strchr(char* s, int c);
3590	char* strrchr(char* s, int c);
3591	size_t strcspn(char* s, char* reject);
3592	size_t strspn(char* s, char* accept);
3593	char* strpbrk(char* s, char* accept);
3594	char* strstr(char* s1, char* s2);
3595	char* strtok(char* s, char* delim);
3596	$system[string] size_t strlen(char* s);
3597	char* strerror(int errnum);
3598	//======================= bundle.cvh =======================
3599	/*@ depends_on \nothing;
3600	@ executes_when $true;
3601	@*/
3602	$system[bundle] int $bundle_size($bundle b);
3603	/*@ depends_on \write(ptr);
3604	@ executes_when $true;
3605	@*/
3606	$system[bundle] $bundle $bundle_pack(void* ptr, int size);
3607	/*@ depends_on \write(ptr);
3608	@ executes_when $true;
3609	@*/
3610	$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
3611	/*@ depends_on \write(buf);
3612	@ executes_when $true;
3613	@*/
3614	$system[bundle] void $bundle_unpack_apply($bundle data, void* buf, int size, $operation op);
3615	//======================= string.cvl =======================
3616	void* memcpy(void* p, void* q, const size_t size)
3617	{
3618	if (size == 0)
3619	return p;
3620	$bundle bundle = $bundle_pack(q, size);
3621	$bundle_unpack(bundle, p);
3622	return p;
3623	}
3624	//======================== civlc.cvh =======================
3625	$system[civlc] void $wait($proc p);
3626	$system[civlc] void $waitall($proc* procs, int numProcs);
3627	/*@ depends_on \nothing;
3628	@ executes_when $true;
3629	@*/
3630	$system[civlc] void $exit(void);
3631	/*@ depends_on \nothing;
3632	@ executes_when $true;
3633	@*/
3634	$system[civlc] int $choose_int(int n);
3635	/*@ depends_on \nothing;
3636	@ executes_when $true;
3637	@*/
3638	$system[civlc] void $assert(_Bool expr, ...);
3639	/*@ depends_on \nothing;
3640	@ executes_when $true;
3641	@*/
3642	$system[civlc] void $assume(_Bool expr);
3643	/*@ pure;
3644	@ depends_on \nothing;
3645	@ executes_when $true;
3646	@*/
3647	$system[civlc] void $elaborate(int x);
3648	/*@ depends_on \nothing;
3649	@ executes_when $true;
3650	@*/
3651	$system[civlc] int $next_time_count(void);
3652	/*@ pure;
3653	@ depends_on \nothing;
3654	@ executes_when $true;
3655	@*/
3656	$system[civlc] void $pathCondition(void);
3657	/*@ pure;
3658	@ depends_on \nothing;
3659	@ executes_when $true;
3660	@*/
3661	$system[civlc] _Bool $is_concrete_int(int value);
3662	/*@ depends_on \nothing;
3663	@ executes_when $true;
3664	@*/
3665	$system[civlc] void* $malloc($scope s, int size);
3666	/*@ depends_on \write(p);
3667	@ executes_when $true;
3668	@*/
3669	$system[civlc] void $free(void* p);
3670	/*@ depends_on \write(ptr);
3671	@ executes_when $true;
3672	@*/
3673	$system[civlc] void $havoc(void* ptr);
3674	/*@ pure;
3675	@ depends_on \nothing;
3676	@ executes_when $true;
3677	@*/
3678	$system[civlc] double $pow(double base, double exp);
3679	//======================== stdlib.h ========================
3680	double atof(char* nptr);
3681	int atoi(char* nptr);
3682	long atol(char* nptr);
3683	long long atoll(char* nptr);
3684	double strtod(char* restrict nptr, char** restrict endptr);
3685	float strtof(char* restrict nptr, char** restrict endptr);
3686	long double strtold(char* restrict nptr, char** restrict endptr);
3687	long strtol(char* restrict nptr, char** restrict endptr, int base);
3688	long long strtoll(char* restrict nptr, char** restrict endptr, int base);
3689	unsigned long strtoul(char* restrict nptr, char** restrict endptr, int base);
3690	unsigned long long strtoull(char* restrict nptr, char** restrict endptr, int base);
3691	$system[stdlib] int rand(void);
3692	$system[stdlib] void srand(unsigned seed);
3693	$system[stdlib] long random(void);
3694	$system[stdlib] void srandom(unsigned seed);
3695	void* aligned_alloc(size_t alignment, size_t size);
3696	void* calloc(size_t nmemb, size_t size);
3697	$system[stdlib] void free(void* ptr);
3698	$system[stdlib] void* malloc(size_t size);
3699	void* realloc(void* ptr, size_t size);
3700	_Noreturn void abort(void);
3701	int atexit( (void (void))* func);
3702	int at_quick_exit( (void (void))* func);
3703	$system[stdlib] void exit(int status);
3704	_Noreturn void _Exit(int status);
3705	char* getenv(char* name);
3706	_Noreturn void quick_exit(int status);
3707	int system(char* string);
3708	void* bsearch(void* key, void* base, size_t nmemb, size_t size, (int (void, void))* compar);
3709	void qsort(void* base, size_t nmemb, size_t size, (int (void, void))* compar);
3710	int abs(int j);
3711	long labs(long j);
3712	long long llabs(long long j);
3713	div_t div(int numer, int denom);
3714	ldiv_t ldiv(long numer, long denom);
3715	lldiv_t lldiv(long long numer, long long denom);
3716	int mblen(char* s, size_t n);
3717	int mbtowc(wchar_t* restrict pwc, char* restrict s, size_t n);
3718	int wctomb(char* s, wchar_t wchar);
3719	size_t mbstowcs(wchar_t* restrict pwcs, char* restrict s, size_t n);
3720	size_t wcstombs(char* restrict s, wchar_t* restrict pwcs, size_t n);
3721	constraint_handler_t set_constraint_handler_s(constraint_handler_t handler);
3722	void abort_handler_s(char* restrict msg, void* restrict ptr, errno_t error);
3723	void ignore_handler_s(char* restrict msg, void* restrict ptr, errno_t error);
3724	errno_t getenv_s(size_t* restrict len, char* restrict value, rsize_t maxsize, char* restrict name);
3725	void* bsearch_s(void* key, void* base, rsize_t nmemb, rsize_t size, (int (void* k, void* y, void* context))* compar, void* context);
3726	errno_t qsort_s(void* base, rsize_t nmemb, rsize_t size, (int (void* x, void* y, void* context))* compar, void* context);
3727	errno_t wctomb_s(int* restrict status, char* restrict s, rsize_t smax, wchar_t wc);
3728	errno_t mbstowcs_s(size_t* restrict retval, wchar_t* restrict dst, rsize_t dstmax, char* restrict src, rsize_t len);
3729	errno_t wcstombs_s(size_t* restrict retval, char* restrict dst, rsize_t dstmax, wchar_t* restrict src, rsize_t len);
3730	//======================= stdlib.cvl =======================
3731	int rand()
3732	{
3733	int tmp;
3734	$havoc(&(tmp));
3735	return tmp;
3736	}
3737	void srand(unsigned seed)
3738	{
3739	}
3740	void srandom(unsigned seed)
3741	{
3742	}
3743	long random()
3744	{
3745	long tmp;
3746	$havoc(&(tmp));
3747	return tmp;
3748	}
3749	void exit(int status)
3750	{
3751	$assert(status == 0, "erroneous exit with code %d", status);
3752	$exit();
3753	}
3754	_Noreturn void abort(void)
3755	{
3756	$exit();
3757	}
3758	int abs(int x)
3759	{
3760	if (x >= 0)
3761	return x;
3762	return -x;
3763	}
3764	//======================== civlc.cvh =======================
3765	$system[civlc] void $wait($proc p);
3766	$system[civlc] void $waitall($proc* procs, int numProcs);
3767	/*@ depends_on \nothing;
3768	@ executes_when $true;
3769	@*/
3770	$system[civlc] void $exit(void);
3771	/*@ depends_on \nothing;
3772	@ executes_when $true;
3773	@*/
3774	$system[civlc] int $choose_int(int n);
3775	/*@ depends_on \nothing;
3776	@ executes_when $true;
3777	@*/
3778	$system[civlc] void $assert(_Bool expr, ...);
3779	/*@ depends_on \nothing;
3780	@ executes_when $true;
3781	@*/
3782	$system[civlc] void $assume(_Bool expr);
3783	/*@ pure;
3784	@ depends_on \nothing;
3785	@ executes_when $true;
3786	@*/
3787	$system[civlc] void $elaborate(int x);
3788	/*@ depends_on \nothing;
3789	@ executes_when $true;
3790	@*/
3791	$system[civlc] int $next_time_count(void);
3792	/*@ pure;
3793	@ depends_on \nothing;
3794	@ executes_when $true;
3795	@*/
3796	$system[civlc] void $pathCondition(void);
3797	/*@ pure;
3798	@ depends_on \nothing;
3799	@ executes_when $true;
3800	@*/
3801	$system[civlc] _Bool $is_concrete_int(int value);
3802	/*@ depends_on \nothing;
3803	@ executes_when $true;
3804	@*/
3805	$system[civlc] void* $malloc($scope s, int size);
3806	/*@ depends_on \write(p);
3807	@ executes_when $true;
3808	@*/
3809	$system[civlc] void $free(void* p);
3810	/*@ depends_on \write(ptr);
3811	@ executes_when $true;
3812	@*/
3813	$system[civlc] void $havoc(void* ptr);
3814	/*@ pure;
3815	@ depends_on \nothing;
3816	@ executes_when $true;
3817	@*/
3818	$system[civlc] double $pow(double base, double exp);
3819	//========================= seq.cvh ========================
3820	/*@ depends_on \write(array);
3821	@ executes_when $true;
3822	@*/
3823	$system[seq] int $seq_length(void* array);
3824	/*@ depends_on \write(array, value);
3825	@ executes_when $true;
3826	@*/
3827	$system[seq] void $seq_init(void* array, int count, void* value);
3828	/*@ depends_on \write(array, values);
3829	@ executes_when $true;
3830	@*/
3831	$system[seq] void $seq_insert(void* array, int index, void* values, int count);
3832	/*@ depends_on \write(array, values);
3833	@ executes_when $true;
3834	@*/
3835	$system[seq] void $seq_remove(void* array, int index, void* values, int count);
3836	/*@ depends_on \write(array, values);
3837	@*/
3838	$atomic_f void $seq_append(void* array, void* values, int count);
3839	//========================= seq.cvl ========================
3840	/*@ depends_on \write(array, values);
3841	@*/
3842	$atomic_f void $seq_append(void* array, void* values, int count)
3843	{
3844	int length = $seq_length(array);
3845	$seq_insert(array, length, values, count);
3846	}
3847	//=================== ContractTransformer ==================
3848	int MPI_Comm_rank(MPI_Comm decl0, int* decl1);
3849	int MPI_Comm_size(MPI_Comm decl0, int* decl1);
3850	int MPI_Init(int* decl0, char*** decl1);
3851	int MPI_Finalize();
3852	$systemvoid $havoc(void* decl0);
3853	$collate_state $mpi_snapshot(MPI_Comm decl0);
3854	int $mpi_contract_enters(MPI_Comm decl0);
3855	int $mpi_contract_entered(MPI_Comm decl0, $range decl1);
3856	$system_Bool $collate_complete($collate_state decl0);
3857	$system_Bool $collate_arrived($collate_state decl0, $range decl1);
3858	//======================= allgather.c ======================
3859	int broadcast(void* buf, int count, MPI_Datatype datatype, int root, MPI_Comm comm)
3860	{
3861	int $mpi_comm_rank;
3862	int $mpi_comm_size;
3863	MPI_Comm_rank(comm, &($mpi_comm_rank));
3864	MPI_Comm_size(comm, &($mpi_comm_size));
3865	$collate_state _conc_cp0 = $mpi_snapshot(comm);
3866	$run
3867	$when ($collate_complete(_conc_cp0))
3868	$with(_conc_cp0) {
3869	$assert(((0 < count) && (count <= 3)) && ($mpi_valid(buf, count, datatype) && (((0 <= root) && (root < $mpi_comm_size)) && ($mpi_agree(root) && $mpi_agree(count * $mpi_extent(datatype))))));
3870	if ($mpi_comm_rank != root)
3871	$assert();
3872	$assert($comm_empty_in(comm.p2p) && $comm_empty_out(comm.p2p));
3873	}
3874	int $result;
3875	$havoc(&($result));
3876	$collate_state _conc_pre_cp1 = $mpi_snapshot(comm);
3877	$with(_conc_pre_cp1) $assume($mpi_equals(buf, count, datatype, \remote(buf , root)) && (\result == 0));
3878	$run
3879	if ($mpi_comm_rank != root)
3880	$when ($collate_arrived(_conc_pre_cp1, root))
3881	$with(_conc_pre_cp1) $assume();
3882	return $result;
3883	}
3884	int gather(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, int root, MPI_Comm comm)
3885	{
3886	int $mpi_comm_rank;
3887	int $mpi_comm_size;
3888	MPI_Comm_rank(comm, &($mpi_comm_rank));
3889	MPI_Comm_size(comm, &($mpi_comm_size));
3890	$collate_state _conc_cp2 = $mpi_snapshot(comm);
3891	$run
3892	$when ($collate_complete(_conc_cp2))
3893	$with(_conc_cp2) {
3894	$assert(($mpi_agree(root) && $mpi_agree($mpi_extent(sendtype) * sendcount)) && (((sendcount > 0) && (sendcount < 3)) && (((recvcount > 0) && (recvcount < 3)) && (((0 <= root) && (root < $mpi_comm_size)) && $mpi_valid(sendbuf, sendcount, sendtype)))));
3895	if ($mpi_comm_rank == root)
3896	$assert($mpi_valid(recvbuf, recvcount * $mpi_comm_size, recvtype) && ((recvcount * $mpi_extent(recvtype)) == (sendcount * $mpi_extent(sendtype))));
3897	$assert($comm_empty_in(comm.p2p) && $comm_empty_out(comm.p2p));
3898	}
3899	int $result;
3900	$havoc(&($result));
3901	$collate_state _conc_pre_cp3 = $mpi_snapshot(comm);
3902	$run
3903	if ($mpi_comm_rank == root)
3904	$when ($collate_arrived(_conc_pre_cp3, 0 .. $mpi_comm_size - 1))
3905	$with(_conc_pre_cp3) $assume($mpi_equals($mpi_offset(recvbuf, root * sendcount, sendtype), sendcount, sendtype, sendbuf) && $forall (int i \| (i >= 0) && (i < $mpi_comm_size)) $mpi_equals($mpi_offset(recvbuf, i * sendcount, recvtype), sendcount, sendtype, \remote(sendbuf , i)));
3906	return $result;
3907	}
3908	int allgather(void* sendbuf, int sendcount, MPI_Datatype sendtype, void* recvbuf, int recvcount, MPI_Datatype recvtype, MPI_Comm comm)
3909	{
3910	int place;
3911	int nprocs;
3912	$elaborate(recvcount);
3913	$elaborate(sendcount);
3914	MPI_Comm_rank(comm, &(place));
3915	MPI_Comm_size(comm, &(nprocs));
3916	gather(sendbuf, sendcount, sendtype, recvbuf, recvcount, recvtype, 0, comm);
3917	broadcast(recvbuf, recvcount * nprocs, recvtype, 0, comm);
3918	return 0;
3919	}
3920	//=================== ContractTransformer ==================
3921	int _driver_allgather()
3922	{
3923	void* sendbuf;
3924	$havoc(&(sendbuf));
3925	int sendcount;
3926	$havoc(&(sendcount));
3927	MPI_Datatype sendtype;
3928	$havoc(&(sendtype));
3929	void* recvbuf;
3930	$havoc(&(recvbuf));
3931	int recvcount;
3932	$havoc(&(recvcount));
3933	MPI_Datatype recvtype;
3934	$havoc(&(recvtype));
3935	MPI_Comm comm = MPI_COMM_WORLD;
3936	int $mpi_comm_rank;
3937	int $mpi_comm_size;
3938	MPI_Comm_rank(comm, &($mpi_comm_rank));
3939	MPI_Comm_size(comm, &($mpi_comm_size));
3940	$collate_state _conc_pre_cp4 = $mpi_snapshot(comm);
3941	$when ($collate_complete(_conc_pre_cp4))
3942	$with(_conc_pre_cp4) {
3943	$assume($mpi_agree(sendcount * $mpi_extent(sendtype)) && (((sendcount >= 0) && (((sendcount * $mpi_extent(sendtype)) * $mpi_comm_size) < 3)) && (((recvcount >= 0) && (((recvcount * $mpi_extent(recvtype)) * $mpi_comm_size) < 3)) && ($mpi_valid(sendbuf, sendcount, sendtype) && ($mpi_valid(recvbuf, recvcount * $mpi_comm_size, recvtype) && (($mpi_extent(recvtype) * recvcount) == ($mpi_extent(sendtype) * sendcount)))))));
3944	}
3945	$mpi_contract_enters(comm);
3946	int $result = allgather(sendbuf, sendcount, sendtype, recvbuf, recvcount, recvtype, comm);
3947	$collate_state _conc_post_cp5 = $mpi_snapshot(comm);
3948	$when ($collate_complete(_conc_post_cp5))
3949	$with(_conc_post_cp5) {
3950	$assert($mpi_agree($mpi_region(recvbuf, recvcount * $mpi_comm_size, recvtype)) && $mpi_equals(sendbuf, sendcount, sendtype, $mpi_offset(recvbuf, $mpi_comm_rank * recvcount, recvtype)));
3951	$assert($comm_empty_in(comm.p2p) && $comm_empty_out(comm.p2p));
3952	}
3953	}
3954	int main()
3955	{
3956	MPI_Init((void)0, (void)0);
3957	_driver_allgather();
3958	MPI_Finalize();
3959	}

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: CIVL/examples/contracts/contractsMPI/auto_allgather.c@ 8b2639d

Download in other formats: