Event: Start with the library "interpreter".

;;;this files defines a token passing solution to the n processor
;;;mutual exclusion problem.

Definition: status (state, index) = cdr (assoc (cons ('me, index), state))

Definition: wait (state, index) = (status (state, index) = 'wait)

Definition: non-critical (state, index) = (status (state, index) = 'non-critical)

Definition: critical (state, index) = ((¬ non-critical (state, index)) ∧ (¬ wait (state, index)))

Definition: ticks (state, index) = fix (status (state, index))

Definition: critical-ticks (state, index, ticks) = (critical (state, index) ∧ (ticks (state, index) = fix (ticks)))

Definition: channel (state, index) = cdr (assoc (cons ('c, index), state))

Definition: token (state, index) = listp (channel (state, index))

Definition: me (old, new, index, size) = if non-critical (old, index)

then if non-critical (new, index) then if token (old, index)

then if add1-mod (size, index) = index

then (length (channel (new, index)) = length (channel (old, index))) ∧ changed (old, new, list (cons ('c, index)))

else (channel (new, index)

= cdr (channel (old, index)))

∧ (length (channel (new,

add1-mod (size, index)))

= (1 + length (channel (old, add1-mod (size,

index)))))

∧ changed (old, new, list (cons ('c, index), cons ('c,

add1-mod (size,

index)))) endif

else changed (old, new, nil) endif else wait (new, index)

∧ changed (old, new, list (cons ('me, index))) endif

elseif wait (old, index) then if token (old, index)

then (channel (new, index) = cdr (channel (old, index))) ∧ critical (new, index) ∧ changed (old,

new,

list (cons ('me, index), cons ('c, index)))

else changed (old, new, nil) endif else ((ticks (new, index) < ticks (old, index))

∧ critical (new, index) ∧ changed (old, new, list (cons ('me, index)))) ∨ (non-critical (new, index)

∧ (length (channel (new, add1-mod (size, index)))

= (1 + length (channel (old,

add1-mod (size,

index)))))

∧ changed (old, new, list (cons ('c, add1-mod (size, index)), cons ('me, index)))) endif

Definition: me-function (index, size, state) = if non-critical (state, index)

then if token (state, index)

then update-assoc (cons ('c, add1-mod (size, index)),

                 cons ('token,

channel (update-assoc (cons ('c, index),

cdr (channel (state,

index)),

state),

add1-mod (size, index))),

update-assoc (cons ('c, index), cdr (channel (state, index)),

state))

else state endif elseif wait (state, index) then if token (state, index)

then update-assoc (cons ('c, index), cdr (channel (state, index)), update-assoc (cons ('me, index), 0, state))

else state endif elseif ticks (state, index) ≃ 0 then update-assoc (cons ('c, add1-mod (size, index)),

cons ('token, channel (state, add1-mod (size, index))), update-assoc (cons ('me, index),

                                'non-critical,

state)) else update-assoc (cons ('me, index), ticks (state, index) − 1, state) endif

Theorem: total-me ((index ∈ N) ∧ (index < size)) → me (old, me-function (index, size, old), index, size)

Definition: program (index, size) = if index ≃ 0 then nil

else cons (list ('me, index − 1, size), program (index − 1, size)) endif

Definition: me-prg (size) = program (size, size)

Theorem: member-program (statement ∈ program (index, size)) = if index ≃ 0 then f

else (car (statement) = 'me) ∧ (cadr (statement) ∈ N) ∧ (cadr (statement) < index) ∧ (caddr (statement) = size) ∧ (cdddr (statement) = nil) endif

Theorem: member-me-prg (statement ∈ me-prg (size)) = if size ≃ 0 then f

else (car (statement) = 'me) ∧ (cadr (statement) ∈ N) ∧ (cadr (statement) < size) ∧ (caddr (statement) = size) ∧ (cdddr (statement) = nil) endif

Event: Disable me-prg.

Theorem: total-prg total (me-prg (size))

Definition: weight-of-triple (state, index, size) = (if critical (state, index) then 1

else 0 endif

+ length (channel (state, index))

+ length (channel (state, add1-mod (size, index))))

Theorem: weight-of-triple-preserved ((index ∈ N) ∧ (1 < size) ∧ (index < size) ∧ me (old, new, index, size)) → (weight-of-triple (new, index, size)

= weight-of-triple (old, index, size))

Definition: weight-but-triple (state, index, size, n) = if n ≃ 0 then 0

elseif (n − 1) = index

then weight-but-triple (state, index, size, n − 1)

else if critical (state, n − 1) then 1 else 0 endif + if (n − 1) = add1-mod (size, index) then 0 else length (channel (state, n − 1)) endif + weight-but-triple (state, index, size, n − 1) endif

Theorem: weight-but-triple-preserved ((index ∈ N) ∧ (index < size) ∧ me (old, new, index, size)) → (weight-but-triple (new, index, size, n)

= weight-but-triple (old, index, size, n))

Definition: weight (state, size) = if size ≃ 0 then 0

else if critical (state, size − 1) then 1 else 0 endif + length (channel (state, size − 1)) + weight (state, size − 1) endif

Theorem: weight-is-sum ((index ∈ N) ∧ (index < size) ∧ (1 < size)) → (weight (state, n)

= (if index < n

then if critical (state, index) then 1 else 0 endif + length (channel (state, index))

else 0 endif

+ if add1-mod (size, index) < n then length (channel (state, add1-mod (size, index))) else 0 endif

+ weight-but-triple (state, index, size, n)))

Theorem: weight-preserved-1 ((index ∈ N) ∧ (index < size) ∧ (1 < size) ∧ me (old, new, index, size)) → (weight (new, size) = weight (old, size))

Theorem: weight-preserved-2 me (old, new, 0, 1) → (weight (new, 1) = weight (old, 1))

Theorem: about-size-index ((index ∈ N) ∧ (index < size)) → (((index = 0) ∧ (size = 1)) ∨ (1 < size))

Theorem: weight-preserved ((index ∈ N) ∧ (index < size) ∧ me (old, new, index, size)) → (weight (new, size) = weight (old, size))

Event: Disable weight-is-sum.

Event: Disable weight-preserved-1.

Event: Disable weight-preserved-2.

Event: Disable weight-of-triple-preserved.

Event: Disable weight-but-triple-preserved.

Event: Disable total-me.

Definition: mutual-exclusionp (state, size) = (weight (state, size) = 1)

Theorem: mutual-exclusionp-unless-sufficient unless-sufficient (statement,

me-prg (size),

old, new,

              `(mutual-exclusionp state ',size),
              '(false))

Event: Disable weight-preserved.

Theorem: mutual-exclusionp-prg

unless (`(mutual-exclusionp state ',size), '(false), me-prg (size))

Theorem: wait-unless-critical-1 ((index ∈ N) ∧ (index < size) ∧ me (old, new, index, size) ∧ wait (old, index)) → (wait (new, index) ∨ critical (new, index))

Theorem: wait-unless-critical-2 ((index ∈ N) ∧ (index < size) ∧ (index1 ∈ N) ∧ (index1 < size) ∧ (index ≠ index1 ) ∧ me (old, new, index1 , size) ∧ wait (old, index)) → (wait (new, index) ∨ critical (new, index))

Theorem: wait-unless-critical-unless-sufficient ((index ∈ N) ∧ (index < size)) → unless-sufficient (statement,

me-prg (size),

old, new,

                  `(wait state ',index),
                  `(critical state ',index))

Theorem: wait-unless-critical ((index ∈ N) ∧ (index < size) ∧ (size ≄ 0))

→ unless (`(wait state ',index),
          `(critical state ',index),

me-prg (size))

Theorem: celcor-ensures-key ((index ∈ N) ∧ (index < size)) → ensures-key (list ('me, index, size),

me-prg (size), old, new,

               `(and
                 (critical state ',index)
                 (lessp
                  (ticks state ',index)
                  ',(add1 ticks))),
               `(or
                 (and
                  (critical state ',index)
                  (lessp (ticks state ',index) ',ticks))
                 (token state ',(add1-mod size index))))

Theorem: celcor-ensures-rest ((index ∈ N) ∧ (index < size)) → ensures-rest (statement,

list ('me, index, size), me-prg (size), old, new,

               `(and
                 (critical state ',index)
                 (lessp
                  (ticks state ',index)
                  ',(add1 ticks))),

q)

Theorem: critical-ensures-less-critical-or-right ((index ∈ N) ∧ (index < size)) → ensures (`(and

             (critical state ',index)
             (lessp (ticks state ',index) ',(add1 ticks))),
           `(or
             (and
              (critical state ',index)
              (lessp (ticks state ',index) ',ticks))
             (token state ',(add1-mod size index))),

me-prg (size))

Theorem: critical-unless-less-critical-or-right ((index ∈ N) ∧ (index < size))

→ unless (`(and

            (critical state ',index)
            (lessp (ticks state ',index) ',(add1 ticks))),
          `(or
            (and
             (critical state ',index)
             (lessp (ticks state ',index) ',ticks))
            (token state ',(add1-mod size index))),

me-prg (size))

Theorem: wlcec-ensures-key ((index ∈ N) ∧ (index < size)) → ensures-key (list ('me, index, size),

me-prg (size),

old, new,

               `(and
                 (wait state ',index)
                 (token state ',index)),
               `(critical state ',index))

Theorem: wlcec-ensures-rest ((index ∈ N) ∧ (index < size)) → ensures-rest (statement,

list ('me, index, size), me-prg (size), old, new,

               `(and
                 (wait state ',index)
                 (token state ',index)),

q)

Theorem: wait-and-left-channel-ensures-critial ((index ∈ N) ∧ (index < size)) → ensures (`(and

             (wait state ',index)
             (token state ',index)),
           `(critical state ',index),

me-prg (size))

Theorem: wait-and-left-channel-unless-critial ((index ∈ N) ∧ (index < size)) → unless (`(and

            (wait state ',index)

            (token state ',index)),
          `(critical state ',index),

me-prg (size))

Theorem: nclcewlcorc-ensures-key ((index ∈ N) ∧ (index < size)) → ensures-key (list ('me, index, size),

me-prg (size), old, new,

               `(and
                 (non-critical state ',index)
                 (token state ',index)),
               `(or
                 (and
                  (wait state ',index)
                  (token state ',index))
                 (token state ',(add1-mod size index))))

Theorem: nclcewlcorc-ensures-rest ((index ∈ N) ∧ (index < size)) → ensures-rest (statement,

list ('me, index, size), me-prg (size), old, new,

               `(and
                 (non-critical state ',index)
                 (token state ',index)),

q)

Theorem: non-critical-left-ensures-wait-left-or-right ((index ∈ N) ∧ (index < size)) → ensures (`(and

             (non-critical state ',index)
             (token state ',index)),
           `(or
             (and
              (wait state ',index)
              (token state ',index))
             (token state ',(add1-mod size index))),

me-prg (size))

Theorem: non-critical-left-unless-wait-left-or-right ((index ∈ N) ∧ (index < size))

→ unless (`(and

            (non-critical state ',index)
            (token state ',index)),
          `(or
            (and
             (wait state ',index)
             (token state ',index))
            (token state ',(add1-mod size index))),

me-prg (size))

Theorem: listp-me-prg (size ≄ 0) → listp (me-prg (size))

Theorem: mutual-exclusionp-is-invariant (initial-condition (`(mutual-exclusionp state ',size), me-prg (size)) ∧ (size ≄ 0))

→ invariant (`(mutual-exclusionp state ',size), me-prg (size))

Theorem: critical-leads-to-less-critical-or-right ((index ∈ N) ∧ (index < size)) → leads-to (`(and

              (critical state ',index)
              (lessp
               (ticks state ',index)
               ',(add1 ticks))),
            `(or
              (and
               (critical state ',index)
               (lessp (ticks state ',index) ',ticks))
              (token state ',(add1-mod size index))),

me-prg (size))

Theorem: critical-ticks-leads-to-right ((index ∈ N) ∧ (index < size)) → leads-to (`(and

              (critical state ',index)
              (lessp
               (ticks state ',index)
               ',(add1 ticks))),
            `(token state ',(add1-mod size index)),

me-prg (size))

Theorem: critical-leads-to-right ((index ∈ N) ∧ (index < size))

→ leads-to (`(critical state ',index),

`(token state ',(add1-mod size index)),

me-prg (size))

Theorem: wait-left-leads-to-critical ((index ∈ N) ∧ (index < size)) → leads-to (`(and

  (wait state ',index)
  (token state ',index)),
`(critical state ',index),

me-prg (size))

Theorem: non-critical-left-leads-to-wait-left-or-right ((index ∈ N) ∧ (index < size)) → leads-to (`(and

  (non-critical state ',index)
  (token state ',index)),
`(or
  (and
   (wait state ',index)
   (token state ',index))
  (token state ',(add1-mod size index))),

me-prg (size))

Theorem: wait-left-leads-to-right ((index ∈ N) ∧ (index < size)) → leads-to (`(and

  (wait state ',index)
  (token state ',index)),
`(token state ',(add1-mod size index)),

me-prg (size))

Theorem: non-critical-left-leads-to-right ((index ∈ N) ∧ (index < size)) → leads-to (`(and

  (non-critical state ',index)
  (token state ',index)),
`(token state ',(add1-mod size index)),

me-prg (size))

Theorem: critical-wait-non-critical critical (state, index) ∨ wait (state, index) ∨ non-critical (state, index)

Definition: tokens (state, size) = if size ≃ 0 then nil elseif token (state, size − 1) then cons (size − 1, tokens (state, size − 1)) else tokens (state, size − 1) endif

Definition: criticals (state, size) = if size ≃ 0 then nil

elseif critical (state, size − 1)

then cons (size − 1, criticals (state, size − 1))

else criticals (state, size − 1) endif

Theorem: equal-plus-1 ((a + b) = 1) = (((a = 1) ∧ (b ≃ 0)) ∨ ((b = 1) ∧ (a ≃ 0)))

Theorem: about-mutual-exclusionp if weight (state, size) ≃ 0 then (tokens (state, size) = nil) ∧ (criticals (state, size) = nil) elseif weight (state, size) = 1 then ((length (tokens (state, size)) = 1)

∧ (criticals (state, size) = nil)) ∨ ((length (criticals (state, size)) = 1) ∧ (tokens (state, size) = nil))

else t endif

Event: Disable equal-plus-1.

Theorem: numberp-car-tokens car (tokens (state, size)) ∈ N

Theorem: numberp-car-criticals car (criticals (state, size)) ∈ N

Theorem: lessp-car-tokens (car (tokens (state, size)) < size) = (size ≄ 0)

Theorem: lessp-car-criticals (car (criticals (state, size)) < size) = (size ≄ 0)

Theorem: mutual-exclusionp-requires-state mutual-exclusionp (state, size) → (size ≄ 0)

Theorem: lessp-car-tokens-and-criticals mutual-exclusionp (state, size) → ((car (tokens (state, size)) < size)

∧ (car (criticals (state, size)) < size))

Theorem: about-member-list-length-one (length (list) = 1) → ((x ∈ list) = (x = car (list)))

Theorem: about-member-car-tokens-criticals mutual-exclusionp (state, size) → (((index ∈ tokens (state, size))

= (listp (tokens (state, size))

∧ (index = car (tokens (state, size))))) ∧ ((index ∈ criticals (state, size))

= (listp (criticals (state, size)) ∧ (index = car (criticals (state, size))))))

Theorem: not-member-tokens (index ≮ size) → (index ∉ tokens (state, size))

Theorem: not-member-criticals (index ≮ size) → (index ∉ criticals (state, size))

Theorem: token-equals ((index ∈ N) ∧ (index < size)) → (token (state, index) = (index ∈ tokens (state, size)))

Theorem: critical-equals ((index ∈ N) ∧ (index < size)) → (critical (state, index) = (index ∈ criticals (state, size)))

Theorem: mtoken-equals (mutual-exclusionp (state, size) ∧ (index ∈ N) ∧ (index < size)) → (token (state, index)

= (listp (tokens (state, size)) ∧ (index = car (tokens (state, size)))))

Theorem: mcritical-equals (mutual-exclusionp (state, size) ∧ (index ∈ N) ∧ (index < size)) → (critical (state, index)

= (listp (criticals (state, size)) ∧ (index = car (criticals (state, size)))))

Theorem: mutual-exclusionp-implies mutual-exclusionp (state, size) → (listp (tokens (state, size)) ↔ (¬ listp (criticals (state, size))))

Event: Disable lessp-car-criticals.

Event: Disable lessp-car-tokens.

Event: Disable about-member-list-length-one.

Event: Disable not-member-tokens.

Event: Disable not-member-criticals.

Event: Disable token.

Event: Disable critical.

Event: Disable non-critical.

Event: Disable wait.

Event: Disable mutual-exclusionp.

Theorem: mutual-exclusionp-implies-prg mutual-exclusionp (state, size) → listp (me-prg (size))

Theorem: left-leads-to-right ((index ∈ N) ∧ (index < size)

 ∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

 → leads-to (`(token state ',index),
            `(token state ',(add1-mod size index)),

me-prg (size))

Definition: walk-ring (a, b, size) = if a ∈ N

then if b ∈ N

then if a < size

then if b < size

then if a = b then t

else walk-ring (add1-mod (size, a), b, size) endif else t endif

else t endif else t endif

else t endif Theorem: any-left-leads-to-right ((left ∈ N) ∧ (left < size) ∧ (right ∈ N) ∧ (right < size)

∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

→ leads-to (`(token state ',left),
           `(token state ',right),

me-prg (size))

Theorem: lessp-add1-mod-size mutual-exclusionp (state, size) → (add1-mod (size, n) < size)

Theorem: any-critical-leads-to-right ((left ∈ N) ∧ (left < size) ∧ (right ∈ N) ∧ (right < size)

∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

→ leads-to (`(critical state ',left),
           `(token state ',right),

me-prg (size))

Theorem: any-leads-to-right ((index ∈ N) ∧ (index < size)

∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

→ leads-to ('(true), `(token state ',index), me-prg (size))

Theorem: me-prg-non-zero-size listp (me-prg (size)) = (size ≄ 0)

Theorem: wait-leads-to-left-wait-or-critical ((index ∈ N) ∧ (index < size)

∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

→ leads-to (`(and (true) (wait state ',index)),
           `(or
             (and
              (token state ',index)
              (wait state ',index))

  (critical state ',index)),

me-prg (size))

Theorem: wait-leads-to-critical ((index ∈ N) ∧ (index < size)

∧ initial-condition (`(mutual-exclusionp state ',size),

me-prg (size)))

→ leads-to (`(wait state ',index),
`(critical state ',index),

me-prg (size))

Index

about-member-car-tokens-critica

ls, 13 about-member-list-length-one, 13 about-mutual-exclusionp, 12 about-size-index, 5 add1-mod, 1–5, 14, 15 any-critical-leads-to-right, 15 any-leads-to-right, 15 any-left-leads-to-right, 15

celcor-ensures-key, 7 celcor-ensures-rest, 7 changed, 1, 2 channel, 1–5 critical, 1, 2, 4–6, 11–13 critical-ensures-less-critical-

or-right, 7 critical-equals, 13 critical-leads-to-less-critical

-or-right, 10 critical-leads-to-right, 10 critical-ticks, 1 critical-ticks-leads-to-right, 10 critical-unless-less-critical-o

r-right, 7 critical-wait-non-critical, 11 criticals, 12, 13

ensures, 7–9 ensures-key, 7–9 ensures-rest, 7–9 equal-plus-1, 12

initial-condition, 10, 14–16 invariant, 10

leads-to, 10, 11, 14–16 left-leads-to-right, 14 length, 1, 2, 4, 5, 12, 13 lessp-add1-mod-size, 15 lessp-car-criticals, 12 lessp-car-tokens, 12 lessp-car-tokens-and-criticals, 12 listp-me-prg, 10

mcritical-equals, 13

me, 1, 3–6

me-function, 2, 3

me-prg, 3, 4, 6–11, 14–16 me-prg-non-zero-size, 15 member-me-prg, 3 member-program, 3 mtoken-equals, 13 mutual-exclusionp, 5, 12–15 mutual-exclusionp-implies, 13 mutual-exclusionp-implies-prg, 14 mutual-exclusionp-is-invariant, 10 mutual-exclusionp-prg, 6 mutual-exclusionp-requires-state, 12 mutual-exclusionp-unless-sufficie

nt, 6

nclcewlcorc-ensures-key, 9 nclcewlcorc-ensures-rest, 9 non-critical, 1, 2, 11 non-critical-left-ensures-wait-

left-or-right, 9 non-critical-left-leads-to-right, 11 non-critical-left-leads-to-wait -left-or-right, 11 non-critical-left-unless-wait-le

ft-or-right, 9 not-member-criticals, 13 not-member-tokens, 13 numberp-car-criticals, 12 numberp-car-tokens, 12

program, 3

status, 1

ticks, 1–3

token, 1–3, 12, 13 token-equals, 13 tokens, 11–13 total, 4 total-me, 3 total-prg, 4

unless, 6, 8–10 unless-sufficient, 6 update-assoc, 2, 3

wait, 1–3, 6, 11 wait-and-left-channel-ensures-c

ritial, 8 wait-and-left-channel-unless-criti

al, 8 wait-leads-to-critical, 16 wait-leads-to-left-wait-or-criti

cal, 15 wait-left-leads-to-critical, 11 wait-left-leads-to-right, 11 wait-unless-critical, 6 wait-unless-critical-1, 6 wait-unless-critical-2, 6 wait-unless-critical-unless-suf

ficient, 6 walk-ring, 14 weight, 4, 5, 12 weight-but-triple, 4, 5 weight-but-triple-preserved, 4 weight-is-sum, 4 weight-of-triple, 4 weight-of-triple-preserved, 4 weight-preserved, 5 weight-preserved-1, 5 weight-preserved-2, 5 wlcec-ensures-key, 8 wlcec-ensures-rest, 8