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
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.
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.
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.
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
Note: See TracBrowser for help on using the repository browser.