← 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/generic-modules/GeNoC-scheduling.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/generic-modules/GeNoC-scheduling.lisp
 
1
#|$ACL2s-Preamble$;
 
2
; Julien Schmaltz
 
3
;; Generic Scheduling Module of GeNoC
 
4
;; Feb 16th 2005
 
5
;; File: GeNoC-scheduling.lisp
 
6
;; Amr HELMY Revised and modified January 24th 2008 
 
7
;;edited by Amr HELMY, Laurence Pierre august 22nd of august 2007
 
8
 
 
9
;;Amr helmy 
 
10
;;31st october 2007
 
11
 
 
12
(begin-book);$ACL2s-Preamble$|#
 
13
 
 
14
(in-package "ACL2")
 
15
(include-book "GeNoC-nodeset")
 
16
(include-book "GeNoC-misc") ;; imports also GeNoC-types
 
17
(include-book "GeNoC-ntkstate")#|ACL2s-ToDo-Line|#
 
18
;
 
19
;; Inputs: TrLst = ( ... (Id org frm route) ...), measure, NodeSet, and
 
20
;; the current network state
 
21
;; outputs: TrLst updated, arrived missives, new state of the network,
 
22
;; measure updated
 
23
 
 
24
 
 
25
(defspec GenericScheduling
 
26
  ;; Function Scheduling represents the scheduling policy of the 
 
27
  ;; network. 
 
28
  ;; arguments: TrLst measure P
 
29
  ;; outputs: newTrLst Arrived newP newMeasure
 
30
  (((scheduling * *  * *) => (mv * * * *))
 
31
   ((get_next_priority *)=> *)
 
32
   ((scheduling-assumptions *  * * *) => *)
 
33
   ((legal-measure * * * * *) => *)
 
34
   ((initial-measure * * * *) => *))
 
35
 
 
36
  (local (defun get_next_priority (port)
 
37
           port))
 
38
  (local (defun scheduling-assumptions (TrLst NodeSet ntkstate order)
 
39
           (declare (ignore TrLst NodeSet ntkstate order))
 
40
           nil))
 
41
  (local (defun legal-measure (measure trlst nodeset ntkstate order)
 
42
           (declare (ignore measure trlst nodeset ntkstate order))
 
43
           nil))
 
44
  (local (defun initial-measure (trlst nodeset ntkstate order)
 
45
           (declare (ignore trlst nodeset ntkstate order))
 
46
           nil))
 
47
  (local (defun scheduling (TrLst NodeSet ntkstate order)
 
48
           ;; local witness
 
49
           (mv 
 
50
            ;; TrLst updated
 
51
            (if (not (scheduling-assumptions TrLst NodeSet ntkstate order))
 
52
                (totmissives TrLst) 
 
53
              nil)
 
54
            ;; arrived messages
 
55
            ;(if (is-base-measure measure)
 
56
                nil  
 
57
            ;  TrLst)
 
58
            ;; measure is nil
 
59
            nil
 
60
            ;; ntkstate preserved
 
61
            ntkstate)
 
62
            ))
 
63
 
 
64
  ;; Proof obligations (also named constraints)
 
65
  ;; -----------------------------------------
 
66
  (defthm scheduled-nil-nil 
 
67
    ;; the result of the scheduling function in the case of empty
 
68
    ;; input list is equal to nil
 
69
    (equal (car (scheduling nil nodeset  ntkstate order)) nil))
 
70
  
 
71
  ;; 1/ Types of newTrLst, Arrived and P (state)
 
72
  ;; ---------------------------------
 
73
  ;; The type of newTrLst is a valid traveling missives list
 
74
  
 
75
  (defthm tmissivesp-newTrlst     
 
76
    (implies (trlstp TrLst nodeset)
 
77
             (tmissivesp (mv-nth 0 (scheduling TrLst NodeSet ntkstate order))
 
78
                         NodeSet)))                        
 
79
   
 
80
  ;; so is the list of Arrived
 
81
  (defthm trlstp-Arrived      ;; OK
 
82
    (implies (trlstp TrLst nodeset)
 
83
             (trlstp (mv-nth 1 (scheduling TrLst NodeSet ntkstate order))
 
84
                     nodeset)))  
 
85
  
 
86
  ;; the state list P is a ValidState
 
87
  (defthm Valid-state-ntkstate
 
88
    (implies (validstate ntkstate)
 
89
             (validstate (mv-nth 3 (scheduling TrLst NodeSet ntkstate order)))))
 
90
 
 
91
  
 
92
  ;; 2/ the measure provided to GeNoC must be decreasing.
 
93
  ;; ------------------------------------------------------
 
94
  ;; scheduling-assumptions must be a boolean
 
95
  (defthm booleanp-assumptions
 
96
    (booleanp (scheduling-assumptions TrLst NodeSet ntkstate order))
 
97
    :rule-classes :type-prescription)
 
98
  
 
99
  ;; legal-measure nust be a boolean
 
100
  (defthm booleanp-legal-measure
 
101
    (booleanp (legal-measure measure trlst nodeset ntkstate order))
 
102
    :rule-classes :type-prescription)
 
103
  
 
104
  ;; the measure must decrease on each call of scheduling
 
105
  (defthm measure-decreases
 
106
    (implies (and (legal-measure measure trlst nodeset ntkstate order)
 
107
                  (scheduling-assumptions trlst NodeSet ntkstate order))
 
108
             (O< (acl2-count (mv-nth 2 (scheduling TrLst NodeSet ntkstate order)))
 
109
                 (acl2-count measure))))
 
110
  
 
111
  
 
112
  ;; 3/ Correctness of the arrived missives
 
113
  ;; ------------------------------------------------------------------
 
114
  ;; For any arrived missive arr, there exists a unique travel
 
115
  ;; tr in the initial TrLst, such that IdV(arr) = IdV(tr)
 
116
  ;; and FrmV(arr) = FrmV(tr) and RoutesV(arr) is a 
 
117
  ;; sublist of RoutesV(tr).
 
118
  ;; In ACL2, the uniqueness of the ids is given by the predicate
 
119
  ;; TrLstp.
 
120
  ;; -------------------------------------------------------------------
 
121
  
 
122
  ;; First, let us define this correctness
 
123
  (defun s/d-travel-correctness (arr-TrLst TrLst/arr-ids)
 
124
    (if (endp arr-TrLst)
 
125
        (if (endp TrLst/arr-ids)
 
126
            t
 
127
          nil)
 
128
      (let* ((arr-tr (car arr-TrLst))
 
129
             (tr (car TrLst/arr-ids)))
 
130
        (and (equal (FrmV arr-tr) (FrmV tr))
 
131
             (equal (IdV arr-tr) (IdV tr))
 
132
             (equal (OrgV arr-tr) (OrgV tr))
 
133
             (equal (FlitV arr-tr) (FlitV tr))
 
134
             (equal (timeV arr-tr) (TimeV tr))
 
135
             (subsetp (RoutesV arr-tr) (RoutesV tr))
 
136
             (s/d-travel-correctness (cdr arr-TrLst) 
 
137
                                     (cdr TrLst/arr-ids))))))
 
138
  
 
139
  
 
140
  (defthm s/d-travel-correctness-unitary
 
141
    (implies (trlstp x nodeset)
 
142
             (s/d-travel-correctness x x)))
 
143
  
 
144
  (defthm arrived-travels-correctness      
 
145
    (mv-let (newTrLst Arrived newMeasure newstate )
 
146
            (scheduling TrLst  NodeSet  ntkstate order)
 
147
            (declare (ignore newTrLst newMeasure newstate ))
 
148
            (implies (TrLstp TrLst nodeset)
 
149
                     (s/d-travel-correctness
 
150
                      Arrived
 
151
                      (extract-sublst TrLst (V-ids Arrived)))))  
 
152
    :hints (("Goal" :in-theory (disable trlstp))))
 
153
  
 
154
  (defthm subsetp-arrived-newTrLst-ids
 
155
    ;; this should be provable from the two lemmas above
 
156
    ;; but it will always be trivial to prove, and it is
 
157
    ;; useful in subsequent proofs.
 
158
    (mv-let (newTrLst Arrived newMeasure newstate )
 
159
            (scheduling TrLst NodeSet ntkstate order)
 
160
            (declare (ignore newMeasure newstate ))
 
161
            (implies (TrLstp TrLst nodeset)
 
162
                     (and (subsetp (v-ids Arrived) (v-ids Trlst))
 
163
                          (subsetp (Tm-ids newTrLst) (v-ids TrLst))))))
 
164
  
 
165
  
 
166
  ;; 4. Correctness of the newTrLst travels
 
167
  ;; -------------------------------------
 
168
  ;; the correctness of the newTrLst travels differs from
 
169
  ;; the correctness of the Arrived travels because,
 
170
  ;; for the Arrived travels we will generally keep only 
 
171
  ;; one route, but for the newTrLst travels we will not modify
 
172
  ;; the travels and keep all the routes. In fact, by 
 
173
  ;; converting a travel back to a missive we will remove the 
 
174
  ;; routes.
 
175
  ;; ---------------------------------------------------------
 
176
  
 
177
  ;; the list newTrLst is equal to filtering the initial 
 
178
  ;; TrLst according to the Ids of newTrLst
 
179
  
 
180
  
 
181
  
 
182
  (defthm newTrLst-travel-correctness       ;; OK
 
183
    ;; the correctness of newtrlst is the equivalence of the transformation
 
184
    ;;of the newtrlst into missives, and the transformation of the
 
185
    ;;initial trlst (input to the scheduling function)
 
186
    ;;into tmissives and then to missives 
 
187
    ;; this rule will cause an infinite number of rewrites that's why
 
188
    ;; it's in rule-classes nil, we have to create an instance to use
 
189
    ;; it
 
190
    (mv-let (newTrLst Arrived  newMeasure newstate )
 
191
            (scheduling TrLst NodeSet  ntkstate order)
 
192
            (declare (ignore Arrived newMeasure newstate))
 
193
            (implies (TrLstp TrLst nodeset)
 
194
                     (equal (tomissives newTrLst)
 
195
                            (extract-sublst (tomissives(totmissives
 
196
                                                        TrLst))
 
197
                                            (Tm-ids newTrLst)))))
 
198
 
 
199
    :rule-classes nil)
 
200
  
 
201
  ;; 6/ if scheduling assumptions are not met, measure is nil
 
202
  (defthm mv-nth-2-scheduling-on-zero-measure      ;; OK
 
203
    ;; if the scheduling measure is 0
 
204
    ;; the new measure is equal to the initial one
 
205
    (implies (and (not (scheduling-assumptions TrLst NodeSet ntkstate order))
 
206
                  (TrLstp trlst nodeset))
 
207
             (equal (mv-nth 2 (scheduling TrLst NodeSet ntkstate order))  ;; new measure
 
208
              nil)))
 
209
  
 
210
  (defthm mv-nth-0-scheduling-on-zero-measure    ;; OK
 
211
    ;; if the scheduling measure is 0
 
212
    ;; the set of newTrLst s is equal to the initial TrLst
 
213
    (implies (not (scheduling-assumptions TrLst NodeSet ntkstate order))
 
214
             (equal
 
215
              (mv-nth 0 (scheduling TrLst NodeSet ntkstate order))
 
216
              (totmissives TrLst))))
 
217
  
 
218
  ;; 7/ The intersection of the ids of the Arrived travels and those 
 
219
  ;; of the newTrLst travels is empty
 
220
  ;; -----------------------------------------------------------------
 
221
  
 
222
  (defthm not-in-newTrLst-Arrived         ;; OK
 
223
    (mv-let (newTrLst Arrived  newmeasure newstate )
 
224
            (scheduling TrLst NodeSet ntkstate order)
 
225
            (declare (ignore  newmeasure newstate ))
 
226
            (implies (TrLstp TrLst nodeset)
 
227
                     (not-in (Tm-ids newTrLst) (v-ids Arrived)))))
 
228
 
 
229
  ;; some constraints required because we do not have a definition
 
230
  ;; for scheduling
 
231
  (defthm consp-scheduling      ;; OK
 
232
    ;; for the mv-nth
 
233
    (consp (scheduling TrLst NodeSet ntkstate order))
 
234
    :rule-classes :type-prescription)
 
235
  
 
236
  (defthm true-listp-car-scheduling      ;; OK
 
237
    (implies (true-listp TrLst)
 
238
             (true-listp (mv-nth 0 (scheduling TrLst NodeSet
 
239
                                               ntkstate order ))))
 
240
    
 
241
    :rule-classes :type-prescription)
 
242
  
 
243
  (defthm true-listp-mv-nth-1-sched-1      ;; OK
 
244
    (implies (true-listp TrLst)
 
245
             (true-listp (mv-nth 1 (scheduling TrLst NodeSet
 
246
                                               ntkstate order))))
 
247
    
 
248
    :rule-classes :type-prescription)
 
249
  
 
250
  (defthm true-listp-mv-nth-1-sched-2      ;; OK
 
251
    (implies (TrLstp TrLst nodeset)
 
252
             (true-listp (mv-nth 1 (scheduling TrLst NodeSet
 
253
                                               ntkstate order))))
 
254
    
 
255
    :rule-classes :type-prescription)
 
256
  
 
257
  ) ;; end of scheduling
 
258
 
 
259
 
 
260
(defthm correctroutesp-s/d-travel-correctness    ;; OK
 
261
  ;; correctroutesp between trlst/ids and it's transformation into
 
262
  ;; tmissves, and the s/d-travel-correctness, between trlst/ids and
 
263
  ;; trlst1 
 
264
  ;; implies the correctroutesp between trlst1 and trlst/ids
 
265
  (implies (and (CorrectRoutesp TrLst/ids (ToTMissives TrLst/ids) NodeSet)
 
266
                (s/d-travel-correctness TrLst1 TrLst/ids))
 
267
           (CorrectRoutesp TrLst1 
 
268
                           (ToTMissives TrLst/ids) NodeSet)))
 
269
 
 
270
 
 
271
(defthm scheduling-preserves-route-correctness      ;; OK
 
272
  ;; we prove that sheduling preserve the correctness of the routes
 
273
  ;; after the transformation
 
274
  (mv-let (newTrLst Arrived newmeasure newstate )
 
275
          (scheduling TrLst NodeSet ntkstate order)
 
276
          (declare (ignore newTrLst newstate newmeasure ))
 
277
          (implies (and (CorrectRoutesp TrLst (ToTMissives TrLst) NodeSet)
 
278
                        (TrLstp TrLst nodeset))
 
279
                   (CorrectRoutesp Arrived
 
280
                                   (ToTMissives
 
281
                                    (extract-sublst 
 
282
                                     TrLst
 
283
                                     (V-ids Arrived)))
 
284
                                   NodeSet)))
 
285
  :otf-flg t
 
286
  :hints (("GOAL"
 
287
           :do-not '(eliminate-destructors generalize)
 
288
           :do-not-induct t
 
289
           :in-theory 
 
290
           (disable mv-nth ;; to have my rules used
 
291
                    ToTMissives-extract-sublst TrLstp))))
 
292
 
 
293
 
 
294
(defthm TMissivesp-mv-nth-0-scheduling       ;; OK
 
295
  (let ((NodeSet (NodeSetGenerator Params)))
 
296
    (implies (and (CorrectRoutesp TrLst (ToTMissives TrLst) NodeSet)
 
297
                  (ValidParamsp Params)
 
298
                  (TrLstp TrLst nodeset))
 
299
             (TMissivesp (mv-nth 0 (scheduling TrLst NodeSet
 
300
                                               ntkstate order))
 
301
                         NodeSet)))
 
302
 
 
303
  :hints (("Goal" 
 
304
           :use 
 
305
           (:instance tmissivesp-newTrlst 
 
306
                      (nodeset (NodeSetGenerator Params))))))
 
307