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

[Yong Kiam]

Oh actually, I see that the second option is exactly what Magnus suggested
in his first reply. I am going to do that instead then.

On Sun, Oct 23, 2016 at 6:32 PM, Yong Kiam <tanyongkiam at gmail.com> wrote:

> 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/a4c23581/attachment-0001.html>