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

[Ramana Kumar]

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/20161018/9af64b3b/attachment.html>