[CakeML-Dev] [CakeML/cakeml] b835dc: Move asm_ok up to word_to_stack

[Yong Kiam]

Implementing it in word_to_stack is turning out to be much harder than I
thought because converting from StackLoad -> LoadAny and Store->StoreAny
turns stack offset in terms of numbers into word offsets and the word
offsets used in stack_remove don't seem to match up exactly in the
semantics (maybe I'm implementing it slightly wrong).

I wonder if it is worth just implementing this in stack_remove? Concretely,
StackLoads can use the existing register, StackStore can be implemented in
the slow loopy way by shifting the stack pointer up and down at
max_stack_alloc intervals (and hopefully, that never happens).



On Tue, Oct 18, 2016 at 2:05 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> asm_ok (Asm) only.
>
> On 18 October 2016 at 16:40, Yong Kiam <tanyongkiam at gmail.com> wrote:
>
>> Oh by the way, I should mention the other comment in my commit: I only
>> started moving asm_ok out, but there are also parts of the labelled-asm
>> checks that can/should be moved out (e.g. that compare-and-jumps are okay).
>>
>> Those checks would need more annoying pre-conditions on the
>> well-formedness of configs e.g. (maybe) that flipping comparisons with any
>> offset_ok fixed offset is also offset_ok.
>>
>> Ramana, was the reduced timing only on the asm_ok check or on the
>> labelled part as well?
>>
>> On Mon, Oct 17, 2016 at 9:38 AM, Yong Kiam <tanyongkiam at gmail.com> wrote:
>>
>>> In that case, I think word_to_stack can just re-use StackStoreAny and
>>> StackLoadAny. Maybe a new StackFreeAny primitive should be added too.
>>>
>>> On Mon, Oct 17, 2016 at 9:33 AM, Magnus Myreen <magnus.myreen at gmail.com>
>>> wrote:
>>>
>>>> Would we really need to use a new register? If at all possible, we
>>>> should try to avoid it because getting asm_ok to fail for one of these
>>>> is extremely rare (when does one have an enormous stack frame?).
>>>>
>>>> Could we try to get through this without another reserved register,
>>>> e.g. StackLoad could load the constant in the register it'll update
>>>> with the load. If I remember correctly, StackStore will only be used
>>>> in places where one of the word_to_stack vars are unused. Similarly,
>>>> StackFree is used only in places where at least one of the reserved
>>>> variables is unused. This suggests that word_to_stack should
>>>> potentially decide how stack_remove is to use temporaries.
>>>>
>>>> Cheers,
>>>> Magnus
>>>>
>>>> On 17 October 2016 at 15:19, Yong Kiam <tanyongkiam at gmail.com> wrote:
>>>> > I think all three can be implemented most cleanly in stack_remove by
>>>> > offloading the constant into a register when it is too big but that
>>>> will
>>>> > require an extra reserved register.
>>>> >
>>>> > On Mon, Oct 17, 2016 at 4:38 AM, Magnus Myreen <
>>>> magnus.myreen at gmail.com>
>>>> > wrote:
>>>> >>
>>>> >> The following commit contains a comment:
>>>> >>
>>>> >>     need to assume something on all stack lookup/store sizes?
>>>> >>
>>>> >> I don't think there should be. Instead the implementation should
>>>> break
>>>> >> problematic stack load/store/shrinks into multiple instructions, eg
>>>> if
>>>> >>
>>>> >> store arg, [sp+40000]
>>>> >>
>>>> >> is not encodable, then do something like:
>>>> >>
>>>> >> add sp, 20000
>>>> >> add sp, 20000
>>>> >> store arg, [sp]
>>>> >> sub sp, 20000
>>>> >> sub sp, 20000
>>>> >>
>>>> >> Is this possible?
>>>> >>
>>>> >> Cheers,
>>>> >> Magnus
>>>> >>
>>>> >> ---------- Forwarded message ---------
>>>> >> From: GitHub <noreply at github.com>
>>>> >> Date: Mon, 17 Oct 2016 at 07:13
>>>> >> Subject: [CakeML/cakeml] b835dc: Move asm_ok up to word_to_stack
>>>> >> To: <commits at cakeml.org>
>>>> >>
>>>> >>
>>>> >>   Branch: refs/heads/asm_ok
>>>> >>   Home:   https://github.com/CakeML/cakeml
>>>> >>   Commit: b835dc96e0442cc883b47044e01fd492253c0244
>>>> >>
>>>> >> https://github.com/CakeML/cakeml/commit/b835dc96e0442cc883b4
>>>> 7044e01fd492253c0244
>>>> >>   Author: Yong Kiam <tanyongkiam at gmail.com>
>>>> >>   Date:   2016-10-17 (Mon, 17 Oct 2016)
>>>> >>
>>>> >>   Changed paths:
>>>> >>     M compiler/backend/lab_to_targetScript.sml
>>>> >>     M compiler/backend/proofs/stack_to_labProofScript.sml
>>>> >>     M compiler/backend/semantics/labPropsScript.sml
>>>> >>
>>>> >>   Log Message:
>>>> >>   -----------
>>>> >>   Move asm_ok up to word_to_stack
>>>> >> - there are 3 probably unprovable cheats to do with over sized stack
>>>> >> arguments
>>>> >>
>>>> >>
>>>> >> _______________________________________________
>>>> >> Commits mailing list
>>>> >> Commits at cakeml.org
>>>> >> https://lists.cakeml.org/listinfo/commits
>>>> >
>>>> >
>>>>
>>>
>>>
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161023/243f3e10/attachment.html>