source: etc/campbell/dev-notes/2012-09-10-clight-labelled-states.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.2 KB
Line 
1The overall statement requires that we identify pairs of Clight states that are
2measurable - in the sense that we can identify a chunk of machine code that
3the cost labels provide timing for.  A core part of this is that they must be
4labelled states, so that we can spot the corresponding labels for the machine
5code.
6
7My first notion of a labelled Clight state was a syntactic version of
8identifying states that will produce a cost label when stepped (actually, it
9was even more wrong, but never mind).  However, this can't be right - a cost
10label may appear deep in the statement (in particular, a subexpression of an
11Econd) which corresponds to a point in the machine code rather later than we
12intend.
13
14Instead, we need the labelled states to be those which start with a cost label
15(or better, consist entirely of processing the cost label).  This is easy at
16the moment because they are just the states about to execute Scost, but if we
17embed cost labels into other statements for (e.g.) solving our problem with
18Swhile, then the natural solution becomes to avoid emitting the cost label
19with the Swhile, but add in an Scost statement.  (Note that Sskip is already
20added in this way.)
Note: See TracBrowser for help on using the repository browser.