Thunks and Debits in Separation Logic with Time Credits (original) (raw)

Résumé

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.

Domaines

DOI

Cite 10.1145/3632892 Autre Pottier, F., Guéneau, A., Jourdan, J.-H., & Mével, G. (2024). Thunks and Debits in Separation Logic with Time Credits. Proceedings of the ACM on Programming Languages, 8(POPL), 1482–1508. https://doi.org/10.1145/3632892

Dates et versions

hal-04238691 , version 1 (12-10-2023)

hal-04238691 , version 2 (14-11-2023)

Licence

Identifiants

Citer

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. ⟨10.1145/3632892⟩. ⟨hal-04238691v2⟩

1346 Consultations

603 Téléchargements

Altmetric