Thunks and Debits in Separation Logic with Time Credits - INRIA - Institut National de Recherche en Informatique et en Automatique Access content directly
Conference Papers Year : 2024

Thunks and Debits in Separation Logic with Time Credits


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.
Fichier principal
Vignette du fichier
main.pdf (658.61 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04238691 , version 1 (12-10-2023)
hal-04238691 , version 2 (14-11-2023)




  • HAL Id : hal-04238691 , version 2


François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével. Thunks and Debits in Separation Logic with Time Credits. POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom. ⟨hal-04238691v2⟩
208 View
61 Download


Gmail Facebook X LinkedIn More