verif/Spin/Test/pftp

   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 }