freenode/#clim - IRC Chatlog
Search
3:29:01
nyef``
beach: In your partial-inlining.pdf, in the description of processing the worklist in section 3.2, by "next instruction" do you mean "successor instruction" (the third element of the worklist item)?
3:30:29
beach
Yeah, I am working on improving the description. I think that is one of the items flagged by my favorite coauthor.
3:32:08
nyef``
In the "already inlined" case, when replacing the funcall instruction with the inlined version of the successor instruction, does this imply altering the successor of the inlined instruction to be the successor of the funcall instruction?
3:32:56
nyef``
This particular manipulation of the CFG seems like it should be specified a bit more closely.
3:35:31
beach
The predecessors of the funcall instruction are redirected to the (already) inlined instruction.
3:36:07
beach
Or, you can see it as the FUNCALL instruction being replaced by a NOP with the inlined instruction as its successor.
3:41:09
nyef``
Maybe have an explicit representation of the workqueue in each figure of the example?
3:42:00
beach
I considered that, but so far I haven't found a way that doesn't make it way too crowded. I'll continue investigating possibilities. My favorite coauthor would like the same.
3:44:21
nyef``
The workqueue entries don't need to be four elements wide, the successor is implicit in the nature of the enter instruction.
3:45:22
nyef``
And your mappings no longer need sit above the enter instructions, they become part of the workqueue.
3:45:49
nyef``
With all that, it looks like there's enough whitespace in the bottom right of each figure.
3:50:23
beach
When I see the description of your work on SBCL, it seems like a clean start would make things so much easier.
3:51:18
nyef``
Won't be this week, of course. I've got some paid work to do yet (now that I've finally gotten the specifics nailed down to the point of implementability), and some SBCL stuff to finish fixing.
3:52:17
nyef``
Isn't there some lambda-calculus process analogy to use in the proof of semantics presevation?
3:52:59
nyef``
My brain is kicking up the phrase "incremental alpha conversion", but I don't even know if "alpha conversion" is the right term.
3:55:22
nyef``
If anything, the termination proof seems more obvious than the correctness proof, TBH.
3:58:18
nyef``
Mmm. I'm not sure, either, but I think that it's the weakest part of the paper to that point.
4:00:10
nyef``
Your termination proof relies critically on the number of instructions to be inlined being finite.
4:01:28
nyef``
Yes, it is going to be finite, but I'm not quite a fan of unexamined assumptions like that. (-:
4:04:59
nyef``
... Section 3.4.1 has a verb phrase as the title, section 3.4.2 has a noun as the title.
4:06:06
nyef``
Perhaps "3.4.1 Semantics preservation" or "semantic preservation" or "preservation of semantics"?