source: etc/campbell/dev-notes/2012-08-29-cost-label-bug.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: 7.1 KB
Line 
1[See the end!]
2
3We accidentally broke the cost labelling invariants when we removed the looping
4constructs from Cminor in favour of gotos.  The code
5
6  while (e) s;
7
8gets cost labelled as
9
10  seq
11    while (e') c1: s';
12    c2: skip;
13
14where a ' indicates the labelled version of an expr/statment.  When transformed
15into Cminor the while is processed separately from c2:
16
17  seq
18    entry: seq
19      if e'' then c1: s''; goto entry else goto exit;
20      exit: skip;
21    c2: skip;
22
23where '' indicates a labelled Cminor version of whatever.  Now we have an
24extra skip before we encounter c2, which our spec doesn't allow for.
25
26Some possible solutions:
27
28 1. change structured traces to allow for some "free" transitions after a jump
29    (not even sure how you would do that)
30 2. change the RTLabs semantics to make another step whenever a skip is
31    encountered (and probably subsequent semantics because I don't think skips
32    will be eliminated until much later) - will need invariant to prevent loops
33    of skips
34 3. squash skips in RTLabs before cost checking and adjust property for earlier
35    passes to allow skips if we have time to prove them correct
36 4. adjust Clight to Cminor stage to avoid generating skips by returning a label
37    to attach to the next instruction if we're in a seq (otherwise generate a
38    skip, e.g., an unlabelled if_then_else - or enforce cost labelling invariant
39    to show there's always a seq)
40 5. make a more drastic change to the cost labelled, such as a cost-after
41    statement
42
43Actually, it's worse than I thought: according to the way we specify cost
44labelling we ought to have a cost label on the else branch as well as the
45goto destination, but there's no way to represent this in the original Clight.
46Somehow we want to know that the goto is "linear" in the sense that there is
47no other way to reach it, hence no cost label is necessary.
48
49The prototype does this too, but the extra instructions get squashed during
50linearisation.
51
52[7th Sep:]
53
54I'm going to look at the impact of putting the cost labels for after the loop
55into the loop statement constructor itself.  This will solve the problem of
56breaking the cost label after a branch invariant, but leaves the cost label
57after goto problem unsolved.  At present this shouldn't be a big issue because
58it disappears when using the cost labelling check in RTLabs rather than trying
59to use the condition on goto labels.
60
61The rough plan is:
62
631. check other loop constructs
64   a) for any other cost labelling problems, and
65   b) to see if they're suitable for this approach too
66
672. look for code affected by the changes
68   (careful - the code I just wrote for when a Clight state is "labelled" was
69   originally wrong because I missed subtleties about when expressions were
70   evaluated; some are only examined in a continuation)
71   a) semantics
72   b) labelling c) cast simplification d) translation to cminor
73   e) the cost labelled state predicate
74
753. try implementing it
76   a) adapt semantics
77   b) adapt translation
78
79|
80v
81
821. a) and b)
83   while - already know about
84   dowhile - similar, but with skip rather than goto to exit
85   for - the extra seq before the body will make a mess, exit as dowhile
86   break - become gotos, not a problem
87   continue - ditto
88
89   "for" suggests that putting the body cost label into the loop syntax is
90   a good idea too.
91
922. a) should be a matter of adding the appropriate cost label (if any) to the
93      end of the trace - note that we have to do it at places like Sbreak as
94      well as after evaluating the guard
95   b) just stick labels in appropriate places; the simulation will change a
96      bit - the relation will be a little simpler and some of the cost labels
97      will turn up while evaluating the loop constructs rather than as a
98      separate step
99   c) don't expect any real impact - should be oblivious to costs
100   d) just adjust to put in expected cost labels; shouldn't affect the
101      invariants
102   e) Sdowhile is a problem, the initial entry into the loop doesn't go through
103      the same place as the guard, so there isn't a single form of state which
104      always generates a cost label.  This is a bit complicated to sort out
105      because the current code isn't correct, see 2012-09-10.
106
1073.  Added cost label to Swhile for exits, then to ind principle for syntax,
108    in Csem to Kwhile, adjusted step relation (generating Scost rather than
109    baking it into the Swhile rule), similarly Cexec.  CexecSound and
110    CexecComplete only need intros adjusted.  CexecEquiv changed some intros,
111    which because of the way I did it requires some changes of case ordering.
112
113    Then went back and made the costs optional, which I should have done in the
114    first place.  This is a little awkward because we only generate the Scost
115    if there's a cost to emit.
116
117    Replaced addition of cost after Swhile in label.ma with integrated label.
118    A small niggle is that the simulation proof of functional correctness for
119    labelling only allows the addition of cost labels, so we preserve any
120    existing cost label.  This is a little unnecessary, because we'll ultimately
121    want to rule out user provided cost labels so that we can ensure uniqueness
122    of cost labels.
123    Adjust simulation relation accordingly - keeping old cost labels around is
124    rather annoying here.  This involves much more effort than I'd like - you
125    have to adjust the number of steps depending on whether there was already
126    a cost label there.
127    Switch removal requires minor syntactic changes.
128    Cast simplification required a little care for the actual simulation
129    because the next statement is explicitly mentioned, and the optional_cost
130    definition needs to be broken up.
131    Translation to Cminor changed to put exit and cost labels in else branch
132    of the if; updating proof obligations a pain because a few additional
133    goals changed the numbering.
134    This removes one of the skips in the resulting RTLabs, but there's still
135    another from the goto label; see my mailing list email and later note
136    (2012-09-18-goto-label-skips.txt) for details.
137
138----
139
140It's tempting to make Clight statements dependent on a type of labels, then have
141an unlabelled form of syntax where they're just unit and a labelled form where
142they must be present.
143
144----
145
1469th Oct:
147
148This is all a bit of a red herring.  The skips that are important came from the
149Cminor to RTLabs translation.  In particular, the loop removal produced
150unavoidable goto labels between the start of a branch and the cost label,
151because you should encounter the same cost label when exiting a loop regardless
152of whether you fail the loop's conditional expression or use Sbreak.  That
153translation has now been changed to avoid generating skips for labels to fix
154the problem.
155
156There was a second issue: Sdowhile was not in a suitable form - it didn't have
157the cost labels straight after the ifthenelse.  This was fixed by moving the
158ifthenelse to the top, introducing an extra goto label for the body and putting
159in a goto for the initial iteration.  Note that this generates essentially the
160same CFG by RTLabs.  It also fixed a nasty bug where continue would jump to the
161loop body rather than the conditional expression.
Note: See TracBrowser for help on using the repository browser.