Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
Advanced Topics in Software Verification
Assignment 3
We will accept
Isabelle .thy files only. In addition to this PDF document, please refer to the provided Isabelle
template for the definitions and lemma statements.
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 a3 a3.thy
For all questions, you may prove your own helper lemmas, and you may use lemmas proved
earlier in other questions. You can also use automated tools like sledghammer. If you can’t
finish an earlier proof, use sorry to assume that the result holds so that you can use it if you
wish in a later proof. You won’t be penalised in the later proof for using an earlier true result you
were unable to prove, and you’ll be awarded partial marks for the earlier question in accordance
with the progress you made on it.
1 General recursive function (22 marks)
In this assignment, we continue with the theme of garbage collector that we explored in assign-
ment 2. In Question 1, we look into markF, a general recursive function version of the marking
function which was defined as an inductive relation in the assignment 2. Here we need to use
Isabelle’s function command as below and manually prove that the computation of markF does
terminate. To prove termination, we need to define an appropriate measure that decreases with
the each step of the computation.
Recall that, in the assignment 2, we used the following two types, parametrised by a type variable
′data:
type-synonym ′data block = nat list × ′data
type-synonym ′data heap = (nat, ′data block) fmap
For the marking phase, we introduced a flag for marking by instantiating the type variable with
bool × ′data. The block also contains a list of pointers, nat list, pointing to other blocks (see
Figure 1 in the assignment 2). The function markF is defined using the two functions marked
and mark-block as below:
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))
function markF where
markF heap [] = heap
| markF heap (root#roots) =
(case fmap.lookup heap root of
None ? markF heap roots
| Some blk ? if marked blk then markF heap roots
else markF (fupd root (mark-block blk) heap) (roots@fst blk))
1
(a) Complete the definition of markF and prove its termination. For the termination proof,
think which values will change in each loop step. (8 marks)
(b) Prove the mark-correct-aux lemma for markF. (7 marks)
markF heap roots =
fmap-keys (λptr (ptrs, tag, data). (ptrs, tag ∨ ptr ∈ ureach heap roots, data)) heap
(c) Prove the correctness of markF. (7 marks)
fpred (λptr block. ? marked block) heap =?
markF heap roots =
fmap-keys (λptr (ptrs, tag, data). (ptrs, ptr ∈ reach heap roots, data)) heap
Note that the ureach and reach relations defined in the a3 template are identical to the ones in
assignment 2.
2 C verification (78 marks)
In Question 2, we will consider a C version of the marking function, which is defined in the file
gc.c. To keep the assignment manageable, we will concentrate on the properties leading up to
the correctness of mark, but only state, not prove, the final lemma.
2.1 Linked lists
The C code uses the following struct block to model a block (a flat piece of data) in the heap.
For the sake of simplicity, we assume that the actual data it carries is of type int:
struct block {
struct blist *nexts;
int flag;
int data;
struct block *m_nxt;
};
Here the nexts field corresponds to the list of pointers to other blocks that the block is linked
to. The block struct also contains a flag field for marking, as well as the m_nxt (”marked next”)
field which is used for collecting marked blocks in the mark function.
In assignment 2, the list of nexts pointers in the block and the roots for the reachability relation
were modelled using Isabelle’s list datatype. In C, we use the following struct blist for these:
struct blist {
struct block *this;
struct blist *next;
};
which gives a linked list of blocks.
In order to further investigate the behaviour of the mark function, we first need to establish a
correspondence between a blist pointer and an abstract representation of a list in Isabelle/HOL.
We do this by using the following predicate list:
With the semantics given by AutoCorres, The blist pointer is given as a blist-C ptr : a pointer
to a blist-C record, which models the blist struct. This record has two fields, corresponding
to the two fields of the C struct: this-C and next-C. For instance, the selector function this-C
2
has type blist-C ? block-C ptr, i.e. given a blist it returns the block-C pointer this field.
Similarly, the next-C selector functions have type blist-C ? blist-C ptr.
The state type that the AutoCorres-generated functions operate on is called lifted-globals, Au-
toCorres also provides a heap for each type, i.e. here, blist-C heap, heap-blist-C, and block-C
heap, heap-block-C, as well as validity functions, is-valid-blist-C and is-valid-block-C.
The following function, for a given lifted-globals state, tests if a blist-C ptr points to a list whose
pointer-structure corresponds to the given blist-C ptr list. A blist-C ptr list is an abstract list
whose elements are blist-C ptrs. Such a structure gives us an abstract way of talking about the
pointer-structure of a list on the blist-C heap.
primrec list :: lifted-globals ? blist-C ptr ? blist-C ptr list ? bool where
list s p [] = (p = NULL)
| list s p (x#xs) =
(p = x ∧ p 6= NULL ∧ is-valid-blist-C s p ∧ list s (next-C (heap-blist-C s p)) xs)
Prove the following statements:
(a) NULL corresponds to an empty list. (3 marks)
list s NULL xs = (xs = [])
(b) If p is not NULL, p is an element of the list it points to. (3 marks)
[[list s p xs; p 6= NULL]] =? p ∈ set xs
(c) When p is not NULL, the list it points to can be split into head and tail. (3 marks)
p 6= NULL =?
list s p xs =
(? ys. xs = p # ys ∧ is-valid-blist-C s p ∧ list s (next-C (heap-blist-C s p)) ys)
(d) p points to a unique list. (4 marks)
[[list s p xs; list s p ys]] =? xs = ys
(e) The elements in a blist list are distinct. (6 marks)
list s p xs =? distinct xs
(f) Updating a pointer that is not in a blist list does not affect the list. (4 marks)
q /∈ set xs =?
list (heap-blist-C-update (λh. h(q := next-C-update (λ-. v) (h q))) s) p xs = list s p xs
Next, we define a function the-list which, given a state s and a pointer p for which list s p xs
holds for a blist list xs, returns the actual list xs.
definition the-list :: lifted-globals ? blist-C ptr ? blist-C ptr list where
the-list s p = (THE xs. list s p xs)
(g) Prove that updating a pointer that is not in the list does not affect the list in terms of
the-list. (5 marks)
[[q /∈ set xs; list s p xs]]
=? the-list (heap-blist-C-update (λh. h(q := next-C-update (λ-. v) (h q))) s) p =
the-list s p
3
2.2 Correctness of append ′
AutoCorres generates a monadic version of mark, which is named mark ′. Similarly, functions
append ′ and append-step ′, which mark ′ depends on, are also generated. We now prove the
correctness of append-step ′ and append ′, which correspond to the following C functions:
struct blist *append_step (struct blist *l1, struct blist *l2)