Skip to Content.
Sympa Menu

coq-club - [Coq-Club] wasting natural fuel is costly

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] wasting natural fuel is costly


Chronological Thread 
  • From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] wasting natural fuel is costly
  • Date: Wed, 16 Dec 2020 20:31:10 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f174.google.com
  • Ironport-phdr: 9a23:SozaOBaiJVKmD2+xR+PDrJD/LSx+4OfEezUN459isYplN5qZrsyybnLW6fgltlLVR4KTs6sC17OJ9fmxAidZvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txjdu80YjIdtN6o8yAbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyvpxJx3ZPaboKSOvVxYqzTcsgXRXZDU8tLSyBMGJ+wY5UJAuEcPehYtY79p14WoBewBwmsA+Xvyj5LhnDo2a01zfouHBrJ3AwlBd0OsXDUoM/pO6cVVOC5wrTDwDLBb/NR3zf96YvIfQ4lof6SQ719asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRm44YylDK+CpnzYopOdC1SEx2bNC4HZZfqy2XN5Z6TM0+T2xsuSs0yr4LtICncCUW1Zkr2RzSZuCafoWG4h/tWuCcKip7inJ9YL+zmQq+/Ey6xuD/VsS4ykhGojRbntXWq3wA1RPe5tCZRvZ84kutxDOC2x3X5+5YJE05mqvWJ4I9zrM1i5YevkfOEyrylUj1kqObdkAp9+q15OTpbLXro5GcOJFohg7gN6kjlNCwDOUlPgUIQmOV4/6z1Kf58k38WLhKjuM5kq3esJ3CIMQUvK+5AwtM3oY66BazEi6q0NoFkXQFI19JYh2Hj4/uO1HBJPD3E+2zjEirkDdu3/zGP7vhDYvRLnXbjrvtYbJw51RfxQcz19xT+YxYBq8bLP7uWEL8u8TUDhojPAy1x+bnBs991oQbWW+XAK+ZN6XSsV6L5u0xJ+mDepEatS3yK/gg/fHujHs5lUUBcqmu2JsbcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9fIKdHvwIdSjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3Rr2caspTi19Vx6uD7mhQ79DgyBMOYmSnZTWZyn2AFQzI79K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrkiUoGgakf6Zt6MDW2ebJCjCDA1QMg2xoZXMUl4EtSmyBvE2njzWuJHp/mwHJUxt5nk8T3xKsJ6kSiU0aAgixw/QZIKOzT52uhw8A/cA4OPmEKcxf7zKfYsmRXV/WLG9lKg+VlCWVcpA6rAVHEbIEDRqIah6w==

I have a recursive Gallina function that uses a nat-typed fuel arg to
guarantee termination. In cases where the function terminates prior to
running out of fuel, I've found that larger than necessary fuel args
are very costly. For example, with a fuel value of 100, the function
takes 30 times longer than if the fuel value is 10 (neither runs out of
fuel, all other args are the same). In both cases, the computation was
done with vm_cast_no_check. Nothing is done with the fuel arg other
than the usual "match fuel with 0 => done | S n => loop n"
recursion idiom.

I guess this is probably due to the overhead of nats in Gallina. But
it is still surprising to me, considering that if I wrote a function to
traverse the first 8 links in a list, I wouldn't expect it to take 30
times longer with a 100-element list than a 10-element list.

Is there a way around this? I'd like to use a constant fuel value
that is plenty large enough, without having to compute one from the
function's arguments that is just barely large enough.



Archive powered by MHonArc 2.6.19+.

Top of Page