source: etc/campbell/dev-notes/2013-02-14-fn-ids-in-semantics-for-stack-space.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: 2.0 KB
1Given the ident → nat map for assigning stack space to functions, we need to
2be able to track the stack space when considering executions of the front-end
5First, recall that the Callstate and Returnstate states are considered the
6actual calls/returns for classification purposes, and are distinct from the
7prior state which executes the corresponding call/return/skip instruction.
8This has the benefit that we don't duplicate expression evaluation / function
9lookup code in order to have separate rules for Internal and External functions
10(although I don't know if that was the original motivation).  It also fits our
11requirement that the first state in the function must be labelled.
13The problem is that the Callstate, Returnstate and intermediate states don't
14remember the identity of the current function, but merely retain its contents.
15Thus using the stack space map is rather difficult.
17Possibilities (in decreasing order of silliness):
19- Move the function lookup from the call instruction to the Callstate.  [Still
20  need to do more for returns (see below for possibilities), but breaks the
21  nice separation between call instruction state and the two Callstate rules,
22  duplicating stuff in the process.]
24- Replace the copy of the function in the state with the identifier/block for
25  it and look it up all of the time.  [About as appealing as it sounds, not
26  least because it will require changes to a lot of proofs.]
28- Put the identifier/block into the states along with a proof that it's the one
29  that gives the right function.  [Nice for eliminating junk states; a bit
30  hairy to work with; and still affects existing proofs.]
32- Put the identifier/block into the states along without a proof that it's the
33  right one.  [Easier; could get into trouble with junk states.]
35- Only put the identifier/block into the Callstate, and track the allocated
36  stack space separately, allowing us to decrement at return by just popping
37  the top size off a list.  [Best so far.]
Note: See TracBrowser for help on using the repository browser.