source: etc/campbell/dev-notes/2012-10-15-instrumenting-semantics.txt

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

Misc notes.

File size: 1.2 KB
Line 
1To make the correctness statement a proper type, we need to have an instrumented
2version of the Clight semantics.  We want stack space (in particular, to end up
3showing that the max stack space is below a threshold) and execution cost.  They
4don't necessarily have to be done together.
5
6The stack costs should come from an assignment of frame size to function.  The
7execution costs come from the cost_map, which can assign execution costs to the
8trace emitted by each step of the Clight semantics.
9
10Both of these maps are specialised to a particular program, so trying to define
11a full ‘instrumented semantics’ in the style of a fullexec record doesn't make
12sense.  A better prospect is to execute the program normally and use the trace
13and state from each step to keep track of the costs.
14
15There is still a choice over the form of the execution: we can use the existing
16exec_inf definition and examine the execution up to the desired step, or we
17can iterate the step function directly.  These are equivalent (although it may
18be a little easier to eliminate I/O in the latter), and the difference can be
19largely ignored by returning a list of the traces and states up to the step of
20interest.
Note: See TracBrowser for help on using the repository browser.