source: etc/campbell/dev-notes/2012-03-22-finite-memory.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.6 KB
Line 
1It was mentioned at the review that the finite memory of the target could be a
2difficulty for proving correctness (we already knew this and had a little
3discussion of it before, but it wasn't definitively resolved and I think we may
4have skipped it in the proof document).  I looked at a couple of pieces of work
5that go to concrete memory:
6
7  - CompCertTSO has concrete pointers and memory allocation failure, but this
8    appears to work by non-determinism - I think any allocation encountered in
9    the abstract machine for the source can fail, so target programs can fail
10    at any allocation.  If I'm right, this means that you could prove the same
11    correctness theorem for a "compiler" that merely produces a program that
12    attempts an impossible memory allocation (assuming that there's a
13    corresponding allocation early enough in the source semantics).
14
15    (Then again, maybe that's not possible because the ASM might still be
16    non-deterministic enough to require allocation to "succeed" in some abstract
17    sense.)
18
19    [28th:] Later parts of the CompCertTSO paper (5.3,5.5) mention that the
20    stack is allocated per-thread and the semantics fails with an out-of-memory
21    error if the stack pointer leaves the allocated memory range.  This roughly
22    corresponds to what I was thinking of, below.
23
24  - Piton requires an initial state be handed to it with an upper bound on the
25    stack sizes (there are two).  The compiler only has to work if it can find
26    enough memory for these.
27
28(Personally, I think a model where the compiled program is allowed to fail if
29the stack pointer runs off the end is a little better.)
Note: See TracBrowser for help on using the repository browser.