source: etc/campbell/dev-notes/2012-06-29-cost-label-uniqueness.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: 1.5 KB
1Claudio's desire for exact costs gives us an extra requirement: that
2each label only appears once in the program.  In terms of the
3corresponding ASM statement, the partial map from program counters to
4labels is injective.  This presents two problems:
61. we don't restrict cost labels in the input program (easy);
72. it can't be stated this way for Clight because there are no cost
8   labels (harder).
10For 1 we can just check that no cost labels exists, or implement some
11check for 2 and produce a cost label generator that starts above the
12highest label in the program.
14For 2, some ideas are
16  a) produce a pseudo-pc that is a path to a particular statement/expr
17     (ugh);
18  b) write a function that produces the multiset (realistically, a list
19     of no particular order) of cost labels in a program and have a
20     no-duplicates predicate;
21  c) write a predicate that checks no-duplication directly by keeping a
22     list of previously seen cost labels (and if it's executable then
23     so much the better)
25Cminor is likely to have a guarantee of the same form, so proving
26preservation there should be fine.  But what about the translation to
29Should be OK - we can keep the injectivity as an invariant of the
30generated function along with the fact that it contains the set of cost
31labels from the corresponding code.  Hence when we add code for a new
32cost label statement it must be fresh w.r.t. the already translated
33code.  We could build the predicate carefully to check statements in the
34same order as they are translated to make things easier.
Note: See TracBrowser for help on using the repository browser.