← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/verbeek-schmaltz/verbeek/instantiations/genoc/simple-ct-global/simple.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/verbeek-schmaltz/verbeek/instantiations/genoc/simple-ct-global/simple.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(begin-book);$ACL2s-Preamble$|#
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
(include-book "make-event/defspec"  :dir :system)
 
7
(include-book "../../routing/XY/XYRouting")
 
8
(include-book "../../departure/simple/simple-R4D")
 
9
(include-book "../../scheduling/circuit-switching-global/circuit")
 
10
(include-book "../../simulation/simple/simple")
 
11
(include-book "../../interfaces/dummy-interfaces/interfaces-computes")
 
12
(include-book "ordinals/lexicographic-ordering" :dir :system)
 
13
(include-book "../../../generic-modules/GeNoC")
 
14
(include-book "sets")
 
15
 
 
16
;;-----------------------------
 
17
;; Defintion of GeNoC
 
18
;;-----------------------------
 
19
 
 
20
 
 
21
; Instantiation of GeNoC with a 2DMesh, XY Routing and packet scheduling,
 
22
; a simple network state (each node has a constant number of buffers)
 
23
; and simple R4D
 
24
(defun simple-genoc_t (missives nodeset measure trlst accup time ntkstate order)
 
25
  ;; the composition of routing and scheduling is built by function genoc_t.
 
26
  ;; it takes as arguments:
 
27
  ;; missives: List of missives
 
28
  ;; nodeset:  NodeSet
 
29
  ;; measure:  The measure that is decreased by the scheduler
 
30
  ;; trlst:    Accumulator of arrived travels
 
31
  ;; accup:    Accumulator of networkstates for simulation
 
32
  ;; time:     Notion of time
 
33
  ;; ntkstate: Network state
 
34
  ;; order:    Ordering
 
35
  ;; it returns:
 
36
  ;; - the arrived messages
 
37
  ;; - the en route messages
 
38
  ;; - the network state accumulator for simulation
 
39
  
 
40
  ;; the measure is set to the measure defined by the scheduler
 
41
  (declare (xargs :measure (acl2-count measure)
 
42
                  :hints (("Goal" :use (:instance ct-measure-decreases
 
43
                                               (trlst (xy-routing-top (mv-nth 1 (inst-readyfordeparture missives nil nil time)) nodeset)))))))
 
44
  (if (endp missives)
 
45
    ;; no more messsages to send
 
46
    (mv trlst nil accup)
 
47
    ;; else
 
48
    (mv-let (delayed departing)
 
49
            ;; call R4D to determine which missives are ready for departure
 
50
            (inst-readyfordeparture missives nil nil time)
 
51
            ;; determine set of routes for all departing missives
 
52
            (let ((v (XY-routing-top departing nodeset)))
 
53
              ;; check if it is possible to schedule
 
54
              (cond ((not (inst-legal-measure measure v nodeset ntkstate order))
 
55
                     ;; illegal measure supplied
 
56
                     (mv trlst missives accup))
 
57
                    ((inst-scheduling-assumptions v nodeset ntkstate order)
 
58
                     ;; schedule and recursivily call genoc_t
 
59
                     (mv-let (newtrlst arrived newmeasure newntkstate)
 
60
                             (inst-scheduling v nodeset ntkstate order)
 
61
                             (simple-genoc_t  (append newtrlst delayed)
 
62
                                              nodeset
 
63
                                              newmeasure
 
64
                                              (append arrived trlst)
 
65
                                              (append accup (list (simple-extract-simulation newntkstate)))
 
66
                                              (+ 1 time)
 
67
                                              newntkstate 
 
68
                                              (inst-get_next_priority order))))
 
69
                    (t
 
70
                     ;; scheduler has instructed to terminate
 
71
                     (mv trlst missives accup)))))))
 
72
 
 
73
 
 
74
; talst     List of transactions
 
75
; p1:       Parameter for generating nodes, a coordinate (X Y)
 
76
; p2:       Parameter for generating ntkstate, isn't used and can be anything
 
77
; order:    Ordering. Isn't used, can be anything
 
78
(defun simple-genoc (talst p1 p2 order)
 
79
  ;; main function
 
80
  (if (simple-ValidStateParamsp p1 p2)
 
81
    (mv-let (responses aborted accup)
 
82
            (simple-genoc_t ;; compute traveling missives
 
83
                            (computetmissives talst)
 
84
                            ;; compute nodeset
 
85
                            (2DMesh-Nodesetgenerator p1)
 
86
                            ;; compute initial measure
 
87
                            (inst-initial-measure (xy-routing-top (computetmissives talst) (2DMesh-Nodesetgenerator p1))
 
88
                                      (2DMesh-Nodesetgenerator p1)
 
89
                                      (inst-generate-initial-ntkstate talst (inst-StateGenerator p1 p2))
 
90
                                      order)
 
91
                            ;; accumulator for arrived travels
 
92
                            nil
 
93
                            ;; accumulator for simulation
 
94
                            nil
 
95
                            ;; time
 
96
                            '0 
 
97
                            ;; compute initial ntkstate
 
98
                            (inst-generate-initial-ntkstate talst (inst-StateGenerator p1 p2))
 
99
                            order)
 
100
            (declare (ignore accup))
 
101
            (mv (computeresults responses) aborted))
 
102
    (mv nil nil)))
 
103
 
 
104
;; non-tail version of first value of genoc: the arrived messages
 
105
(defun simple-genoc_t-nt-mv-nth0 (missives nodeset measure time ntkstate order)
 
106
  (declare (xargs :measure (acl2-count measure)
 
107
                  :hints (("Goal" :use (:instance ct-measure-decreases
 
108
                                               (trlst (xy-routing-top (mv-nth 1 (inst-readyfordeparture missives nil nil time)) nodeset)))))))
 
109
  (if (endp missives)
 
110
    nil
 
111
    (mv-let (delayed departing)
 
112
            (inst-readyfordeparture missives nil nil time)
 
113
            (let ((v (XY-routing-top departing nodeset)))
 
114
              (cond ((not (inst-legal-measure measure v nodeset ntkstate order))
 
115
                     nil)
 
116
                    ((inst-scheduling-assumptions v nodeset ntkstate order)
 
117
                     (mv-let (newtrlst arrived newmeasure newntkstate)
 
118
                             (ct-scheduling v nodeset ntkstate order)
 
119
                           (append
 
120
                             (simple-genoc_t-nt-mv-nth0  (append newtrlst delayed)
 
121
                                                         nodeset
 
122
                                                         newmeasure
 
123
                                                         (+ 1 time)
 
124
                                                         newntkstate 
 
125
                                                         (inst-get_next_priority order))
 
126
 
 
127
                            arrived )))
 
128
                    (t
 
129
                     nil))))))
 
130
;; proof equality between tail and non-tailversion of GeNoC_t
 
131
(defthm simple-genoc_t-nt-mv-nth0=tail-mv-nth0
 
132
  (equal (mv-nth 0 (simple-genoc_t missives nodeset measure trlst accup time ntkstate order))
 
133
         (append (simple-genoc_t-nt-mv-nth0 missives nodeset measure time ntkstate order)
 
134
                 trlst))
 
135
  :hints (("Goal" :in-theory (disable xy-routing-top ct-scheduling))))
 
136
 
 
137
;; non-tail version of second value of genoc: the delayed messages
 
138
(defun simple-genoc_t-nt-mv-nth1 (missives nodeset measure time ntkstate order)
 
139
  (declare (xargs :measure (acl2-count measure)
 
140
                  :hints (("Goal" :use (:instance ct-measure-decreases
 
141
                                               (trlst (xy-routing-top (mv-nth 1 (inst-readyfordeparture missives nil nil time)) nodeset)))))))
 
142
  (if (endp missives)
 
143
    nil
 
144
    (mv-let (delayed departing)
 
145
            (inst-readyfordeparture missives nil nil time)
 
146
            (let ((v (XY-routing-top departing nodeset)))
 
147
              (cond ((not (inst-legal-measure measure v nodeset ntkstate order))
 
148
                     missives)
 
149
                    ((inst-scheduling-assumptions v nodeset ntkstate order)
 
150
                     (mv-let (newtrlst arrived newmeasure newntkstate)
 
151
                             (ct-scheduling v nodeset ntkstate order)
 
152
                             (declare (ignore arrived))
 
153
                             (simple-genoc_t-nt-mv-nth1  (append newtrlst delayed)
 
154
                                                         nodeset
 
155
                                                         newmeasure
 
156
                                                         (+ 1 time)
 
157
                                                         newntkstate 
 
158
                                                         (inst-get_next_priority order))))
 
159
                    (t
 
160
                     missives))))))
 
161
;; proof equality between tail and non-tailversion of GeNoC_t
 
162
(defthm simple-genoc_t-nt-mv-nth1=tail-mv-nth1
 
163
  (equal (mv-nth 1 (simple-genoc_t missives nodeset measure trlst accup time ntkstate order))
 
164
         (simple-genoc_t-nt-mv-nth1 missives nodeset measure time ntkstate order))
 
165
  :hints (("Goal" :in-theory (disable xy-routing-top ct-scheduling))))
 
166
 
 
167
 
 
168
;;----------------------------------------
 
169
;; DEADLOCK FREEDOM FOR CIRCUIT SWITCHING
 
170
;;----------------------------------------
 
171
;; The proof is structured as follows:
 
172
;; 1.) We define a property P which implies deadlockfreedom
 
173
;; 2.) We proof P implies a possible route
 
174
;; 3.) We prove P is preserved by GeNoC, i.e., if
 
175
;;     it holds, then after one GeNoC-cycle it still holds.
 
176
;; 4.) We prove P implies en route is empty, by proving that
 
177
;;     scheduling always provides a legal measure.
 
178
;; 5.) We prove that if en route is empty, then arrived is full.
 
179
;;
 
180
;; Property P is defined as:
 
181
;; (and ---the nodeset doesn't contain nil---
 
182
;;      (not (member-equal nil nodeset))
 
183
;;      ---each node has *num-of-buffers* buffers---
 
184
;;      (buffersize ntkstate *num-of-buffers*)
 
185
;;      ---trlst has no travel whose frm is nil---
 
186
;;      (not (member-equal nil (V-Frms trlst)))
 
187
;;      ---the trlst is created by xy routing---
 
188
;;      (trlst-created-by-xy-routing trlst nodeset)
 
189
;;      ---trlst is a valid travel list---
 
190
;;      (trlstp trlst nodeset)
 
191
;;      ---the nodeset is created by parameter p1---
 
192
;;      (p1-created-ntkstate p1 ntkstate))
 
193
;;      ---the network and trlst relate to each other---
 
194
;;      (n==t ntkstate trlst)
 
195
;;      ---the situation is deadlockfree as defined below
 
196
;;      (deadlockfree 0 trlst ntkstate)
 
197
 
 
198
 
 
199
;;----------------------------------------
 
200
;; DEADLOCK FREEDOM FOR CIRCUIT SWITCHING
 
201
;; 1.) Definitions
 
202
;;----------------------------------------
 
203
 
 
204
;; 1.) Macro's used for convenience
 
205
(defmacro propertyP (trlst nodeset ntkstate p1)
 
206
  `(and (not (member-equal nil ,nodeset))
 
207
        (buffersize ,ntkstate 3)
 
208
        (not (member-equal nil (V-Frms ,trlst)))
 
209
        (trlst-created-by-xy-routing ,trlst ,nodeset)
 
210
        (trlstp trlst nodeset)
 
211
        (p1-created-ntkstate ,p1 ,ntkstate)
 
212
        (n==t ,ntkstate ,trlst)
 
213
        (deadlockfree 0 ,trlst ,ntkstate)))
 
214
;; checks if the node is full in the current ntkstate
 
215
(defmacro full-node (node ntkstate)
 
216
  (list 'not (list 'has-empty-buffer (list 'inst-readbuffers node ntkstate))))
 
217
;; return t iff n is in the range of the length of the list l
 
218
(defmacro in-range (n l)
 
219
  (list 'and (list 'natp n) (list '>= n 0) (list '< n (list 'len l))))
 
220
;; hop1 denotes the first element of the first route
 
221
;; of the first travel of trlst
 
222
(defmacro hop1 (trlst)
 
223
  (list 'caar (list 'RoutesV (list 'car trlst))))#|ACL2s-ToDo-Line|#
 
224
 
 
225
 
 
226
 
 
227
;; 1.) Definition of ntkstate-trlst relation
 
228
;; we assume that the ntkstate and the trlst relate to each
 
229
;; other in the following way: if an entry is full, then
 
230
;; there exists a travel currently in that entry. This
 
231
;; is expressed by (ntkstate-trlst-relate ntkstate trlst)
 
232
 
 
233
;; returns t iff there exists a travel v
 
234
;; in trlst with (FrmV v) = frm and
 
235
;; which is currently in entry
 
236
(defun frm-in-trlst (trlst frm node)
 
237
  (if (endp trlst)
 
238
    nil
 
239
    (if (and (equal (FrmV (car trlst)) frm)
 
240
             (equal (hop1 trlst) node))
 
241
      t
 
242
      (frm-in-trlst (cdr trlst) frm node))))
 
243
;; returns t iff each frame in the buffer is in
 
244
;; trlst
 
245
(defun buffercontents-in-trlst (buffer trlst node)
 
246
  (if (endp buffer)
 
247
    t
 
248
    (if (or (equal (car buffer) nil)
 
249
            (frm-in-trlst trlst (car buffer) node))
 
250
      (buffercontents-in-trlst (cdr buffer) trlst node)
 
251
      nil)))
 
252
;; returns t if all the contents of the entries in ntkstate
 
253
;; are in a travel in trlst
 
254
(defun ntkstate-relates-to-trlst (ntkstate trlst)
 
255
  (if (endp ntkstate)
 
256
    t
 
257
    (let* ((entry (car ntkstate))
 
258
           (buffer (get_buff entry)))
 
259
      (if (and (consp entry)
 
260
               (buffercontents-in-trlst buffer trlst (get_coor entry)))
 
261
        (ntkstate-relates-to-trlst (cdr ntkstate) trlst)
 
262
        nil))))
 
263
;; the following function expresses the previopus relation
 
264
;; in a more convenient way: an ntkstate and trlst relate to
 
265
;; each other if updating the ntkstate with trlst
 
266
;; doesn't change the ntkstate
 
267
(defun n==t (ntkstate trlst)
 
268
  (equal (update-ntkstate ntkstate trlst) ntkstate))
 
269
 
 
270
 
 
271
;; 1.) Definition of trlst-created-by-xy-routing relation
 
272
;; we assume that the routes of trlst have been created by
 
273
;; the currently used routing function, i.e. xy.
 
274
;; This is expressed by the following function.
 
275
(defun trlst-created-by-xy-routing (trlst nodeset)
 
276
  (equal (xy-routing-top (totmissives trlst) nodeset) trlst))
 
277
 
 
278
 
 
279
;; 1.) Definition of buffer size of nodes
 
280
;; returns t if all entries of the ntkstate have
 
281
;; size number of buffers
 
282
(defun buffersize (ntkstate size)
 
283
  (if (endp ntkstate)
 
284
    t
 
285
    (if (equal (len (get_buff (car ntkstate))) size)
 
286
      (buffersize (cdr ntkstate) size)
 
287
      nil)))
 
288
 
 
289
 
 
290
;; 1.) Defintion of p1-created-ntkstate
 
291
;; returns t iff the coordinates of the ntkstate are equal to the
 
292
;; nodeset generated by params
 
293
(defun p1-created-ntkstate (p1 ntkstate)
 
294
  (and (2DMesh-validparamsp p1)
 
295
       (equal (getcoordinates ntkstate) (2DMesh-NodesetGenerator p1))))
 
296
 
 
297
 
 
298
;; 1.) Misc. definitions used in proof
 
299
;; returns t iff ntkstate1 is less or equal full
 
300
;; than ntkstate2
 
301
(defun <=-full (ntkstate1 ntkstate2)
 
302
  (if (endp ntkstate1)
 
303
    t
 
304
    (if (has-empty-buffer (car ntkstate2))
 
305
      (and (has-empty-buffer (car ntkstate1))
 
306
           (<=-full (cdr ntkstate1) (cdr ntkstate2)))
 
307
      (<=-full (cdr ntkstate1) (cdr ntkstate2)))))
 
308
;; returns t if the list of buffers has at least
 
309
;; one full buffer
 
310
(defun E-full-buffer (buffer)
 
311
  (cond ((endp buffer) nil)
 
312
        ((car buffer) t)
 
313
        (t (E-full-buffer (cdr buffer)))))
 
314
;; creates a list of all travels currently in a node
 
315
;; of the route
 
316
(defun get-travels-route (route trlst)
 
317
  (if (endp route)
 
318
    nil
 
319
    (let ((recur (get-travels-route (cdr route) trlst)))
 
320
      (append (get-travels (car route) trlst)
 
321
              recur))))
 
322
;; returns the number of elements in lst2
 
323
;; that are not in lst1
 
324
(defun diff-size (lst1 lst2)
 
325
  (if (endp lst2)
 
326
    0
 
327
    (let ((recur (diff-size lst1 (cdr lst2))))
 
328
      (if (member-equal (car lst2) lst1)
 
329
        recur
 
330
        (nfix (1+ recur))))))
 
331
 
 
332
;; 1.) Definition of deadlockfree
 
333
;; theorems needed to prove termination of
 
334
;; the following function
 
335
(defthm subsetp-get-travels
 
336
  (subsetp (get-travels org trlst) trlst))
 
337
(defthm subsetp-get-travels-route
 
338
  (subsetp (get-travels-route route trlst) trlst))
 
339
(mutual-recursion
 
340
 ;; deadlockfree_v returns nil if the given travel
 
341
 ;; is or will be in deadlockstate and t otherwise.
 
342
 ;;
 
343
 ;; Parameters:
 
344
 ;; v: the travel that is currently checked
 
345
 ;; v-acc: an accumulator of travels already examined
 
346
 ;; trlst: the complete initial trlst
 
347
 ;; ntkstate: the network state
 
348
 ;;
 
349
 ;; A given travel v is deadlockfree if either
 
350
 ;; 1.) each node of the route has empty buffers
 
351
 ;; 2.) the travels that fill the nodes of the route are deadlockfree.
 
352
 ;; If while checking the second condition v must again be checked, a cycle is encountered
 
353
 ;; and thus v is in deadlockstate. Therefor the travels are accumulated in v-acc.
 
354
 ;;
 
355
 ;; From a computational point of view, this function can be much more effective.
 
356
 ;; First, instead of checking al travels in a route with A-deadlockfree_v, it
 
357
 ;; suffices to check if for all nodes in route there exists a travel that is deadlockfree.
 
358
 ;; However, for such function E-deadlockfree_v, we can't prove the needed theorem
 
359
 ;; subsetp-preverves-E-deadlockfree_v, because the witness can be outside the subset.
 
360
 ;; Secondly, it is sufficient to check only full nodes, since a non-full node can't
 
361
 ;; cause deadlock. This would increase complexity of the proof.
 
362
 ;; Thirdly, the function could check, before it enters recursion, whether the rest of
 
363
 ;; the route is free, and not go into recursion if so. Again this would increase
 
364
 ;; complexity of the proof.
 
365
 ;;
 
366
 ;; The measure is a list of four elements, lexicographically compared:
 
367
 ;; it is possible (but shouldn't occur) that v is not in the trlst. However this can occur
 
368
 ;; only with the first call, since get-travels returns travels from trlst (see the previous
 
369
 ;; theorem). The first element is 1 if v is not in trlst, and if so, decreases to 0 after the
 
370
 ;; first call. The same holds for travels of A-deadlockfree_v. Thus for correct input the
 
371
 ;; first element is always 0.
 
372
 ;; The second element decreases on each call of A-deadlockfree_v in deadlockfree_v and remains
 
373
 ;; equal on each call of deadlockfree_v in A-deadlockfree_v.
 
374
 ;; The third element decreases on each call of deadlockfree_v in A-deadlockfree_v.
 
375
 ;; The fourth element is the `self' decreasing measure: for deadlockfree_v this is constant
 
376
 ;; since it's non-recursive. For A-deadlockfree_v this is the length of travels, since this
 
377
 ;; decreases on each self-call.
 
378
 (defun deadlockfree_v (v v-acc trlst ntkstate)
 
379
   (declare (xargs :measure (list (if (member-equal v trlst) 0 1) (diff-size v-acc trlst) 0 0)
 
380
                   :well-founded-relation l<))
 
381
   (let* ((route (car (RoutesV v)))
 
382
          (travels (get-travels-route (cdr route) trlst)))
 
383
     (cond ((member-equal v v-acc)
 
384
            ;; we get into a circle, the route isn't deadlockfree
 
385
            nil)
 
386
           ((has-empty-buffers (cdr route) ntkstate)
 
387
            ;; the travel is possible, thus it is deadlockfree
 
388
            t)
 
389
           (t
 
390
            (A-deadlockfree_v travels (cons v v-acc) trlst ntkstate)))))
 
391
 ;; returns t iff all travels in travels
 
392
 ;; are deadlockfree
 
393
 (defun A-deadlockfree_v (travels v-acc trlst ntkstate)
 
394
   (declare (xargs :measure (list (if (subsetp travels trlst) 0 1) (diff-size v-acc trlst) 1 (len travels))))
 
395
   (if (endp travels)
 
396
     t
 
397
     (and (deadlockfree_v (car travels) v-acc trlst ntkstate)
 
398
          (A-deadlockfree_v (cdr travels) v-acc trlst ntkstate)))))
 
399
 
 
400
;; deadlockfree returns t iff we can prove
 
401
;; deadlockfree_v for the last (len trlst) - n
 
402
;; travels in trlst. In case n = 0, it thus returns
 
403
;; t iff all travels are deadlockfree.
 
404
;;
 
405
;; We can't simply perform recursion on the trlst,
 
406
;; since we need to supply deadlockfree_v with the
 
407
;; complete trlst in each call.
 
408
(defun deadlockfree (n trlst ntkstate)
 
409
  (declare (xargs :measure (nfix (- (len trlst) n))))
 
410
  (cond ((not (natp n))
 
411
         nil)
 
412
        ((not (in-range n trlst))
 
413
         t)
 
414
        (t
 
415
         (and (deadlockfree_v (nth n trlst) nil trlst ntkstate)
 
416
              (deadlockfree (1+ n) trlst ntkstate)))))
 
417
 
 
418
;; some constants to test the function
 
419
;; creates a 3 by 3 mesh, filled as follows:
 
420
;;       x   x   f
 
421
;;       x   x   x
 
422
;;       f   x   x
 
423
;; where x is a node with an empty buffer and
 
424
;; f a node with a full buffer.
 
425
;; For circuit and xy, this is deadlocked.
 
426
(defconst *dimension* '(3 3))
 
427
(defconst *TransactionList* '((0 (0 0) "msg1" (2 0) 1 0)
 
428
                              (1 (0 0) "msg2" (2 0) 1 0)
 
429
                              (2 (0 0) "msg3" (2 0) 1 0)
 
430
                              (3 (2 0) "msg4" (0 0) 1 0)
 
431
                              (4 (2 0) "msg5" (0 0) 1 0)
 
432
                              (5 (2 0) "msg6" (0 0) 1 0)))
 
433
(defconst *Nodeset* (2DMesh-Nodesetgenerator *dimension*))
 
434
(defconst *trlst* (xy-routing-top (computetmissives *Transactionlist*) *nodeset*))
 
435
(defconst *ntkstate* (inst-generate-initial-ntkstate *Transactionlist* (inst-StateGenerator *dimension* nil)))
 
436
;(deadlockfree 0 *trlst* *ntkstate*)
 
437
 
 
438
;; induction scheme that can be used to induct on deadlockfree_v
 
439
(defun deadlockfree_v-inductionscheme (flg v v-acc trlst ntkstate travels)
 
440
  (declare (xargs :measure (list (if flg
 
441
                                   (if (member-equal v trlst) 0 1)
 
442
                                   (if (subsetp travels trlst) 0 1))
 
443
                                 (diff-size v-acc trlst)
 
444
                                 (if flg 0 1)
 
445
                                 (if flg 0 (len travels)))
 
446
                  :well-founded-relation l<))
 
447
  (if flg
 
448
    (let* ((route (car (RoutesV v)))
 
449
           (travels1 (get-travels-route (cdr route) trlst)))
 
450
      (cond ((member-equal v v-acc) nil)
 
451
            ((has-empty-buffers (cdr route) ntkstate) nil)
 
452
            (t
 
453
             (deadlockfree_v-inductionscheme nil v (cons v v-acc) trlst ntkstate travels1))))
 
454
    (cond ((endp travels) nil)
 
455
          ((deadlockfree_v (car travels) v-acc trlst ntkstate)
 
456
           (list (deadlockfree_v-inductionscheme t (car travels) v-acc trlst ntkstate travels)
 
457
                 (deadlockfree_v-inductionscheme nil v v-acc trlst ntkstate (cdr travels))))
 
458
          (t
 
459
           nil))))
 
460
 
 
461
 
 
462
;;----------------------------------------------------------
 
463
;; THEOREM 2: deadlockfree implies that a route is possible
 
464
;;----------------------------------------------------------
 
465
 
 
466
;; update the ntkstate results in a ntkstate-trlst relation
 
467
(defthm buffercontents-cdr
 
468
  (implies (buffercontents-in-trlst buffer (cdr trlst) node)
 
469
           (buffercontents-in-trlst buffer trlst node)))
 
470
(defthm ntkstate-relates-updated-ntkstate
 
471
  (implies (n==t ntkstate trlst)
 
472
           (ntkstate-relates-to-trlst ntkstate trlst)))
 
473
 
 
474
;; a route without full nodes implies that a route is possible
 
475
(defthm has-empty-buffers-implies-route-possible
 
476
  (implies (and (trlstp trlst nodeset)
 
477
                (has-empty-buffers (cdar (RoutesV v)) ntkstate)
 
478
                (member-equal v trlst))
 
479
           (not (no-good-routes trlst ntkstate))))
 
480
(defthm buffer-implies-travels
 
481
  (implies (and (buffercontents-in-trlst buffer trlst node)
 
482
                (E-full-buffer buffer))
 
483
           (consp (get-travels node trlst))))
 
484
(defthm full-node-implies-travels
 
485
  (implies (and (full-node node ntkstate)
 
486
                (buffersize ntkstate 3)
 
487
                (ntkstate-relates-to-trlst ntkstate trlst)
 
488
                (member-equal node (getcoordinates ntkstate)))
 
489
           (consp (get-travels node trlst)))
 
490
  :hints (("Subgoal *1/2" 
 
491
           :use (:instance buffer-implies-travels (node (get_coor (car ntkstate)))
 
492
                 (buffer (get_buff (car ntkstate)))))))
 
493
(defthm non-empty-route-implies-travels-in-route
 
494
  (implies (and (ntkstate-relates-to-trlst ntkstate trlst)
 
495
                (buffersize ntkstate 3)
 
496
                (subsetp route (getcoordinates ntkstate))
 
497
                (not (has-empty-buffers route ntkstate)))
 
498
           (consp (get-travels-route route trlst)))
 
499
  :hints (("Goal" :in-theory (disable has-empty-buffer))))
 
500
;; thanks to this theorem, trlstp can be disabled in
 
501
;; the following proof
 
502
(defthm trlstp-implies-subsetp-route
 
503
  (implies (and (trlstp trlst nodeset)
 
504
                (member-equal v trlst))
 
505
           (subsetp (cdar (RoutesV v)) nodeset)))
 
506
;; use induction scheme to prove deadlockfree_v returns a route that is free
 
507
(defthm deadlockfree_v-implies-route-possible-flg
 
508
  (if flg
 
509
    (let ((v1 (deadlockfree_v v v-acc trlst ntkstate)))
 
510
      (implies (and v1
 
511
                    (buffersize ntkstate 3)
 
512
                (ntkstate-relates-to-trlst ntkstate trlst)
 
513
                    (member-equal v trlst)
 
514
                    (trlstp trlst (getcoordinates ntkstate)))
 
515
               (not (no-good-routes trlst ntkstate))))
 
516
    (let ((v1 (A-deadlockfree_v travels v-acc trlst ntkstate)))
 
517
      (implies (and v1
 
518
                    (buffersize ntkstate 3)
 
519
                    (ntkstate-relates-to-trlst ntkstate trlst)
 
520
                    (subsetp travels trlst)
 
521
                    (trlstp trlst (getcoordinates ntkstate))
 
522
                    (consp travels))
 
523
               (not (no-good-routes trlst ntkstate)))))
 
524
    :rule-classes nil
 
525
  :hints (("Goal" :induct (deadlockfree_v-inductionscheme flg v v-acc trlst ntkstate travels)
 
526
                  :in-theory (disable trlstp routesv))))
 
527
(defthm deadlockfree_v-implies-route-possible
 
528
  (let ((v1 (deadlockfree_v v v-acc trlst ntkstate)))
 
529
    (implies (and v1
 
530
                  (buffersize ntkstate 3)
 
531
                  (ntkstate-relates-to-trlst ntkstate trlst)
 
532
                  (trlstp trlst (getcoordinates ntkstate))
 
533
                  (member-equal v trlst))
 
534
             (not (no-good-routes trlst ntkstate))))
 
535
  :hints (("Goal" :use (:instance deadlockfree_v-implies-route-possible-flg (flg t)))))
 
536
;; first proof by induction that if the nth cdr
 
537
;; from trlst is deadlockfree then there is a possible route
 
538
(defthm nth-cdr-deadlockfree-implies-route-possible
 
539
  (implies (and (consp trlst)
 
540
                (buffersize ntkstate 3)
 
541
                (ntkstate-relates-to-trlst ntkstate trlst)
 
542
                (trlstp trlst (getcoordinates ntkstate))
 
543
                (deadlockfree n trlst ntkstate)
 
544
                (in-range n trlst))
 
545
           (not (no-good-routes trlst ntkstate)))
 
546
  :hints (("Subgoal *1/4" :use ((:instance deadlockfree_v-implies-route-possible
 
547
                                 (v (nth n trlst)) (v-acc nil))))))
 
548
 
 
549
;; Theorem 2 is an instantiation of the previous theorem with n = 0
 
550
;; All assumptions are part of property P
 
551
(defthm deadlockfree-implies-route-possible
 
552
  (implies (and (consp trlst)
 
553
                (buffersize ntkstate 3)
 
554
                (n==t ntkstate trlst)
 
555
                (trlstp trlst (getcoordinates ntkstate))
 
556
                (deadlockfree 0 trlst ntkstate))
 
557
           (not (no-good-routes trlst ntkstate)))
 
558
  :hints (("Goal" :use (:instance nth-cdr-deadlockfree-implies-route-possible (n 0)))))
 
559
 
 
560
 
 
561
;;---------------------------------------------
 
562
;; THEOREM 3: Property P is preserved by GeNoC
 
563
;;---------------------------------------------
 
564
;; Proof: that (getcoordinates ntkstate) equals (getcoordinates newntkstate)
 
565
(defthm update-preserves-coor
 
566
  (equal (getcoordinates (update-ntkstate ntkstate trlst))
 
567
         (getcoordinates ntkstate)))
 
568
(defthm scheduling-preserves-coor
 
569
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
570
         (newntkstate (mv-nth 3 out)))
 
571
     (equal (getcoordinates newntkstate)
 
572
            (getcoordinates ntkstate))))
 
573
 
 
574
;; Proof: (buffersize ntkstate n) is preserved
 
575
(defthm update-preserves-buffersize
 
576
  (implies (buffersize ntkstate *num-of-buffers*)
 
577
           (buffersize (update-ntkstate ntkstate trlst) *num-of-buffers*)))
 
578
(defthm scheduling-preserves-buffersize
 
579
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
580
         (newntkstate (mv-nth 3 out)))
 
581
    (implies (buffersize ntkstate *num-of-buffers*)
 
582
             (buffersize newntkstate *num-of-buffers*))))
 
583
 
 
584
;; Proof: (not (member-equal nil (v-frms trlst))) is preserved
 
585
(defthm scheduler-preserves-v-frms
 
586
  (let ((newtrlst (ct-scheduler-nt-car trlst prev ntkstate)))
 
587
    (implies (not (member-equal frm (V-Frms trlst)))
 
588
             (not (member-equal frm (V-Frms newtrlst))))))
 
589
(defthm routing-preserves-v-frms
 
590
  (let ((newtrlst (xy-routing-top (totmissives trlst) nodeset)))
 
591
    (implies (not (member-equal frm (V-Frms trlst)))
 
592
             (not (member-equal frm (V-Frms newtrlst))))))
 
593
(defthm mv-nth-equals-car
 
594
  (implies (true-listp lst)
 
595
           (equal (mv-nth 0 lst)
 
596
                  (car lst))))
 
597
(defthm scheduling-preserves-v-frms
 
598
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
599
         (newtrlst (xy-routing-top (car out) nodeset)))
 
600
    (implies (not (member-equal frm (V-Frms trlst)))
 
601
             (not (member-equal frm (V-Frms newtrlst))))))
 
602
 
 
603
 
 
604
;; Proof: the routing remains the same for the delayed travels
 
605
;; Assume trlst is created by xy. If a.) newtrlst is a subset of trlst,
 
606
;; and b.) taking a subset preserves created-by-xy,
 
607
;; then newtrlst is created by xy as well.
 
608
 
 
609
;; A.)
 
610
(defthm scheduled-is-subsetp
 
611
  (let ((newtrlst (ct-scheduler-nt-car trlst prev ntkstate)))
 
612
    (subsetp newtrlst trlst)))
 
613
 
 
614
;; B.)
 
615
(defthm remove-twice-xyrouting
 
616
           (equal (xyrouting (car (xyrouting current to))
 
617
                             (car (last (xyrouting current to))))
 
618
                  (xyrouting current to)))
 
619
(defthm remove-twice-xy-routing-top
 
620
           (equal (xy-routing-top (totmissives (xy-routing-top missives nodeset)) nodeset)
 
621
                  (xy-routing-top missives nodeset)))
 
622
(defthm travel-from-xy-routing-list
 
623
  (implies (and (member-equal (car newtrlst) trlst)
 
624
                (trlst-created-by-xy-routing trlst nodeset))
 
625
           (equal (cons (list (caar newtrlst) (nth 1 (car newtrlst)) (nth 2 (car newtrlst))
 
626
                              (list (xyrouting (caar (nth 3 (car newtrlst)))
 
627
                                               (car (last (car (nth 3 (car newtrlst)))))))
 
628
                              (nth 4 (car newtrlst)) (nth 5 (car newtrlst)))
 
629
                        (cdr newtrlst))
 
630
            newtrlst)))
 
631
(defthm subsetp-preserves-created-by-xy
 
632
  (implies (and (subsetp newtrlst trlst)
 
633
                (true-listp newtrlst)
 
634
                (trlst-created-by-xy-routing trlst nodeset))
 
635
           (trlst-created-by-xy-routing newtrlst nodeset))
 
636
  :hints (("Subgoal *1/1" :use (:instance travel-from-xy-routing-list))))
 
637
;; Combing A.) and B.)
 
638
(defthm scheduler-preserves-created-by-xy
 
639
  (let ((newtrlst (ct-scheduler-nt-car trlst nil ntkstate)))
 
640
    (implies (trlst-created-by-xy-routing trlst nodeset)
 
641
             (trlst-created-by-xy-routing newtrlst nodeset)))
 
642
  :hints (("Goal" :use (:instance subsetp-preserves-created-by-xy (newtrlst (ct-scheduler-nt-car trlst nil ntkstate))))))
 
643
(defthm created-by-xy-xy
 
644
  (trlst-created-by-xy-routing (xy-routing-top trlst nodeset) nodeset))
 
645
 
 
646
 
 
647
;; Proof: (trlstp trlst nodeset) is preserved
 
648
;; this is done using proof obligations
 
649
(defthm scheduling-preserves-trlstp
 
650
    (let* ((nodeset (getcoordinates ntkstate))
 
651
           (out (inst-scheduling trlst nodeset ntkstate order))
 
652
           (newtrlst (car out)))
 
653
    (implies (and (p1-created-ntkstate params ntkstate)
 
654
                  (trlstp trlst nodeset))
 
655
             (trlstp (xy-routing-top newtrlst nodeset) nodeset)))
 
656
    :hints (("Goal" :in-theory (e/d (p1-created-ntkstate)
 
657
                                    (totmissives trlstp 2DMesh-Nodesetgenerator xy-routing-top
 
658
                                     2dmesh-validparamsp totmissives)))))
 
659
 
 
660
 
 
661
;; Proof: (p1-created-ntkstate p1 ntkstate) is preserved
 
662
(defthm scheduling-preserves-nodeset-parameter
 
663
      (let* ((nodeset (getcoordinates ntkstate))
 
664
             (out (inst-scheduling trlst nodeset ntkstate order))
 
665
             (newntkstate (mv-nth 3 out)))
 
666
        (implies (p1-created-ntkstate p1 ntkstate)
 
667
                 (p1-created-ntkstate p1 newntkstate)))
 
668
      :hints (("Goal" :in-theory (enable p1-created-ntkstate))))
 
669
 
 
670
 
 
671
;; Proof: (n==t ntkstate trlst) is preserved
 
672
(defthm remove-twice-update-ntkstate
 
673
  (implies (and (trlstp trlst2 nodeset)
 
674
                (not (member-equal nil nodeset)))
 
675
           (equal (update-ntkstate (update-ntkstate ntkstate trlst1) trlst2)
 
676
                  (update-ntkstate ntkstate trlst2))))
 
677
(defthm genoc-preserves-n==t
 
678
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
679
         (newntkstate (mv-nth 3 out))
 
680
         (newtrlst (xy-routing-top (car out) nodeset)))
 
681
    (implies (and (trlstp trlst nodeset)
 
682
                  (not (member-equal nil nodeset))
 
683
                  (trlst-created-by-xy-routing trlst nodeset)
 
684
                  (n==t ntkstate trlst))
 
685
             (n==t newntkstate newtrlst)))
 
686
  :hints (("Goal" :in-theory (disable trlstp))
 
687
          ("Subgoal 1" :use ((:instance remove-twice-update-ntkstate
 
688
                              (trlst1 (ct-scheduler-nt-car TrLst nil ntkstate))
 
689
                              (trlst2 (ct-scheduler-nt-car TrLst nil ntkstate)))
 
690
                              (:instance scheduler-preserves-created-by-xy)))))
 
691
 
 
692
 
 
693
;; Proof: (deadlockfree 0 ntrlst ntkstate) is preserved
 
694
;; We proof this theorem by first proving A.) it holds for an
 
695
;; abstraction of the ntkstate and trlst and then B.) that the
 
696
;; abstract properties hold for the output of the scheduler.
 
697
;; We abstract on the new ntkstate by using only
 
698
;; the property that it is 'less or equal full' than
 
699
;; the old one:
 
700
;; if an entry has an empty buffer then that is preserved.
 
701
;; We abstract on the new trlst by using only
 
702
;; the property that it is a subset of the old one.
 
703
;; This last abstraction holds for the global version
 
704
;; of circuit scheduling only.
 
705
 
 
706
;; A.) the abstraction preserves deadlockfreedom
 
707
(defthm <=-full-preserves-has-empty-buffers
 
708
  (implies (and (<=-full newntkstate ntkstate)
 
709
                (equal (getcoordinates ntkstate) (getcoordinates newntkstate))
 
710
                (has-empty-buffers route ntkstate))
 
711
           (has-empty-buffers route newntkstate)))
 
712
;; the following theorem can only be proven if we now
 
713
;; for all travels that they are deadlockfree, instead
 
714
;; of that we merely know there exists a deadlockfree
 
715
;; travel
 
716
(defthm subsetp-preverves-A-deadlockfree_v
 
717
  (implies (and (subsetp newtravels travels)
 
718
                (A-deadlockfree_v travels v-acc trlst ntkstate))
 
719
           (A-deadlockfree_v newtravels v-acc trlst ntkstate)))  
 
720
(defthm member-equal-get-travels
 
721
  (implies (member-equal v trlst)
 
722
           (member-equal v (get-travels (caar (RoutesV v)) trlst))))
 
723
(defthm subsetp-trlst-get-travels
 
724
  (implies (subsetp newtrlst trlst)
 
725
           (subsetp (get-travels node newtrlst) (get-travels node trlst)))
 
726
  :hints (("Subgoal *1/3" :in-theory (disable routesv))))
 
727
(defthm subsetp-append-subsets
 
728
  (implies (and (subsetp lst1 lst2)
 
729
                (subsetp lst3 lst4))
 
730
           (subsetp (append lst1 lst3) (append lst2 lst4))))
 
731
(defthm subsetp-trlst-get-travels-route
 
732
  (implies (and (subsetp newtrlst trlst))
 
733
           (subsetp (get-travels-route route newtrlst) (get-travels-route route trlst))))
 
734
;; use induction scheme to prove that deadlockfree_v is
 
735
;; preserved by the abstraction
 
736
(defthm abstraction-preserves-deadlockfree_v-flg
 
737
  (implies (and (subsetp newtrlst trlst)
 
738
                (equal (getcoordinates ntkstate) (getcoordinates newntkstate))
 
739
                (<=-full newntkstate ntkstate))
 
740
           (if flg
 
741
             (implies (deadlockfree_v v v-acc trlst ntkstate)
 
742
                      (deadlockfree_v v v-acc newtrlst newntkstate))
 
743
             (implies (A-deadlockfree_v travels v-acc trlst ntkstate)
 
744
                      (A-deadlockfree_v travels v-acc newtrlst newntkstate))))
 
745
  :rule-classes nil
 
746
  :hints (("Goal" :induct (deadlockfree_v-inductionscheme flg v v-acc trlst ntkstate travels))
 
747
          ("Subgoal *1/3" :use ((:instance subsetp-preverves-A-deadlockfree_v
 
748
                                 (newtravels (get-travels-route (cdar (nth 3 v)) newtrlst))
 
749
                                 (travels (get-travels-route (cdar (nth 3 v)) trlst))
 
750
                                 (v-acc (cons v v-acc))
 
751
                                 (trlst newtrlst)
 
752
                                 (ntkstate newntkstate))))))
 
753
(defthm abstraction-preserves-deadlockfree_v
 
754
  (implies (and (subsetp newtrlst trlst)
 
755
                (equal (getcoordinates ntkstate) (getcoordinates newntkstate))
 
756
                (<=-full newntkstate ntkstate)
 
757
                (deadlockfree_v v v-acc trlst ntkstate))
 
758
           (deadlockfree_v v v-acc newtrlst newntkstate))
 
759
  :hints (("Goal" :use (:instance abstraction-preserves-deadlockfree_v-flg (flg t)))))
 
760
 
 
761
;; prove relation between deadlockfree_v and deadlockfree:
 
762
;; (deadlockfree 0 trlst ntkstate)
 
763
;; implies that for all travels deadlockfree_v
 
764
;; holds with the default parameters.
 
765
;; First prove it by induction on n, then
 
766
;; instantiate n with 0.
 
767
(defthm not-in-cdr-implies-equal-to-car
 
768
  (implies (and (natp n)
 
769
                (member-equal x (nthcdr n lst))
 
770
                (not (member-equal x (nthcdr (1+ n) lst))))
 
771
           (equal (nth n lst) x)))
 
772
(defthm member-equal-nth-element
 
773
  (implies (and (in-range n lst1)
 
774
                (subsetp lst1 lst2))
 
775
           (member-equal (nth n lst1) lst2)))
 
776
(defthm nth-cdr-deadlockfree-vs-deadlockfree_v
 
777
  (implies (and (deadlockfree n trlst ntkstate)
 
778
                (member-equal v (nthcdr n trlst)))
 
779
           (deadlockfree_v v nil trlst ntkstate)))
 
780
(defthm deadlockfree-vs-deadlockfree_v
 
781
  (implies (and (deadlockfree 0 trlst ntkstate)
 
782
                (member-equal v trlst))
 
783
           (deadlockfree_v v nil trlst ntkstate))
 
784
  :hints (("Goal" :use (:instance nth-cdr-deadlockfree-vs-deadlockfree_v (n 0)))))
 
785
;; the abstract version of the theorem:
 
786
;; the abstraction preserves deadlockfree
 
787
;; up to the nth cdr of the new trlst
 
788
(defthm abstraction-preserves-deadlockfree-nth-cdr
 
789
  (implies (and (subsetp newtrlst trlst)
 
790
                (equal (getcoordinates ntkstate) (getcoordinates newntkstate))
 
791
                (<=-full newntkstate ntkstate)
 
792
                (deadlockfree 0 trlst ntkstate)
 
793
                (in-range n newtrlst))
 
794
           (deadlockfree n newtrlst newntkstate)))
 
795
 
 
796
 
 
797
;; B.) the scheduler output is a concrete version
 
798
;;     of the abstraction
 
799
;; We already know that newtrlst is a subset of trlst.
 
800
;; Since newntkstate is obtained by updating ntkstate with
 
801
;; newtrlst, it suffices to proof that a ntkstate-update
 
802
;; with a smaller trlst results in a ntkstate that is lesser
 
803
;; or equal full. This holds only if the original ntkstate
 
804
;; relates to the original trlst, i.e. (n==t ntkstate trlst).
 
805
;; We use the book "sets" here.
 
806
(defthm frms-member-equal-nil-create-buffer
 
807
  (implies (and (natp n)
 
808
                (< (len travels) n))
 
809
           (member-equal nil (create-buffer n travels))))
 
810
(defthm create-buffer-frms<n
 
811
  (implies (and (not (member-equal nil (v-frms travels)))
 
812
                (member-equal nil (create-buffer n travels))
 
813
                (natp n))
 
814
           (< (len travels) n)))
 
815
(defthm len-remove-dups
 
816
  (implies (<= (len x) (len (remove-duplicates-equal y)))
 
817
           (<= (len x) (len y))))
 
818
(defthm subsetp-remove-dups
 
819
  (implies (subsetp x y)
 
820
           (subsetp x (remove-duplicates-equal y))))
 
821
(defthm <-and-<=-imply-<
 
822
  (implies (and (< x y)
 
823
                (<= z x))
 
824
           (< z y)))
 
825
(defthm member-equal-nil-create-buffer
 
826
  (implies (and (subsetp travels1 travels2)
 
827
                (<= (len travels1) (len travels2))
 
828
                (no-duplicatesp travels1)
 
829
                (natp n)
 
830
                (not (member-equal nil (v-frms travels2)))
 
831
                (member-equal nil (create-buffer n travels2)))
 
832
           (member-equal nil (create-buffer n travels1)))
 
833
  :hints (("Goal" :use  (:instance <-and-<=-imply-< (x (len travels2)) (y n) (z (len travels1))))))
 
834
(defthm get-travels-preserves-frms
 
835
  (implies (not (member-equal frm (V-Frms trlst)))
 
836
           (not (member-equal frm (V-Frms (get-travels node trlst))))))
 
837
(defthm get-travels-preserves-not-member
 
838
  (implies (not (member-equal v trlst))
 
839
           (not (member-equal v (get-travels node trlst)))))
 
840
(defthm get-travels-preserves-no-duplicatesp
 
841
  (implies (no-duplicatesp-equal trlst)
 
842
           (no-duplicatesp-equal (get-travels node trlst))))
 
843
(defthm subsetp-newtrlst-implies-<=-full
 
844
  (implies (and (not (member-equal nil (V-Frms trlst)))
 
845
                (subsetp newtrlst trlst)
 
846
                (no-duplicatesp newtrlst))
 
847
          (<=-full (update-ntkstate ntkstate newtrlst)
 
848
                   (update-ntkstate ntkstate trlst)))
 
849
  :hints (("Subgoal *1/2" :use (:instance member-equal-nil-create-buffer
 
850
                                (travels1 (get-travels (cadaar ntkstate) newtrlst))
 
851
                                (travels2 (get-travels (cadaar ntkstate) trlst))
 
852
                                (n *num-of-buffers*)))))
 
853
(defthm no-duplicatesp-trlst
 
854
  (implies (no-duplicatesp-equal (v-ids trlst))
 
855
           (no-duplicatesp-equal trlst))
 
856
  :hints (("Subgoal *1/2" :use (:instance member-equal-idv-v-ids
 
857
                                (v (car trlst)) (trlst (cdr trlst))))))
 
858
(defthm scheduled-is-<=-full
 
859
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
860
         (newntkstate (mv-nth 3 out)))
 
861
    (implies (and (trlstp trlst nodeset)
 
862
                  (not (member-equal nil nodeset))
 
863
                  (not (member-equal nil (V-Frms trlst)))
 
864
                  (n==t ntkstate trlst))
 
865
             (<=-full newntkstate ntkstate)))
 
866
  :hints (("Subgoal 1" :use ((:instance subsetp-newtrlst-implies-<=-full
 
867
                              (newtrlst (ct-scheduler-nt-car TrLst nil ntkstate)))))))
 
868
           
 
869
 
 
870
;; A.) + B.)
 
871
;; Then prove an instantiation of the abstract theorem with n = 0
 
872
;; and with newntkstate and newtrlst as provided by the scheduler
 
873
(defthm scheduler-preserves-deadlockfreedom
 
874
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
875
         (newntkstate (mv-nth 3 out))
 
876
         (newtrlst (ct-scheduler-nt-car trlst prev ntkstate)))
 
877
    (implies (and (trlstp trlst nodeset)
 
878
                  (not (member-equal nil nodeset))
 
879
                  (not (member-equal nil (V-Frms trlst)))
 
880
                  (n==t ntkstate trlst)
 
881
                  (deadlockfree 0 trlst ntkstate))
 
882
             (deadlockfree 0 newtrlst newntkstate)))
 
883
  :hints (("Goal" :use ((:instance abstraction-preserves-deadlockfree-nth-cdr
 
884
                         (newntkstate (mv-nth 3 (ct-scheduling trlst nodeset ntkstate order)))
 
885
                         (newtrlst (ct-scheduler-nt-car trlst prev ntkstate))
 
886
                         (n 0)))
 
887
                  :in-theory (disable ct-scheduling n==t trlstp))))
 
888
 
 
889
;; Now that is has been proven that scheduler preserves dlf,
 
890
;; prove that new routing on the delayed travels preserves dlf.
 
891
(defthm genoc-preserves-deadlockfreedom
 
892
  (let* ((nodeset (getcoordinates ntkstate))
 
893
         (out (inst-scheduling trlst nodeset ntkstate order))
 
894
         (newntkstate (mv-nth 3 out))
 
895
         (newtrlst (xy-routing-top (car out) nodeset)))
 
896
    (implies (and (trlstp trlst nodeset)
 
897
                  (not (member-equal nil nodeset))
 
898
                  (not (member-equal nil (V-Frms trlst)))
 
899
                  (n==t ntkstate trlst)
 
900
                  (trlst-created-by-xy-routing trlst nodeset)
 
901
                  (deadlockfree 0 trlst ntkstate))
 
902
             (deadlockfree 0 newtrlst newntkstate)))
 
903
  :otf-flg t
 
904
  :hints (("Goal" :in-theory (disable xy-routing-top ct-scheduling-assumptions ct-legal-measure
 
905
                                      ct-test_routes trlstp scheduler-preserves-deadlockfreedom
 
906
                                      scheduler-preserves-created-by-xy))
 
907
          ("Subgoal 2" :in-theory (e/d (trlst-created-by-xy-routing)
 
908
                                       (scheduler-preserves-deadlockfreedom scheduler-preserves-created-by-xy))
 
909
                       :use ((:instance scheduler-preserves-deadlockfreedom
 
910
                              (prev nil) (nodeset (getcoordinates ntkstate)))
 
911
                              (:instance scheduler-preserves-created-by-xy
 
912
                               (nodeset (getcoordinates ntkstate)))))))
 
913
 
 
914
 
 
915
 
 
916
;;-------------------------------------------------
 
917
;; THEOREM 4: Property P implies en route is empty
 
918
;;-------------------------------------------------
 
919
 
 
920
;; proof output of scheduler is legal measure
 
921
(defthm measure-is-routelengths
 
922
  (equal (sum-of-lst (RouteLengths-TrLst (ct-scheduler-nt-car trlst prev ntkstate)))
 
923
         (sum-of-lst (ct-scheduler-nt-mv2 TrLst prev ntkstate))))
 
924
(defthm scheduling-provides-legal-measure
 
925
  (let* ((out (inst-scheduling trlst nodeset ntkstate order))
 
926
         (newntkstate (mv-nth 3 out))
 
927
         (newmeasure (mv-nth 2 out))
 
928
         (newtrlst (xy-routing-top (car out) nodeset)))
 
929
    (implies (and (inst-scheduling-assumptions trlst nodeset ntkstate order)
 
930
                  (trlst-created-by-xy-routing trlst nodeset))
 
931
             (ct-legal-measure newmeasure newtrlst nodeset newntkstate order)))
 
932
  :hints (("Goal" :in-theory (e/d (trlst-created-by-xy-routing)
 
933
                                  (scheduler-preserves-created-by-xy))
 
934
                  :use (:instance scheduler-preserves-created-by-xy))))
 
935
 
 
936
;; we need the following theorem because otherwise
 
937
;; we would have to enable trlstp in theorem 4
 
938
(defthm routing-append-nil
 
939
  (equal (xy-routing-top (append trlst nil) nodeset)
 
940
         (xy-routing-top trlst nodeset)))
 
941
(defthm consp-routing
 
942
  (implies (consp missives)
 
943
           (consp (xy-routing-top missives nodeset))))
 
944
        
 
945
;; Theorem 4:
 
946
;; If the measure initially supplied to GeNoC_t is legal,
 
947
;; Property P implies that GeNoC terminates with no
 
948
;; en route messages
 
949
(defthm en-route-empty
 
950
  (let* ((nodeset (getcoordinates ntkstate))
 
951
         (trlst (XY-routing-top missives nodeset)))
 
952
    (implies (and (propertyP trlst nodeset ntkstate p1)
 
953
                  (inst-legal-measure measure trlst nodeset ntkstate order))
 
954
             (endp (mv-nth 1 (simple-genoc_t missives nodeset measure nil nil time ntkstate order)))))
 
955
  :hints (("Goal" :in-theory (disable XY-routing-top p1-created-ntkstate deadlockfree ct-scheduling
 
956
                                      ct-legal-measure trlstp n==t))))
 
957
 
 
958
;;-------------------------------------------------
 
959
;; THEOREM 5: If en route is empty, all travels
 
960
;; have arrived.
 
961
;;-------------------------------------------------
 
962
 
 
963
(defthm trlst-equal-routing-missives
 
964
  (trlst-equal (xy-routing-top missives nodeset)
 
965
               missives))
 
966
(defthm missives-equal-enroute+arrived
 
967
  (implies (true-listp missives)
 
968
           (trlst-equal (append (simple-genoc_t-nt-mv-nth0 missives nodeset measure time ntkstate order)
 
969
                                (simple-genoc_t-nt-mv-nth1 missives nodeset measure time ntkstate order))
 
970
                        missives))
 
971
  :hints (("Goal" :in-theory (disable XY-routing-top ct-scheduling trlst-equal))
 
972
          ("Subgoal *1/4" :use (:instance input=output (trlst (xy-routing-top missives nodeset))))))
 
973
 
 
974
(defthm trlst-equal-append-nil
 
975
  (implies (endp y)
 
976
           (trlst-equal (append x y) x))
 
977
  :rule-classes :rewrite)
 
978
 
 
979
 
 
980
(defthm enroute-empty->arrived-full
 
981
  (implies (and (true-listp missives)
 
982
                (endp (mv-nth 1 (simple-genoc_t missives nodeset measure nil nil time ntkstate order))))
 
983
           (trlst-equal (mv-nth 0 (simple-genoc_t missives nodeset measure nil nil time ntkstate order))
 
984
                  missives))
 
985
    :hints (("Goal" :in-theory (disable XY-routing-top ct-scheduling trlst-equal)
 
986
                    :use ((:instance trlst-equal-append-nil
 
987
                           (x (simple-genoc_t-nt-mv-nth0 missives nodeset measure time ntkstate order))
 
988
                           (y (simple-genoc_t-nt-mv-nth1 missives nodeset measure time ntkstate order)))
 
989
                          (:instance missives-equal-enroute+arrived)))))
 
990
 
 
991
;;----------------------
 
992
;; PROVING CORRECTNESS
 
993
;;----------------------
 
994
(defthm simple-genoc-is-correct
 
995
  (let ((nodeset (2dMesh-NodesetGenerator p1)))
 
996
    (mv-let (results aborted)
 
997
            (simple-genoc trs p1 p2 order)
 
998
            (declare (ignore aborted))
 
999
            (implies (and (transactionsp trs nodeset)
 
1000
                          (inst-ValidStateParamsp p1 p2))
 
1001
                     (genoc-correctness results
 
1002
                                        (extract-sublst trs (r-ids results))))))
 
1003
  :otf-flg t
 
1004
  :hints (("goal":by 
 
1005
                 (:functional-instance genoc-is-correct
 
1006
                  (generate-initial-ntkstate simple-generate-initial-ntkstate)
 
1007
                  (readyfordeparture simple-readyfordeparture)
 
1008
                  (genoc simple-genoc)
 
1009
                  (genoc_t simple-genoc_t)
 
1010
                  (validstateparamsp simple-ValidStateParamsp)
 
1011
                  (stategenerator simple-StateGenerator)
 
1012
                  (readbuffers simple-readbuffers)
 
1013
                  (nodesetgenerator 2DMesh-NodeSetGenerator)
 
1014
                  (extract-simulation simple-extract-simulation)
 
1015
                  (loadbuffers simple-loadbuffers)
 
1016
                  (validparamsp 2DMesh-ValidParamsp)
 
1017
                  (nodesetp 2DMesh-NodeSetp)
 
1018
                  (scheduling ct-scheduling)
 
1019
                  (routing XY-Routing-top)
 
1020
                  (get_next_priority ct-get_next_priority)
 
1021
                  (scheduling-assumptions ct-scheduling-assumptions)
 
1022
                  (legal-measure ct-legal-measure)
 
1023
                  (initial-measure ct-initial-measure))
 
1024
                 :in-theory (disable trlstp))
 
1025
 
 
1026
; Comment from J Moore for changes after v5-0 for tau:
 
1027
 
 
1028
; This comment contains (:executable-counterpart tau-system) just so that rune
 
1029
; is a reliable marker for changes made to support tau.  These have had to be 
 
1030
; renamed so often (with changes in tau) that I have lost track of what they
 
1031
; used to be!  Just don't be surprised if this proof fails after changing tau!
 
1032
 
 
1033
; However, an earlier version of this file had these notes:
 
1034
;         ("Subgoal 32" ; tau on: {"Subgoal 32"} tau off: {"Subgoal 34"}
 
1035
;          :in-theory (disable ct-scheduling xy-routing-top))
 
1036
;         ("Subgoal 25" ; tau on: {"Subgoal 25"} tau off: {"Subgoal 26"}
 
1037
;          :in-theory (disable ct-scheduling ct-scheduling-assumptions xy-routing-top
 
1038
;                              simple-extract-simulation))
 
1039
;         ("Subgoal 27" ; tau on: {"Subgoal 27"} tau off: {"Subgoal 28"}
 
1040
;          :use (:instance CorrectRoutesp-XYRouting (tmissives m)))
 
1041
;         ("Subgoal 26" ; tau on: {"Subgoal 26"} tau off: {"Subgoal 27"}
 
1042
;          :use (:instance TrLstp-XYRouting (tmissives m)))
 
1043
;         ("Subgoal 13.2'" :use (:instance not-in-v-ids-ct (prev nil)))
 
1044
;         ("subgoal 10" :in-theory (disable consp-last trlstp))
 
1045
;         ("subgoal 10.2" :in-theory (e/d (trlstp) (consp-last)))
 
1046
;         ("subgoal 10.1" :use ((:instance tm-ids-tomissives-v-ids (x trlst))
 
1047
;                               (:instance tomissives-extract-sublst
 
1048
;                                          (l (totmissives trlst))
 
1049
;                                          (ids (tm-ids (totmissives trlst))))
 
1050
;                               (:instance totmissives-extract-sublst (l trlst) (ids (v-ids trlst)))
 
1051
;                               (:instance extract-sublst-identity)))
 
1052
;         ("Subgoal 9" :use (:instance ct-scheduled-correctness (prev nil)))
 
1053
;         ("Subgoal 9.4" :use (:instance ct-delayed-correctness (st ntkstate) (prev nil)))
 
1054
;         ("Subgoal 9.3" :use (:instance subsetp-scheduled-id-ct (prev nil)))
 
1055
;         ("Subgoal 8.2" :use (:instance ct-scheduled-correctness (st ntkstate) (prev nil)))))
 
1056
 
 
1057
          ("Subgoal 30"
 
1058
           :in-theory (disable ct-scheduling xy-routing-top))
 
1059
          ("Subgoal 23"
 
1060
           :in-theory (disable ct-scheduling ct-scheduling-assumptions xy-routing-top
 
1061
                               simple-extract-simulation))
 
1062
          ("Subgoal 25"
 
1063
           :use (:instance CorrectRoutesp-XYRouting (tmissives m)))
 
1064
          ("Subgoal 24"
 
1065
           :use (:instance TrLstp-XYRouting (tmissives m)))
 
1066
          ("Subgoal 13.2'" :use (:instance not-in-v-ids-ct (prev nil)))
 
1067
          ("Subgoal 8" :in-theory (disable consp-last trlstp))
 
1068
          ("Subgoal 8.2" :in-theory (e/d (trlstp) (consp-last)))
 
1069
          ("Subgoal 8.1" :use ((:instance tm-ids-tomissives-v-ids (x trlst))
 
1070
                                (:instance tomissives-extract-sublst
 
1071
                                           (l (totmissives trlst))
 
1072
                                           (ids (tm-ids (totmissives trlst))))
 
1073
                                (:instance totmissives-extract-sublst (l trlst) (ids (v-ids trlst)))
 
1074
                                (:instance extract-sublst-identity)))
 
1075
          ))
 
1076
 
 
1077
 
 
1078