<div dir="ltr">asm_ok (Asm) only.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 18 October 2016 at 16:40, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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).<br><br></div><div>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.<br></div><div><br></div>Ramana, was the reduced timing only on the asm_ok check or on the labelled part as well?<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 17, 2016 at 9:38 AM, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">In that case, I think word_to_stack can just re-use StackStoreAny and StackLoadAny. Maybe a new StackFreeAny primitive should be added too.<br></div><div class="m_147092832828922641HOEnZb"><div class="m_147092832828922641h5"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 17, 2016 at 9:33 AM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Would we really need to use a new register? If at all possible, we<br>
should try to avoid it because getting asm_ok to fail for one of these<br>
is extremely rare (when does one have an enormous stack frame?).<br>
<br>
Could we try to get through this without another reserved register,<br>
e.g. StackLoad could load the constant in the register it'll update<br>
with the load. If I remember correctly, StackStore will only be used<br>
in places where one of the word_to_stack vars are unused. Similarly,<br>
StackFree is used only in places where at least one of the reserved<br>
variables is unused. This suggests that word_to_stack should<br>
potentially decide how stack_remove is to use temporaries.<br>
<br>
Cheers,<br>
Magnus<br>
<div class="m_147092832828922641m_-2868714120474231907HOEnZb"><div class="m_147092832828922641m_-2868714120474231907h5"><br>
On 17 October 2016 at 15:19, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>> wrote:<br>
> I think all three can be implemented most cleanly in stack_remove by<br>
> offloading the constant into a register when it is too big but that will<br>
> require an extra reserved register.<br>
><br>
> On Mon, Oct 17, 2016 at 4:38 AM, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>><br>
> wrote:<br>
>><br>
>> The following commit contains a comment:<br>
>><br>
>>     need to assume something on all stack lookup/store sizes?<br>
>><br>
>> I don't think there should be. Instead the implementation should break<br>
>> problematic stack load/store/shrinks into multiple instructions, eg if<br>
>><br>
>> store arg, [sp+40000]<br>
>><br>
>> is not encodable, then do something like:<br>
>><br>
>> add sp, 20000<br>
>> add sp, 20000<br>
>> store arg, [sp]<br>
>> sub sp, 20000<br>
>> sub sp, 20000<br>
>><br>
>> Is this possible?<br>
>><br>
>> Cheers,<br>
>> Magnus<br>
>><br>
>> ---------- Forwarded message ---------<br>
>> From: GitHub <<a href="mailto:noreply@github.com" target="_blank">noreply@github.com</a>><br>
>> Date: Mon, 17 Oct 2016 at 07:13<br>
>> Subject: [CakeML/cakeml] b835dc: Move asm_ok up to word_to_stack<br>
>> To: <<a href="mailto:commits@cakeml.org" target="_blank">commits@cakeml.org</a>><br>
>><br>
>><br>
>>   Branch: refs/heads/asm_ok<br>
>>   Home:   <a href="https://github.com/CakeML/cakeml" rel="noreferrer" target="_blank">https://github.com/CakeML/cak<wbr>eml</a><br>
>>   Commit: b835dc96e0442cc883b47044e01fd4<wbr>92253c0244<br>
>><br>
>> <a href="https://github.com/CakeML/cakeml/commit/b835dc96e0442cc883b47044e01fd492253c0244" rel="noreferrer" target="_blank">https://github.com/CakeML/cake<wbr>ml/commit/b835dc96e0442cc883b4<wbr>7044e01fd492253c0244</a><br>
>>   Author: Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>><br>
>>   Date:   2016-10-17 (Mon, 17 Oct 2016)<br>
>><br>
>>   Changed paths:<br>
>>     M compiler/backend/lab_to_target<wbr>Script.sml<br>
>>     M compiler/backend/proofs/stack_<wbr>to_labProofScript.sml<br>
>>     M compiler/backend/semantics/lab<wbr>PropsScript.sml<br>
>><br>
>>   Log Message:<br>
>>   -----------<br>
>>   Move asm_ok up to word_to_stack<br>
>> - there are 3 probably unprovable cheats to do with over sized stack<br>
>> arguments<br>
>><br>
>><br>
>> ______________________________<wbr>_________________<br>
>> Commits mailing list<br>
>> <a href="mailto:Commits@cakeml.org" target="_blank">Commits@cakeml.org</a><br>
>> <a href="https://lists.cakeml.org/listinfo/commits" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/commits</a><br>
><br>
><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br></blockquote></div><br></div>