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
nxt, that satisfy the
f is the scheduler, and given a natural
(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)))
fis fair means that for any time
iand process id
p, there is another time
(nxt i p) >=iat which
ptakes 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))))
(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.
(defthm nxt-f (implies (and (natp i) (natp p)) (equal (f (nxt i p)) p))))
(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
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
Develop a book that allows one to reason about finite functions.
Start by defining the functions
set such that if
f is a finite
(val elem f) returns the value that
f assigns to element
(set elem val f) is the finite function that is just
f, except that the value of
The book should export the following events (and any others you need/ want).
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
(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)))))
<<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 <<))