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
1Using common/ 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.
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).
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.
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/ 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]?
25Looking at again, that lemma appears to be exactly what we need.
28To do:
30  Ask on list about [1] and [2].
31  Investigate [3].
Note: See TracBrowser for help on using the repository browser.