← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/concurrent-programs/bakery/fairenv.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/concurrent-programs/bakery/fairenv.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#| 
 
4
 
 
5
     fairenv.lisp
 
6
     ~~~~~~~~~~~~
 
7
 
 
8
Note from Sandip:  The original version of this fairness book was developed by
 
9
Rob Sumners.  This version makes several changes, in particular the use of
 
10
btm-measure and top-measure.  A cleaner collection of fairness books were later
 
11
derived by Rob and submitted to the ACl2 2003 workshop.
 
12
 
 
13
Fair environment assumptions for the bakery algorithm
 
14
 
 
15
OK, the following encapsulated functions define the properties of a fair
 
16
environment for the bakery. This environment is defined by the following three
 
17
functions:
 
18
 
 
19
   (fair-select env X)   -- returns the next input for the bakery algorithm
 
20
   (faie-step env X)     -- takes the current environment state, bakery state
 
21
                            and Xternal input and returns the next environment
 
22
                            state.
 
23
   (fair-measure env in) -- returns a lexicographic pair (i include some theory 
 
24
                            below for well-founded ranks based on lexicographic
 
25
                            combinations of natural numbers) which is ensured
 
26
                            to decrease until the input in is selected.
 
27
 
 
28
We "install" the fair environment by redefining our step function to include
 
29
the functions fair-step and fair-select. Thus, with the  (bake+ st in) before,
 
30
we can now define the step function fair-bake+ as a step function using the
 
31
fair input. The precise definition will be given in programs.lisp.
 
32
 
 
33
|#
 
34
 
 
35
(include-book "measures")
 
36
(include-book "records")
 
37
 
 
38
(defun enqueue (e q)
 
39
  (if (endp q) (list e)
 
40
      (cons (first q) 
 
41
            (enqueue e (rest q)))))
 
42
 
 
43
(defmacro select-ctr (x) `(<- ,x :select-ctr))
 
44
(defmacro select-que (x) `(<- ,x :select-que))
 
45
(defmacro env (x) `(<- ,x :env))
 
46
 
 
47
(defun add-que (x q)
 
48
  (if (memberp x q) q (enqueue x q)))
 
49
 
 
50
(defun rotate-que (x)
 
51
  (enqueue (first x) (rest x)))
 
52
 
 
53
(defun que-pos (x q)
 
54
  (if (or (endp q)
 
55
          (equal x (first q)))
 
56
      0
 
57
    (1+ (que-pos x (rest q)))))
 
58
 
 
59
(defthm enqueue-leaves-que-pos-unchanged
 
60
  (implies (memberp x q)
 
61
           (equal (que-pos x (enqueue e q))
 
62
                  (que-pos x q))))
 
63
 
 
64
(defthm memberp-holds-of-enqueue
 
65
  (memberp e (enqueue e q)))
 
66
 
 
67
(defthm memberp-preserved-by-enqueue
 
68
  (implies (memberp a q)
 
69
           (memberp a (enqueue e q))))
 
70
 
 
71
(encapsulate 
 
72
 (((fair-select * *) => *)
 
73
  ((fair-step * *) => *)
 
74
  ((fair-measure * *) => *)
 
75
  ((btm-measure) => *)
 
76
  ((top-measure) => *))
 
77
 
 
78
 (local 
 
79
  (defun fair-select (env X)
 
80
    (if (zp (select-ctr env))
 
81
        (first (select-que env))
 
82
      X)))
 
83
 
 
84
 (local
 
85
  (defun fair-step (env X)
 
86
    (let ((queue (select-que env)))
 
87
      (if (zp (select-ctr env))
 
88
          (update env
 
89
                  :select-ctr X
 
90
                  :select-que (rotate-que queue))
 
91
        (update env
 
92
                :select-ctr (1- (select-ctr env))
 
93
                :select-que (add-que X queue))))))
 
94
 
 
95
 (local
 
96
  (defun fair-measure (env in)
 
97
    (list 2
 
98
          (que-pos in (select-que env))
 
99
          (nfix (select-ctr env)))))
 
100
 
 
101
 (local
 
102
  (defun btm-measure ()
 
103
    (list 1 0 0)))
 
104
 
 
105
 (local
 
106
  (defun top-measure ()
 
107
    (list 3 0 0)))
 
108
 
 
109
 ;;;; exported theorem required to prove invariant with select-que
 
110
 
 
111
 (defthm fair-env-select-que-preserves
 
112
   (memberp (fair-select env X) 
 
113
            (select-que (fair-step env X))))
 
114
 
 
115
 (defthm fair-step-preserves-membership
 
116
   (implies (memberp e (select-que env))
 
117
            (memberp e (select-que (fair-step env X)))))
 
118
 
 
119
 ;;;; exported properties of fair-measure
 
120
 
 
121
 (defthm fair-measure-is-measure
 
122
   (and (msrp (fair-measure env in))
 
123
        (nat-listp (fair-measure env in))))
 
124
 
 
125
 (defthm fair-measure-is-len-constant
 
126
   (len= (fair-measure (fair-step env in) in)
 
127
         (fair-measure env in)))
 
128
 
 
129
 (defthm input-selection-is-fair
 
130
   (implies (and (memberp in (select-que env))
 
131
                 (not (equal in (fair-select env X))))
 
132
            (msr< (fair-measure (fair-step env X) in)
 
133
                  (fair-measure env in))))
 
134
 
 
135
 ;;;; exported properties of btm-measure
 
136
 
 
137
 (defthm btm-measure-is-measure
 
138
   (and (msrp (btm-measure))
 
139
        (nat-listp (btm-measure))))
 
140
 
 
141
 (defthm btm-measure-is-len=0-fair-measure
 
142
   (len= (fair-measure env in)
 
143
         (btm-measure)))
 
144
 
 
145
 (defthm btm-measure-msr<-fair-measure
 
146
   (msr< (btm-measure)
 
147
         (fair-measure env in)))
 
148
 
 
149
 ;;;; exported properties of top-measure
 
150
 
 
151
 (defthm top-measure-is-measure
 
152
   (and (msrp (top-measure))
 
153
        (nat-listp (top-measure))))
 
154
 
 
155
 (defthm top-measure-is-len=0-fair-measure
 
156
   (len= (fair-measure env in)
 
157
         (top-measure)))
 
158
 
 
159
 (defthm fair-measure-msr<-top-measure
 
160
   (msr< (fair-measure env in)
 
161
         (top-measure)))
 
162
 
 
163
)
 
164
 
 
165
 
 
166
 
 
167
 
 
168