Below are two extra credit problems. You can send solutions before Dec. 7th and each is worth an extra 25 points on one of your homework assignments. You have to work on these alone.
The semantics of distributed systems are often given with respect
to what is called the interleaved semantics. A state of a
distributed system is just a configuration of the systems
comprising the distributed system, which might also include the
state of the network(s). The set of successor states of a
distributed system state is the set of states obtained by
selecting one of the systems and stepping it: letting it take a
local, atomic step. A schedule is just a list of systems and
defines a run, a sequence of states, of the distributed system,
where the first state is the initial state, the second state is
obtained by stepping the first system of the schedule starting in
the first state of the run, the third state is obtained by
stepping the second system of the schedule starting in the second
state of the run, and so on. A scheduler defines a set of
schedules. The semantics of a distributed system given some
scheduler is the set of runs allowed by scheduler. Since some
schedules can ignore certain systems (meaning that they never get
a chance to make a move), schedulers are often required to be
fair. Your job is to define a fair scheduler for an infinite
number of processes. Provide a book that exports two constrained
functions f and nxt, that satisfy the
following constraints.
The function f is the scheduler, and given a natural
number i, (f i) is the id of the
process that takes a step at time i. One of the
constraints is that f returns a natural number.
(defthm natp-f
(natp (f i)))
That f is fair means that for any time
i and process id p, there is another
time (nxt i p) >=i at which p takes a
step. This is expressed with the following two theorems. First,
i <= (nxt i p).
(defthm <=-i-nxt
(implies (and (natp i)
(natp p))
(<= i (nxt i p))))
Second, (f (nxt i p)) = p.
(defthm nxt-f
(implies (and (natp i)
(natp p))
(equal (f (nxt i p)) p))))
The only thing that your book should export are the above three
theorems. Note that this means you will have to use local and
encapsulate to exhibit functions that satisfy the above
constraints.
You may want to use the top-with-meta arithmetic book, which can
be included with the following command.
(include-book "arithmetic/top-with-meta" :dir :system)
It is often useful to reason about finite functions; functions
whose domain is essentially finite. I say "essentially" because
the functions can be over an infinite domain, as long as only a
finite number of elements in the domain have a non-default value
(let's say that the default value is nil). Notice
that such functions can be represented as alists. Also, notice
that such functions generalize the notion of a structure, as a
structure is just a finite function whose domain is the set of
fields.
Develop a book that allows one to reason about finite functions.
Start by defining the functions val and
set such that if f is a finite
function, then (val elem f) returns the value that
f assigns to element elem and
(set elem val f) is the finite function that is just
like f, except that the value of elem
is val.
The book should export the following events (and any others you need/ want).
(defthm val-same-set
(equal (val elem (set elem x f))
x))
(defthm val-diff-set
(implies (not (equal elem elem2))
(equal (val elem (set elem2 x f))
(val elem f))))
(defthm set-same-val
(equal (set elem (val elem f) f)
f))
(defthm set-same-set
(equal (set elem y (set elem x f))
(set elem y f)))
(defthm set-diff-set
(implies (not (equal elem elem2))
(equal (set elem2 y (set elem x f))
(set elem x (set elem2 y f))))
:rule-classes ((:rewrite :loop-stopper ((elem2 elem set)))))
Note that the you cannot prove the above theorems using the
obvious ways of representing finite functions. This exercise is
hard, so if you have to, you can include additional hypotheses to
the above theorems.
You will want to familiarize yourself with ACL2's total order,
because finite functions can have any type of elements in their
domain. To get you started, here are the contents of a book that
defines << to be an irreflexive total order on the
ACL2 universe.
(in-package "ACL2")
(defun << (x y)
(and (lexorder x y)
(not (equal x y))))
(defthm <<-irreflexive
(not (<< x x)))
(defthm <<-transitive
(implies (and (<< x y)
(<< y z))
(<< x z)))
(defthm <<-asymmetric
(implies (<< x y)
(not (<< y x))))
(defthm <<-trichotomy
(implies (and (not (<< y x))
(not (equal x y)))
(<< x y)))
(defthm <<-implies-lexorder
(implies (<< x y)
(lexorder x y)))
(in-theory (disable <<))