source: etc/campbell/dev-notes/2013-02-25-sim-relation-properties-in-femeasurable.txt @ 2735

Last change on this file since 2735 was 2735, checked in by campbell, 6 years ago

Note about loose end in FEMeasurable.

File size: 1.6 KB
Line 
1In FEMeasurable.ma I have
2
3  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 →
4      pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2;
5  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 →
6      pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2;
7  (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *)
8  ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 →
9      pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2;
10
11as some of the hypotheses expected for passes in the front-end.  The labelling
12property is reasonable - cost labels can't disappear - but the classification
13(and hence whether a state is "normal"; ms_rel_normal could be derived from
14ms_rel_classify) is less certain.
15
16For example, in Cminor → RTLabs the label statements (for goto targets, not
17costs) disappear in favour of using the graph label for the translation of the
18enclosed statement; but we've no guarantee that the state for the enclosed
19statement will have the same classification as a label.  Fortunately I think
20that we never encounter a call or return in this fashion.
21
22Where are these assumptions used?
23
241. showing intensional trace preservation for the expansion of normal steps;
25   this can be replace by an extra clause in the simulation hypothesis requiring
26   the first state to be normal when there is at least one step
27
282. showing that call (resp. return) states are matched by call (return) states;
29   this is a reasonable specialisation of ms_rel_classify
30
313. constructing will_return_aux in the cost label case (could use fact that
32   cost labels are "normal" states instead?)
Note: See TracBrowser for help on using the repository browser.