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$, 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.
Wed 17 JanDisplayed time zone: London change
15:10 - 16:30
|An Iris Instance for Verifying CompCert C Programs
|The Logical Essence of Well-Bracketed Control Flow
|Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen Aarhus University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti NYU, Lars Birkedal Aarhus UniversityDOI Pre-print
|Thunks and Debits in Separation Logic with Time Credits