source: etc/campbell/dev-notes/2013-02-27-linking-measurable-rtlabs-to-rest.txt

Last change on this file was 3672, checked in by campbell, 3 years ago

I'd been keeping some notes in the repo; didn't commit these before

File size: 1.6 KB
Line 
1Using common/FEMeasurable.ma we expect that we can find a measurable subtrace
2of the RTLabs execution that corresponds to the original Clight one.  Now we
3need to link it to a structured RTLabs subtrace, and then the back-end.
4
5This involves showing that the stack space bound is still respected, the
6observables are preserved (although we still don't have an observables
7function for the ASM; maybe CSC will want something different) and the
8clock difference implied by the costs is maintained (although we should be
9able to show this from the observables).
10
11Thus we need a notion of stack space usage for RTLabs structured traces.  There
12is one for the "joint" languages, which looks like it could be easily reworked
13for arbitrary structured traces [1].  That said, it isn't used anywhere.
14
15For the observables and clock, we should get tlr_rel between the RTLabs
16structured trace and ASM, so however we extract observables from structured
17traces for ASM [2] ought to match what we can get at RTLabs str trace, then
18we can link that with the observables from the measurable version.  We also
19need tlr_unrepeating.  There's already a lemma showing that the labels given
20by flatten_trace_label_return is preserved when tlr_rel holds, but we have
21to relate the sum over tech_cost_of_label in ASM/CostsProof.ma with something
22suitable for RTLabs.  The final lemma in CostsProof looks like it should
23help with this.  Should we use the Σ_{l ∈ trace}(...) notation elsewhere [3]?
24
25Looking at compiler.ma again, that lemma appears to be exactly what we need.
26
27
28To do:
29
30  Ask on list about [1] and [2].
31  Investigate [3].
Note: See TracBrowser for help on using the repository browser.