Real-time immutable queue with const time operations #229
Conversation
Kamirus
changed the title
| @@ -0,0 +1,1026 @@ | |||
| /// Double-ended immutable queue with guaranteed `O(1)` push/pop operations (caveat: high constant factor). | |||
| /// Space: `O(size)` as the current implementation uses `values` to iterate over the queue. | ||
| /// | ||
| /// *Runtime and space assumes that `f` runs in O(1) time and space. | ||
| /// *Runtime and space assumes that the `predicate` runs in `O(1)` time and space. |
There was a problem hiding this comment.
I wonder if we should make both Queue.any and Queue.all not preserve order, for efficiency and consistency with RealTimeQueue (or vice versa). Queue.contains doesn't either.
There was a problem hiding this comment.
We could do that, but ideally in another PR, because I know that some might prefer other approach.
Right now, every non-preserving operation in RealTimeQueue is also not preserving in the original pure/Queue. Only filter and filterMap preserve the order here, but not in pure/Queue. This is because of implementation difficulties (not worth to work on that if we might make all operations order preserving in the future)
| /// - `#idles`: the queue is in the idle state, where `l` and `r` are non-empty stacks of elements fulfilling the size invariant | ||
| /// - `#rebal`: the queue is in the rebalancing state | ||
| public type Queue<T> = { | ||
| #empty; |
There was a problem hiding this comment.
https://dl.acm.org/doi/pdf/10.1145/165180.165225 actually doesn't distinguish the #empty...#three cases and just uses a finite list. I wonder if that might improve perf a little, but I guess these are rare cases...
Perhaps Nipkow did this so simplify his proof.
There was a problem hiding this comment.
I've followed this implementation. The paper was not accurate enough.
| case (#two(_, _)) 2; | ||
| case (#three(_, _, _)) 3; | ||
| case (#idles((l, nL), (r, nR))) { | ||
| debug assert Stacks.size(l) == nL and Stacks.size(r) == nR; |
There was a problem hiding this comment.
| debug assert Stacks.size(l) == nL and Stacks.size(r) == nR; | |
| debug assert Stacks.size(l) == nL and Stacks.size(r) == nR; |
I wonder if we should disable this assert since peope are probably all building with debug on.
There was a problem hiding this comment.
Maybe you could check it in the tests instead?
|
I'll leave it up to you whether you want to apply the microoptimization in #307 or not (about 9-10% on bench) |
|
@crusso I've applied the microoptimization + I've inlined reverse inside push/popBack and got -20% savings Instructions
Garbage Collection
|
3 participants
Adds
pure/RealTimeQueuemodule which implements "Real-Time Double-Ended Queue" (formalization code archive) to achieve worst-caseO(1)const-time&space push/pop/peek operations.This implementation avoids performance cliffs that were leading to unexpected cycle/fuel exhaustion.
However, this implementation has worse amortized performance than
pure/Queue. The differences between all three queue implementations are demonstrated in theQueues.bench.mobenchmark.Resolves #149
TODOs:
pure/RealTimeQueueshould be an alternative to thepure/Queue, match the following aspects:pure/Queue) - exception:filterandfilterMappreserve the front-to-back order, whilepure/Queuedoes not