source: etc/campbell/dev-notes/2012-11-26-top-level-front-end.txt

Last change on this file was 2509, checked in by campbell, 7 years ago

misc note

File size: 2.1 KB
Line 
1We'd like to show that given suitable simulation results about the front-end
2that we can link the measurable Clight subtrace from the statement in
3correctness.ma with an RTLabs structured subtrace.  We've made a few steps
4towards this already by generalising the statement of a measurable subtrace and
5devising some simulation statements for the Clight to Cminor pass that we
6expect should be sufficient to identify the measurable Cminor subtrace.
7
8
9
10We currently fail to handle I/O in several incompatible ways: the correctness
11statement requires execution by some number of steps to be deterministically
12executed without feeding in any input (we could probably add this without too
13much trouble, using the fact that it doesn't go wrong to exclude badly typed
14input); the RTLabs structured traces proofs require the entire trace to be
15I/O free; and the ASM semantics doesn't appear to have any (from a quick look
16it seems that LIN to ASM produces a call to an asm label, but there's no code
17at the label).  A further problem is that we have no high level semantics for
18I/O.  Also, Claudio's comment that this style of I/O is difficult to reconcile
19with intensional behaviour of the chip (especially for timers) still stands.
20
21Some kind of plan:
22 - Use/wrap exec_inf to apply a given sequence of I/O operations during
23   execution and obtain a flat trace
24 - Adjust measurable subtrace definition to cope with this, but only allow the
25   I/O in the prefix/suffix, so that
26 - building the structured trace is much the same as before, but we have to
27   tweak the notion of flat trace used there to allow I/O (which will be ruled
28   out for the part that we're structuring by the measurable subtrace
29   definition)
30 - constrain the correctness result with some predicate on the I/O or whole
31   trace to make the high level behaviour match something that the system
32   might actually do (as would be specified in the ASM interpreter, if it
33   actually did any - this could just enforce the lack of I/O for now)
34
35Perhaps we could deal with mixed intensional / I/O behaviour by including the
36timing information in the latter?
Note: See TracBrowser for help on using the repository browser.