Changeset 2482


Ignore:
Timestamp:
Nov 22, 2012, 3:49:39 PM (7 years ago)
Author:
campbell
Message:

Note about front-end simulations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • etc/campbell/dev-notes/2012-10-31-clight-to-cminor.txt

    r2472 r2482  
    5959  Clight with a list of facts about where the entry/exit labels in Cminor go,
    6060  as there is no corresponding information in Cminor continuations/stacks.
     61
     62[22nd Nov:]
     63
     64Form of the simulations:
     65
     66To ensure that we can find the RTLabs measurable subtrace that we're interested
     67in which corresponds to the Clight measurable subtrace that we started with we
     68need to
     69 - ensure that function calls and returns are preserved
     70 - show that we have states corresponding to the start and end states from the
     71   Clight subtrace; that is, the combined simulation relation between Clight
     72   and RTLabs states should include the start of each subtrace, and the ends.
     73
     74We could take a leaf out of the back-end structured trace lifting and obtain
     75results based on classifying states:
     76
     77- From an other/jump state that isn't cost labelled, some 𝑛 steps over
     78  other/jump states that are not cost labelled are simulated by 𝑚 other/jump
     79  steps (possibly containing labelled states that are exposed during the
     80  translation of expressions)
     81- a step from a call state is simulated by 𝑚 steps from a call state (all of
     82  which are other except for the initial call)
     83- a step from a return state is simulated by 𝑚 steps from a return state
     84  (all of which are other except for the initial return)
     85- a step from a cost labelled state is simulated by a single step from a cost
     86  labelled state
     87
     88This should be sufficient to show that the prefix before a measurable Clight
     89subtrace is simulated by the RTLabs program, the first state of the subtrace
     90is in the relation with it's counterpart, and the measurable subtrace is
     91simulated by the RTLabs subtrace, neatly finishing at end states which are in
     92the relation.
Note: See TracChangeset for help on using the changeset viewer.