Up
# Module Priority_queue

### Signature

##
include Invariant.S1 with type
'a
t :=
'a
t

Timing wheel is implemented as a priority queue in which the keys are
non-negative integers corresponding to the intervals of time. The priority queue is
unlike a typical priority queue in that rather than having a "delete min" operation,
it has a nondecreasing minimum allowed key, which corresponds to the current time,
and an `increase_min_allowed_key`

operation, which implements `advance_clock`

.
`increase_min_allowed_key`

as a side effect removes all elements from the timing
wheel whose key is smaller than the new minimum, which implements firing the alarms
whose time has expired.

Adding elements to and removing elements from a timing wheel takes constant time,
unlike a heap-based priority queue which takes log(N), where N is the number of
elements in the heap. `increase_min_allowed_key`

takes time proportional to the
amount of increase in the min-allowed key, as compared to log(N) for a heap. It is
these performance differences that motivate the existence of timing wheels and make
them a good choice for maintaing a set of alarms. With a timing wheel, one can
support any number of alarms paying constant overhead per alarm, while paying a
small constant overhead per unit of time passed.

As the minimum allowed key increases, the timing wheel does a lazy radix sort of the
element keys, with level 0 handling the least significant `b_0`

bits in a key, and
each subsequent level `i`

handling the next most significant `b_i`

bits. The levels
hold increasingly larger ranges of keys, where the union of all the levels can hold
any key from `min_allowed_key t`

to `max_allowed_key t`

. When a key is added to the
timing wheel, it is added at the lowest possible level that can store the key. As
the minimum allowed key increases, timing-wheel elements move down levels until they
reach level 0, and then are eventually removed.

type
'a
priority_queue
=
'a t

module
Elt
: sig .. end

`create ?level_bits ()`

creates a new empty timing wheel, `t`

, with `length t = 0`

and `min_allowed_key t = 0`

.

val
length : _ t -> int

`length t`

returns the number of elements in the timing wheel.

val
is_empty : _ t -> bool

`is_empty t`

is `length t = 0`

`min_allowed_key t`

is the minimum key that can be stored in `t`

. This only
indicates the possibility; there need not be an element `elt`

in `t`

with ```
Elt.key
elt = min_allowed_key t
```

. This is not the same as the "min_key" operation in a
typical priority queue.

`min_allowed_key t`

can increase over time, via calls to
`increase_min_allowed_key`

. It is guaranteed that ```
min_allowed_key t <=
Key.max_representable
```

.

`max_allowed_key t`

is the maximum allowed key that can be stored in `t`

. As
`min_allowed_key`

increases, so does `max_allowed_key`

; however it is not the case
that `max_allowed_key t - min_allowed_key t`

is a constant. It is guaranteed that
`max_allowed_key t >= min (Key.max_representable, min_allowed_key t + 2^B - 1`

,
where `B`

is the sum of the b_i in `level_bits`

. It is also guaranteed that
`max_allowed_key t <= Key.max_representable`

.

`min_elt t`

returns an element in `t`

that has the minimum key, if `t`

is
nonempty. `min_elt`

takes time proportional to the size of the timing-wheel data
structure in the worst case. It is implemented via a linear search.

`min_key t`

returns the key of `min_elt t`

, if any.

val
clear : _ t -> unit

`clear t`

removes all elts from `t`

.

`increase_min_allowed_key t ~key ~handle_removed`

increases the minimum allowed
key in `t`

to `key`

, and removes all elements with keys less than `key`

, applying
`handle_removed`

to each element that is removed. If `key <= min_allowed_key t`

,
then `increase_min_allowed_key`

does nothing. Otherwise, if
`increase_min_allowed_key`

returns successfully, `min_allowed_key t = key`

.

`increase_min_allowed_key`

raises if `key > Key.max_representable`

.

`increase_min_allowed_key`

takes time proportional to `key - min_allowed_key t`

,
although possibly less time.

Behavior is unspecified if `handle_removed`

accesses `t`

in any way other than
`Elt`

functions.