source: etc/campbell/dev-notes/2012-01-27-tailcalls-in-structured-traces.txt

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

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 1.2 KB
Line 
1Tailcalls present a problem in the production of our structured traces for
2RTLabs programs.  Function calls involve four states of the RTLabs abstract
3machine:
4
5  1. A normal state about to execute one of the function call instructions,
6  2. A call state with the function, arguments and return register made plain,
7  3. A normal state about to execute to execute the return instruction, and
8  4. A return state with the frame elided.
9
10For the purposes of the structured traces the call state is classified as the
11call and the return state the return.  However, with tail calls there is no
12explicit return instruction or state --- it behaves more like a jump.  Worse,
13the call state has no record of the fact that a tail call is happening, so it
14isn't easy to match them up without changing either the semantics, or the
15classification of which state is the "call".
16
17The lack of support for tail calls breaks two things:  the termination proofs
18obtained from the excluded middle aren't going to make sense (because they
19insist on well-bracketing, and we're missing return states), and the
20as_after_return property won't be provable because the return may not match up
21with the function call.
Note: See TracBrowser for help on using the repository browser.