iris-time-proofs merge requestshttps://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests2023-01-03T15:29:52+01:00https://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests/2case study: Okasaki's persistent queues using the physicist method2023-01-03T15:29:52+01:00Armaël Guéneaucase study: Okasaki's persistent queues using the physicist methodI was teaching last week about persistent data structures, which got me thinking about Okasaki's persistent queues.
So here's the code+proof for the structure described in §6.4.2 of the book, the one that uses the so-called "physicist ...I was teaching last week about persistent data structures, which got me thinking about Okasaki's persistent queues.
So here's the code+proof for the structure described in §6.4.2 of the book, the one that uses the so-called "physicist method". It looked easier to implement that the one using the banker method, as here a given version of the queue data structure only features a single thunk.
It was still quite interesting to see how to account for re-entrancy and manage the namespaces/`na_own` tokens, as we do need to reason about thunks forcing other thunks. In the end, a relatively simple strategy suffices here: associate a given thunk with a namespace indexed by an integer `id`. Then, this thunk has the permission to force all thunks of ids less than `id` (and thus is given access to the corresponding `na_own` tokens). When creating a new thunk that wraps an existing thunk, we simply pick the successor of the id of the wrapped thunk as the id for the new thunk.