0b55f123 |
1 | /* |
2 | * PROMELA Validation Model |
3 | * FLOW CONTROL LAYER VALIDATION |
4 | */ |
5 | |
6 | #define LOSS 1 /* message loss */ |
7 | #define DUPS 0 /* duplicate msgs */ |
8 | #define QSZ 2 /* queue size */ |
9 | |
10 | mtype = { |
11 | red, white, blue, |
12 | abort, accept, ack, sync_ack, close, connect, |
13 | create, data, eof, open, reject, sync, transfer, |
14 | FATAL, NON_FATAL, COMPLETE |
15 | } |
16 | |
17 | chan ses_to_flow[2] = [QSZ] of { byte, byte }; |
18 | chan flow_to_ses[2] = [QSZ] of { byte, byte }; |
19 | chan dll_to_flow[2] = [QSZ] of { byte, byte }; |
20 | |
21 | /* |
22 | * Flow Control Layer Validation Model |
23 | */ |
24 | |
25 | #define true 1 |
26 | #define false 0 |
27 | |
28 | #define M 4 /* range sequence numbers */ |
29 | #define W 2 /* window size: M/2 */ |
30 | |
31 | proctype fc(chan s2f, f2d, f2s, d2f) |
32 | { bool busy[M]; /* outstanding messages */ |
33 | byte q; /* seq# oldest unacked msg */ |
34 | byte m; /* seq# last msg received */ |
35 | byte s; /* seq# next msg to send */ |
36 | byte window; /* nr of outstanding msgs */ |
37 | byte type; /* msg type */ |
38 | bit received[M]; /* receiver housekeeping */ |
39 | bit x; /* scratch variable */ |
40 | byte p; /* seq# of last msg acked */ |
41 | byte I_buf[M], O_buf[M]; /* message buffers */ |
42 | |
43 | xr s2f; |
44 | xs f2d; |
45 | xs f2s; |
46 | xr d2f; |
47 | |
48 | /* sender part */ |
49 | end: do |
50 | :: atomic { |
51 | (window < W && nempty(s2f) |
52 | && nfull(f2d)) -> |
53 | s2f?type,x; |
54 | window = window + 1; |
55 | busy[s] = true; |
56 | O_buf[s] = type; |
57 | f2d!type,s; |
58 | if |
59 | :: (type != sync) -> |
60 | s = (s+1)%M |
61 | :: (type == sync) -> |
62 | window = 0; |
63 | s = M; |
64 | do |
65 | :: (s > 0) -> |
66 | s = s-1; |
67 | busy[s] = false |
68 | :: (s == 0) -> |
69 | break |
70 | od |
71 | fi |
72 | } |
73 | :: atomic { |
74 | (window > 0 && busy[q] == false) -> |
75 | window = window - 1; |
76 | q = (q+1)%M |
77 | } |
78 | #if DUPS |
79 | :: atomic { |
80 | (nfull(f2d) && window > 0 && busy[q] == true) -> |
81 | f2d!O_buf[q],q |
82 | } |
83 | #endif |
84 | :: atomic { |
85 | (timeout && nfull(f2d) && window > 0 && busy[q] == true) -> |
86 | f2d!O_buf[q],q |
87 | } |
88 | /* receiver part */ |
89 | #if LOSS |
90 | :: d2f?type,m /* lose any message */ |
91 | #endif |
92 | :: d2f?type,m -> |
93 | if |
94 | :: atomic { |
95 | (type == ack) -> |
96 | busy[m] = false |
97 | } |
98 | :: atomic { |
99 | (type == sync) -> |
100 | m = 0; |
101 | do |
102 | :: (m < M) -> |
103 | received[m] = 0; |
104 | m = m+1 |
105 | :: (m == M) -> |
106 | break |
107 | od |
108 | }; f2d!sync_ack,0 |
109 | :: (type == sync_ack) -> |
110 | f2s!sync_ack,0 |
111 | :: (type != ack && type != sync && type != sync_ack)-> |
112 | if |
113 | :: atomic { |
114 | (received[m] == true) -> |
115 | x = ((0<p-m && p-m<=W) |
116 | || (0<p-m+M && p-m+M<=W)) }; |
117 | if |
118 | :: (x) -> f2d!ack,m |
119 | :: (!x) /* else skip */ |
120 | fi |
121 | :: atomic { |
122 | (received[m] == false) -> |
123 | I_buf[m] = type; |
124 | received[m] = true; |
125 | received[(m-W+M)%M] = false |
126 | } |
127 | fi |
128 | fi |
129 | :: /* atomic { */ |
130 | (received[p] == true && nfull(f2s) && nfull(f2d)) -> |
131 | f2s!I_buf[p],0; |
132 | f2d!ack,p; |
133 | p = (p+1)%M |
134 | /* } */ |
135 | od |
136 | } |
137 | |
138 | proctype upper_s(chan s2f, f2s0) |
139 | { byte s_state; |
140 | byte type, toggle; |
141 | |
142 | xs s2f; |
143 | xr f2s0; |
144 | |
145 | s2f!sync,toggle; |
146 | do |
147 | :: f2s0?sync_ack,type -> |
148 | if |
149 | :: (type != toggle) |
150 | :: (type == toggle) -> break |
151 | fi |
152 | :: timeout -> |
153 | s2f!sync,toggle |
154 | od; |
155 | toggle = 1 - toggle; |
156 | |
157 | end: do |
158 | :: s2f!white,0 |
159 | :: atomic { |
160 | (s_state == 0 && nfull(s2f)) -> |
161 | s2f!red,0 -> |
162 | s_state = 1 |
163 | } |
164 | :: atomic { |
165 | (s_state == 1 && nfull(s2f)) -> |
166 | s2f!blue,0 -> |
167 | s_state = 2 |
168 | } |
169 | od |
170 | } |
171 | |
172 | proctype upper_r(chan f2s1) |
173 | { byte r_state; |
174 | |
175 | xr f2s1; |
176 | |
177 | do |
178 | :: f2s1?white,0 |
179 | :: f2s1?red,0 -> break |
180 | :: f2s1?blue,0 -> assert(0) |
181 | od; |
182 | |
183 | do |
184 | :: f2s1?white,0 |
185 | :: f2s1?red,0 -> assert(0) |
186 | :: f2s1?blue,0 -> goto end |
187 | od; |
188 | end: |
189 | do |
190 | :: f2s1?white,0 |
191 | :: f2s1?red,0 -> assert(0) |
192 | :: f2s1?blue,0 -> assert(0) |
193 | od |
194 | } |
195 | |
196 | init |
197 | { |
198 | atomic { |
199 | run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]); |
200 | run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]); |
201 | run upper_s(ses_to_flow[0], flow_to_ses[0]); |
202 | run upper_r(flow_to_ses[1]) |
203 | } |
204 | } |