Thunks and Debits in Separation Logic with Time Credits
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
Abstract
A thunk is a mutable data structure that offers a simple memoization service: it stores either a suspended computation or the result of this computation. Okasaki [1999] presents many data structures that exploit thunks to achieve good amortized time complexity. He analyzes their complexity by associating a debit with every thunk. A debit can be paid off in several increments; a thunk whose debit has been fully paid off can be forced. Quite strikingly, a debit is associated also with future thunks, which do not yet exist in memory. Some of the debit of a faraway future thunk can be transferred to a nearer future thunk. We present a complete machine-checked reconstruction of Okasaki’s reasoning rules in Iris <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msup> <mml:mrow/> <mml:mi>$</mml:mi> </mml:msup> </mml:math> , a rich separation logic with time credits. We demonstrate the applicability of the rules by verifying a few operations on streams as well as several of Okasaki’s data structures, namely the physicist’s queue, implicit queues, and the banker’s queue.