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

[Yong Kiam]

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
>> >
>> >
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161018/3c621297/attachment.html>