source: CIVL/src/include/civl/comm.cvl@ 3049148

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 3049148 was e045201d, checked in by Ziqing Luo <ziqing@…>, 9 years ago

Added the fix for checking invisibility of deadlock properties.

To improve the performance after that fix, I added a flag in location to indicate if it is a switch or choose with deafult case.

And let statement with conditional expression be marked as binary branching as well

Have to diable the deadlock checking for cudaTests, otherwise they cannot finish

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

  • Property mode set to 100644
File size: 4.4 KB
Line 
1/* This file completes the definitions of some types and functions
2 * for communication, which are declared in comm-common.cvh.
3 */
4
5#ifndef __CIVLC_COMM__
6#define __CIVLC_COMM__
7#include <civlc.cvh>
8#include<comm.cvh>
9#include<seq.cvh>
10#include<pointer.cvh>
11#pragma PARSE_ACSL
12/* *********************** Types *********************** */
13
14/* A datatype representing a queue of messages. All message
15 * data is encapsulated inside this value; no external allocation
16 * is used. Completes the declaration of this structure type in
17 * civlc-common.h */
18struct _queue {
19 int length;
20 $message messages[];
21};
22
23
24/* A global communicator datatype which must be operated by local communicators.
25 * This communicator type has the same meaning as the communicator type
26 * in MPI. Completes the declaration of this type in civlc-common.h */
27struct _gcomm {
28 int nprocs; // number of processes
29 $proc procs[]; // process references
30 _Bool isInit[]; // if the local comm has been initiated
31 $queue buf[][]; // message buffers
32};
33
34/* A datatype representing a local communicator which is used for
35 * operating global communicators. The local communicator type has
36 * a handle of a global communicator. This type represents for
37 * a set of processes which have ranks in common.
38 * Completes the declaration of this type in civlc-common.h.
39 */
40struct _comm {
41 int place;
42 $gcomm gcomm;
43};
44
45/* *********************** Functions *********************** */
46
47/* creates a new message, copying data from the specified buffer */
48$atomic_f $message $message_pack(int source, int dest, int tag,
49 const void *data, int size) {
50 $message result;
51
52 result.source = source;
53 result.dest = dest;
54 result.tag = tag;
55 if (data != NULL && size > 0) {
56 result.data = $bundle_pack(data, size);
57 } else if (data == NULL)
58 $assert(size == 0, "Attempt to pack a non-zero size message with a NULL pointer");
59 result.size = size;
60 return result;
61}
62
63/* returns the message source */
64int $message_source($message message) {
65 return message.source;
66}
67
68/* returns the message tag */
69int $message_tag($message message) {
70 return message.tag;
71}
72
73/* returns the message destination */
74int $message_dest($message message) {
75 return message.dest;
76}
77
78/* returns the message size */
79int $message_size($message message) {
80 return message.size;
81}
82
83/* transfers message data to buf, throwing exception if message
84 * size exceeds specified size */
85$atomic_f void $message_unpack($message message, void *buf, int size) {
86 if (buf != NULL && message.size > 0) {
87 $bundle_unpack(message.data, buf);
88 $assert(message.size <= size, "Message of size %d exceeds the specified size %d.",
89 message.size, size);
90 }
91 else if (buf == NULL)
92 $assert(message.size == 0,
93 "Attempt to unpack a non-zero size message with a NULL pointer.");
94}
95
96$atomic_f $gcomm $gcomm_create($scope scope, int size){
97 $gcomm gcomm=($gcomm)$malloc(scope, sizeof(struct _gcomm));
98 $queue empty;
99
100 empty.length=0;
101 $seq_init(&empty.messages, 0, NULL);
102 gcomm->nprocs=size;
103 gcomm->procs=(($proc[size])$lambda(int i)$proc_null);
104 gcomm->isInit=((_Bool[size])$lambda(int i)$false);
105 gcomm->buf=(($queue[size][size])$lambda(int i,j) empty);
106 return gcomm;
107}
108
109$atomic_f int $gcomm_destroy($gcomm gcomm, void * junkMsgs){
110 int nprocs = gcomm->nprocs;
111 int numJunks = 0;
112
113 if(junkMsgs != NULL) {
114 for (int i = 0; i < nprocs; i++)
115 for (int j = 0; j < nprocs; j++) {
116 $queue queue = gcomm->buf[i][j];
117
118 if (queue.length > 0)
119 $seq_append(junkMsgs, queue.messages, queue.length);
120 }
121 numJunks = $seq_length(junkMsgs);
122 }
123 $free(gcomm);
124 return numJunks;
125}
126
127/*@ executes_when \true;
128 @ depends_on \access(comm->gcomm, newcomm->gcomm); */
129$atomic_f void $gcomm_dup($comm comm, $comm newcomm){
130 $copy(newcomm->gcomm, comm->gcomm);
131}
132
133$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place){
134 $assert(!gcomm->isInit[place], "the place %d is already occupied in the global communicator!", place);
135
136 $comm comm=($comm)$malloc(scope, sizeof(struct _comm));
137
138 gcomm->procs[place]=$self;
139 gcomm->isInit[place]=$true;
140 comm->gcomm=gcomm;
141 comm->place=place;
142 return comm;
143}
144
145$atomic_f void $comm_destroy($comm comm){
146 $free(comm);
147}
148
149/* Returns the place of the local communicator. This is the same as the
150 * place argument used to create the local communicator. */
151$atomic_f int $comm_place($comm comm){
152 return comm->place;
153}
154
155$atomic_f int $comm_size($comm comm){
156 return comm->gcomm->nprocs;
157}
158
159#endif
Note: See TracBrowser for help on using the repository browser.