COMP4161 T3/2022 Advanced Topics in Software Verification
Assignment 2
This assignment starts on Friday 14th October 2022 and is due on Friday 4nd November 2022 6pm. We will accept Isabelle theory (.thy) files only.
The assignment is take-home. This does NOT mean you can work in groups. Each submission is personal. For more information, see the plagiarism policy: https://student.unsw.edu.au/plagiarism
Submit using give on a CSE machine: give cs4161 a2 files …
For example:
give cs4161 a2 a2.thy a2_fmap.thy
For this assignment, all proof methods aand proof automation available in the standard Isabelle distribution is allowed. This includes, but is not limited to, simp, auto, blast, force, and fastforce.
However, if you’re going for full marks, you shouldn’t use ”proof” methods that bypass the inference kernel, such as sorry. We may award partial marks for plausible proof sketches where some subgoals or lemmas are sorried.
If you use sledgehammer, it’s important to understand that the proofs suggested by sledgehammer are just suggestions, and aren’t guaranteed to work. Make sure that the proof suggested by sledgehammer actually terminates on your machine (assuming an average spec machine). If not, you can try to reconstruct the proof yourself based on the output, or apply a few manual steps to make the subgoal smaller before using sledgehammer.
Note: this document contains explanations of the problems and your assignment tasks. The full set of definitions can be found in the associated Isabelle theory files.
Hint: there are hints at the end of this document. 0 Introduction
The garbage collector is the most important runtime component for programming languages with automatic memory management. The role of the garbage collector is to detect when data allocated on the heap is no longer in use, and free it. This liberates the programmer from having to juggle error-prone mallocs and frees
In this assignment, we will verify (a model of) a mark-and-sweep garbage collector.
This assignment spans over two theory files, a2_fmap.thy and a2.thy. Both files contain ques- tions, and, in particular, in a2_fmap.thy, the library development and questions are interleaved, so make sure you go through the file and attempt them all!
1 Finite map library (22 marks)
We will build our model of a garbage collector using a library of finite maps. A finite map is a partial map whose domain is finite. In Isabelle, a partial map (type ′a ⇀ ′b) is implemented
Programming Help
using an option type: if f has type ′a ⇀ ′b and x is in the domain of f (i.e., f is defined for x), there exists y such that f x = Some y. If f is not defined for x, we have f x = None.
In a2_fmap.thy, the type of finite map (′a, ′b) fmap is defined using typedef, and various oper- ations on fmaps are defined and their properties are proved.
Explain how the type fmap is defined as an example of what you learned in the lecture. Also give a brief description of the lemmas Isabelle generates. What exactly is lookup? (4 marks)
Prove the extensionality lemma for lookup (3 marks) (Vx.lookupfx =lookupgx)=⇒f =g
fmap-filter P f is a fmap whose domain is the domain of f restricted only to x such that P x holds. Prove that the domain of fmap-filter P f is equal to the domain of f restricted to P. (4 marks)
fdom (fmap-filter P m) = Set.filter P (fdom m)
fmap-of converts a (′a × ′b) list to a (′a, ′b) fmap. Prove simplification rules for fmap-of. (3 marks) fmap-of [] = fempty
fmap-of ((k, v) # kvs) = fupd k v (fmap-of kvs)
Prove a lemma about fmap-keys and fpred. (5 marks) fpred P (fmap-keys f m) = fpred (λa b. P a (f a b)) m
fmmap f m takes a function f:′b ⇒ ′c and an fmap m:(′a, ′b) fmap and returns an fmap of type (′a, ′c) fmap. Prove the following equality about lookup and fmmap. (3 marks)
lookup (fmmap f m) x = map-option f (lookup m x) Garbage collector specification (30 marks)
We will use natural numbers to represent memory addresses (politely ignoring the inconvenience that real memory is finite). A block is a flat piece of data that resides on the heap; for example, in a Java runtime, blocks might represent objects. At this level of abstraction, we don’t particularly care how blocks are laid out in memory. All we need to know is that blocks contain a list of pointers to other blocks, and some (non-pointer) data:
type-synonym ′data block = nat list × ′data
We use a type variable to represent the non-pointer data, because we do not (yet) care about
its structure. A heap is a finite map that associates memory addresses to blocks: type-synonym ′data heap = (nat, ′data block) fmap
The intuition is that lookup h a = Some b holds if, in the heap h, if we dereference the pointer a, we’ll find the block b. If lookup h a = None holds, that means that there is no block at address a.
2.1 Reachability
The relation reach specifies the set of reachable addresses in a heap h from a given set of roots. Intuitively, the roots are memory addresses that can be reached directly from outside the heap; a real-world example is a heap pointer residing in a stack frame.
inductive-set reach :: ′data heap ⇒ nat list ⇒ nat set for h roots where
reach-root[intro]: a ∈ set roots =⇒ a ∈ reach h roots
| reach-step[intro]: [b ∈ reach h roots; lookup h b = Some(as,data); a ∈ set as] =⇒ a ∈ reach h roots The first rule states that the roots themselves are always reachable. The second rule states that
we can reach an address by following a pointer from within a reachable block. Prove that the reach relation enjoys the following properties:
(a) If we have no roots, nothing is reachable. (3 marks)
a ∈ reach h [] =⇒ False
(b) Reachability is monotonic wrt. the roots. (3 marks)
[a ∈ reach h roots; set roots ⊆ set roots′] =⇒ a ∈ reach h roots′
(c) Any address reachable from a reachable address is reachable. (3 marks)
[a ∈ reach h roots; b ∈ reach h [a]] =⇒ b ∈ reach h roots
(d) If the roots contain a dangling pointer x, this adds no reachable elements except the
dangling pointer itself. (3 marks)
[lookup h x = None; a ∈ reach h (x # roots)] =⇒ x = a ∨ a ∈ reach h roots
(e) Reachable addresses can be found either in the roots or in a block. (4 marks)
x ∈ reach heap roots =⇒ x ∈ set roots ∨ (∃block. block ∈ fran heap ∧ x ∈ set (fst block))
2.2 Collection
We can now specify the expected behaviour of a garbage collector as follows:
fun collect :: ′data heap ⇒ nat list ⇒ ′data heap where
collect h roots = frestrict-set (reach h roots) h
The garbage collector restricts the heap h to the set of reachable addresses. Or, for a more operational intution, it removes all unreachable addresses from the heap.
(f) Consider the following example heap, which is illustrated in Figure 1: ex1-heap = fmap-of [(0, [1, 2], ()), (1, [0], ()), (2, [2], ()), (3, [0], ())]
Define a set of addresses ex1-reach, which is the set of reachable addresses from the root 0. (3 marks)
(g) Use your answer to the previous question to show that after garbage collection, the ex- pected addresses are all reachable. (3 marks)
ex1-reach ⊆ fdom (collect ex1-heap [0])
(h) Show that garbage collection is sound, in the sense that it doesn’t collect reachable blocks
(preserves reachability). (3 marks)
n ∈ reach h roots =⇒ n ∈ reach (collect h roots) roots
(i) Show that garbage collection is complete, in the sense that it collects all garbage. (3 marks)
[n ∈ fdom h; n ∈/ reach h roots] =⇒ n ∈/ fdom (collect h roots)
(j) Show that running the garbage collector again does nothing. (2 marks)
collect (collect h roots) roots = collect h roots 3
12020 0123
Figure 1: Illustration of the heap from Question 2(g). Blocks are represented as rectangles partitioned into data segments and pointers. The number below each block is its address in the heap. The arrows show where pointers point.
3 Garbage collector refinement (48 marks)
In this part, we will elaborate the garbage collector specification by introducing more implemen- tation details, and prove our elaboration sound with respect to our specification. This process is called refinement. In a real-world application, we could perform more and more refinement steps, adding further implementation details until we’re down to the machine code level. For the sake of your sanity, we’ll only do this one step in this assignment.
In a mark-and-sweep collector, the first step is to traverse the heap and mark all reachable blocks. We assume all blocks have a special tag bit for this purpose, which is only used internally by the GC. When the marking phase finishes, a sweep is conducted: the entire heap is traversed top-to-bottom. In this process, any unmarked block is freed and marked blocks are kept and their markings are removed.
For the sweep process, we need blocks to additionally contain this tag bits. Here it is handy that we chose a type variable for the data, which we can now instantiate to (bool × ′data) block, on the understanding that the boolean contains the tag bit. The following auxiliary functions test whether a block is marked, mark it, and unmark it, respectively:
fun marked :: (bool × ′data) block ⇒ bool where marked(ptr,(tag,data)) = tag
fun mark-block :: (bool × ′data) block ⇒ (bool × ′data) block where mark-block(ptr,(tag,data)) = (ptr,(True,data))
fun unmark-block :: (bool × ′data) block ⇒ (bool × ′data) block where unmark-block(ptr,(tag,data)) = (ptr,(False,data))
The following inductive relation defines the behaviour of the marking phase:
inductive mark where mark-done[intro!,simp]: mark heap [] heap
| mark-dangling[elim]: [lookup heap root = None;
mark heap roots new-heap]
=⇒ mark heap (root#roots) new-heap
| mark-marked[intro]:
[lookup heap root = Some block;
marked block;
mark heap roots new-heap]
=⇒ mark heap (root#roots) new-heap
| mark-unmarked[intro]:
[lookup heap root = Some block;
¬marked block;
mark (fupd root (mark-block block) heap) block) new-heap] =⇒ mark heap (root#roots) new-heap
The intention is that mark old-heap roots new-heap is true if the result of marking old-heap, starting from roots, is new-heap. The new heap will contain the same data and blocks as the old heap, except reachable blocks become marked.
The argument roots maintains a list of memory addresses we need to visit in the future. When we visit an address, if it points to a marked block, we ignore it (on the understanding that it’s already been visited). If it points to an unmarked block, we mark it, and add its children to the roots.
3.2 Unmarked reachability
To connect the GC specification reach with the marking implementation mark, the following definition turns out to be useful:
abbreviation unmarked-root where
unmarked-root ≡ λh root. case lookup h root of None ⇒ True | Some block ⇒ Not(marked block)
inductive-set ureach:: (bool × ′data) heap ⇒ nat list ⇒ nat set for h roots where
ureach-root[intro]: [a ∈ set roots; unmarked-root h a] =⇒ a ∈ ureach h roots
| ureach-step[intro]: [b ∈ ureach h roots; lookup h b = Some(as,(False,data)); a ∈ set as; unmarked-root h a]
=⇒ a ∈ ureach h roots
Intuitively ureach denotes reachability via unmarked blocks (u-reachability for short). It’s like
reach, except you’re not allowed to visit marked blocks.
The following properties of it will be handy, many of which are similar to those for reach:
(a) U-reachability is monotonic wrt. the roots. (3 marks)
[a ∈ ureach h roots; set roots ⊆ set roots′] =⇒ a ∈ ureach h roots′
(b) If the roots contain a dangling pointer x, this adds no u-reachable elements except the
dangling pointer itself. (3 marks)
[lookup h x = None; a ∈ ureach h (x # roots)] =⇒ a = x ∨ a ∈ ureach h roots
(c) Removing the address of a marked block from the roots does not impact u-reachability. (3
[lookup h x = Some (ptrs, True, tags); a ∈ ureach h (x # roots)] =⇒ a ∈ ureach h roots
(d) If an address can be u-reached after marking an unmarked block and adding its children
to the roots, it could be u-reached before too. (5 marks) 5
Computer Science Tutoring
[lookup heap root = Some (a, False, b); x ∈ ureach (fupd root (a, True, b) heap) (roots @ a)] =⇒ x ∈ ureach heap (root # roots)
(e) If an address can be u-reached from an unmarked root, marking this address and adding its children as roots preserves u-reachability of other addresses. (6 marks)
[lookup heap root = Some (a, False, b); x ∈ ureach heap (root # roots)] =⇒ x ∈ ureach (fupd root (a, True, b) heap) (roots @ a) ∨ x = root
(f) Running mark will mark all blocks that are u-reachable through unmarked blocks: (7 marks)
mark heap roots newheap =⇒ newheap = fmap-keys (λptr (ptrs, tag, data). (ptrs, tag ∨ ptr ∈ ureach heap roots, data)) heap
(g) U-eachability implies reachability. (3 marks)
a ∈ ureach h roots =⇒ a ∈ reach h roots
(h) Reachability implies u-reachability, if all blocks are unmarked. (6 marks)
[a ∈ reach h roots; fpred (λptr block. ¬ marked block) h] =⇒ a ∈ ureach h roots ∨ a ∈ set roots
(i) mark marks all reachable blocks, if everything is initially unmarked. (6 marks)
[mark heap roots newheap; fpred (λptr block. ¬ marked block) heap] =⇒ newheap =
fmap-keys (λptr (ptrs, tag, data). (ptrs, ptr ∈ reach heap roots, data)) heap
Our characterisation of the sweeping phase will be considerably more abstract than the marking; for example, we don’t worry about characterising the step-by-step behaviour of the sweeping function.
A sweep removes all marked blocks (with fmap-filter) and then unmarks all blocks (with fmmap). definition sweep :: (bool × ′data) heap ⇒ (bool × ′data) heap where
sweep h = fmmap unmark-block (fmap-filter (Not o unmarked-root h) h)
This allows us to conclude our refinement story by showing that together, mark and sweep
implements collect.
(j) Prove the following theorem statement. (6 marks)
[mark h roots h′; fpred (λptr block. ¬ marked block) h] =⇒ collect h roots = sweep h′ 4 Hints
• The lemma you prove for 1(a), called lookup-ext, is often useful in proving lemmas for the later questions. Applying it as an introduction rule tends to unlock a lot of simplification.
• For proving mark-correct-aux proof, the ureach lemmas are useful.
• Many proofs will require induction of one kind or the other. Other than inducting on datatypes directly, you may find it useful to do induction on inductively defined sets and relations such as reach and mark. The induction rules for these are automatically generated by Isabelle.
浙大学霸代写 加微信 cstutorcs
You can apply these induction rules as elimination rules, e.g. apply(erule reach.induct), but a more convenient and flexible alternative is
apply(induct rule: reach.induct)
which allows you to specify which variables should not be all-eliminated using e.g.
apply(induct arbitrary: x y rule: reach.induct)
• Not everything needs an induction.
• The assumptions of theorems stated in the assumes-show format are accessible via the fact named assms. For example, you can do simp add: assms or rule assms(1). The assumptions can be added directly to the goal state by beginning your proof with the command apply(insert assms) or using assms; that is usually what you want to do before starting an induction.
• The equivalent of spec for the meta-logic universal quantifier, if you need it, is called meta_spec.
• For some exercises, you will likely need additional lemmas to make the proof go through. Part of the assignment is figuring out which lemmas are needed.
• Make use of the find_theorems command to find library theorems. You are allowed to use all theorems proved in the Isabelle distribution.
5 Acknowledgements
This assignment is inspired by Magnus O. Myreen’s paper Reusable verification of a copying collector. The finite map library is based on a finite map library by Lars Hupel.