source: src/RTLabs/MeasurableTraces.ma @ 2677

Last change on this file since 2677 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 1.8 KB
Line 
1include "common/Measurable.ma".
2include "RTLabs/RTLabs_traces.ma".
3
4definition RTLabs_system : preclassified_system ≝
5mk_preclassified_system
6  RTLabs_fullexec
7  (λ_.RTLabs_cost)
8  (λ_. RTLabs_classify).
9
10notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }.
11notation "hbox(‘ ident i : t ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in (? : $t)) }.
12
13(* The start and end states are existentially quantified because the states
14   need to be extended with the shadow stack of functions.  (I'm not sure that
15   was such a great idea now...)  In principle the quantified away part of the
16   stack would be important for stack-space correctness, except that the
17   structured trace will never touch it, only the suffix of the trace will.
18   We could extract the true value from the execution of the prefix anyway. *)
19
20(* XXX: split of observables seem arbitrary *)
21
22theorem measurable_structured_trace : ∀p,m,n,stack_cost,max_stack,obs_pre,obs.
23  measurable RTLabs_system p m n stack_cost max_stack →
24  observables RTLabs_fullexec p m n = Some ? 〈obs_pre,obs〉 →
25  ∃start,end:RTLabs_ext_state (make_global … p).
26    state_at … RTLabs_system p m = Some state start →
27    state_at … RTLabs_system p n = Some state end →
28  ∃tlr:trace_label_return (RTLabs_status (make_global … p)) start end.
29    obs = ‘obs’ tlr.
30
31(* XXX: need some assumption on start to kick off further simulations, presumably
32   from the execution of the prefix? *)
33
34(*
35  There is no clock in the states of rtlabs, instead it's extracted from the
36  whole trace.  Might not match up well with asm?
37 
38  i.e., do we build the clock into the semantics so that it appears in the
39  structured trace (or equiv, use an instrumented semantics), or use the time
40  implict from the observables?
41*)
Note: See TracBrowser for help on using the repository browser.