source: etc/campbell/dev-notes/2012-08-22-cost-label-checking.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 3.7 KB
Line 
1I've been proposing that we add a function to check whether a function is
2soundly labelled in RTLabs, for three reasons:
3
4 1. If we run short of time we can use it as a runtime check rather than proving
5    that the Clight programs are soundly labelled and that sound labelling is
6    preserved.
7
8 2. It will be faster; in particular, we'll be able to test whether some
9    programs are soundly labelled before attempting to prove the transformations
10    correct.
11
12 3. We'll have the option of importing RTLabs code.
13
14The requirements for labels at the head of the function and after each branch
15are easy to check, but the bound on the number of instructions until a cost
16label is more difficult.  However, it does live in Prop, so we don't actually
17need to calculate and store the bound, just prove that the checker says yes
18iff it exists.
19
20So, the obvious checker is to traverse the function from the entry point
21keeping a set of the CFG labels seen since the last cost label, and failing if
22we spot a loop without a cost label.  We then need to prove the existence or
23otherwise of a bound.
24
25To make this a little easier, perhaps we can keep the labels in a list (with a
26proof that they are not cost labels, then reuse the bad_label_list definition
27and loop_soundness_contradiction lemma from the unrepeating proof in
28RTLabs/Traces.ma to construct the proof that there's no bound.
29
30Questions:
31
32  - Intuitively, the control flow graph ought to be connected, but do we check
33    that, require it, or cope without it?  If we want to reject functions with
34    dead code we'll have to add that to the spec.  Otherwise we'll need to
35    check all of the components of the CFG in order to prove that there's a
36    bound for every instruction.
37
38
39-----
40
4127th Aug:
42
43There's a problem in the above: when we see a branch we must check both branches
44for a bound, so we can't just trace the function one instruction at a time from
45the start.  Unless, that is, we check before that each branch is followed by
46cost labels.  We already do that, so we can just do one at a time.
47
48[It gets a bit sketchy below because I started trying a couple of different
49 directions, then just wrote the code instead.  See the code for the final
50 version.]
51
52So, we
53
54 - Write a checking function which takes a set of CFG labels which haven't been
55   checked yet (but are cost labels, or successors of cost labels?), a list
56   giving a string of (successive) labels which we are currently looking for
57   a cost label for, and a set of labels which we have already got a bound for.
58
59   It looks at the next instruction, and
60     + for cost labels moves the list into the set of labels we have a bound
61       for and continues from the successor of the cost label (with the cost
62       label in the list),
63     + for branches moves the list into the set of labels including the branch
64       itself and continues with one of the branches and puts the other into
65       the set of labels to check
66     + for everything else
67
68
69 a function which checks for a bound for a particular label in the CFG by
70saying yes if it's a branch (because the prior check means the successors are
71cost labels); says yes if it's a return statement; says yes if the (necessarily
72single) successor has already been checked; says yes if the successor is a cost
73label; says no if it's in the list of labels being checked; recursively checks
74the successor otherwise.  How to witness termination?  One possibility is
75|set of nodes to check|.
76
77
78Keep set of unchecked nodes rather than checked nodes because we only need
79an emptiness check (by cardinality?) and a choice fn, rather than equiv
80checking and minus (we already have that, but we'd need to do it every outer
81iteration and reason around it).
Note: See TracBrowser for help on using the repository browser.