ucsd-progsys
WIP update to latest liquid-fixpoint
Don't merge yet (before https://github.com/ucsd-progsys/liquid-fixpoint/pull/696), the LF submodule currently points to a branch of a fork.
This updates LF to the version with compacted sort coercions for Sets, which fixes crashes for PLE-heavy code resulting from missing coercions.
Odd to see the Data.Map.Base slowdown; it doesn't really use Set does it?
@ranjitjhala I think everything after the first ~8 slowdowns is more or less statistical noise, and we should focus first on regaining performance on large benchmarks which do not use Set/Map. I've found out that disabling the coercions just on the Elaborate code path (while keeping them on Checkable) is enough to get the perf back, so the plan is currently to automatically decide whether the elaborator should perform the full coercion on the environment based on whether Set/Map sort symbols are used in it.
After some investigating, I've discovered that the environment coercion on the Elaborate code path is the biggest offender in terms of performance and moved it earlier to the point of environment creation. I think the charts look much better now:
Great, thank you!!!
- Ranjit.
On Tue, Jul 9, 2024 at 8:09 AM Alex Gryzlov @.***> wrote:
After some investigating, I've discovered that the environment coercion on the Elaborate code path is the biggest offender in terms of performance and moved it earlier to the point of environment creation. I think the charts look much better now:
filtered.svg (view on web) https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/assets/321557/bbc3b233-ae1a-481f-abbb-65d0d2b140c5__;!!Mih3wA!HX_ZbhqZdIxzq4LQCULEsB0rZplWH16YanBsbTclSf_IA7a-P1w1nLgFcmOGz3BxyLyDMYkxmAjnViTLy4LA1u7X$ bot.svg (view on web) https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/assets/321557/1613604d-dd9e-41bd-bd28-db011c1e465d__;!!Mih3wA!HX_ZbhqZdIxzq4LQCULEsB0rZplWH16YanBsbTclSf_IA7a-P1w1nLgFcmOGz3BxyLyDMYkxmAjnViTLyymS62Qg$ top.svg (view on web) https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/assets/321557/acb080da-8eae-4b42-a6bb-088110f17fea__;!!Mih3wA!HX_ZbhqZdIxzq4LQCULEsB0rZplWH16YanBsbTclSf_IA7a-P1w1nLgFcmOGz3BxyLyDMYkxmAjnViTLy35FvJ1L$
— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/pull/2302*issuecomment-2217980324__;Iw!!Mih3wA!HX_ZbhqZdIxzq4LQCULEsB0rZplWH16YanBsbTclSf_IA7a-P1w1nLgFcmOGz3BxyLyDMYkxmAjnViTLy0YbG-So$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAL3ISNOHWATGCXMX3ZLP4LRAVCNFSM6AAAAABJO5JA6KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMJXHE4DAMZSGQ__;!!Mih3wA!HX_ZbhqZdIxzq4LQCULEsB0rZplWH16YanBsbTclSf_IA7a-P1w1nLgFcmOGz3BxyLyDMYkxmAjnViTLy-wqFeaU$ . You are receiving this because you were mentioned.Message ID: @.***>
Much better! Let's merge!
BTW, did you add a test that could not run before (i.e., was creating a crash) and passes now? I believe the feature of this PR should close some issues related with sets and SMT crashing!
Much better! Let's merge!
BTW, did you add a test that could not run before (i.e., was creating a crash) and passes now? I believe the feature of this PR should close some issues related with sets and SMT crashing!
Oh yeah, that's a good point, the initial issue was one missing local coercion that I subsequently added to make some PLE-enabled code in dynamic-policies go through. I'll add a minimized form of that code as a new test.
Added a new test and inserted an additional coercion in LF (see https://github.com/ucsd-progsys/liquid-fixpoint/pull/696#issuecomment-2225652088), here are the new performance charts: