Re: noverlay branch

[Stefan Monnier <monnier@iro.umontreal.ca>]

> I had a different idea of tightening the otree invariant to this:
>
>  1) A node's otick must be greater than or equal to its children's.

That's already checked in the current code, right?

>  2) There is no tree->otick, just tree->root->otick.  That is what is
>     incremented when offsets are added.

Sounds good.

>  3) All downward tree traversal propagates offsets and otick.

I think we already do that, but if there are places we missed, then yes,
of course.

Regarding `otick`, I can see 2 more options:
- Get rid of it completely: its sole purpose is to try and keep
  `overlay-start/end` O(1) in the usual case instead of O(log N), but
  I'm not convinced it's worth the cost of propagating `otick` everywhere
  all the time.
- A halfway point is to keep `otick` but update it more lazily,
  i.e. only update it when we do `overlay-start/end` (e.g. in
  `interval_tree_validate`).

> Anyway, thanks for fixing my "thinko" bug in the check_tree code -- I
> had the fix but should have sent it faster.  I didn't actually intend
> for that to be commited yet (pushed it to sr.ht by accident), but maybe
> it helped you chase down the bugs you fixed today?

Yes, pointed out the problem in the tree insertion code, yes.

> Subject: [PATCH 2/2] Add ./configure --enable-checking=overlays

I think this is going overboard.  I'd rather focus on providing good
"everyday checks" (i.e. cheap checks which help document our invariants,
controlled by the normal ENABLE_CHECKING) and leave the rest of the
debugging code under "manual" control rather than expose it as an
`--enable-checking=` option.

My assumption here is that once debugged, this overlay code will stay
untouched for the next many years (based on the past history of our
overlay code).

> +static struct check_subtree_result
> +check_subtree (struct interval_node *node, uintmax_t tree_otick,
> +               int max_depth, ptrdiff_t offset, ptrdiff_t min_begin,
> +               ptrdiff_t max_begin)

This max_depth also sounds to me like over-engineering.

> -  /* We don't check the RB invariants here (neither the absence of
> -     red+red nor the equal-black-depth), so that we can use this check
> -     even while the tree is temporarily breaking some of those invarints.  */
> -  /* Red nodes cannot have red parents.  */
> -  /* eassert (node->parent == ITREE_NULL
> -              || !(node->red && node->parent->red)); */
> +  /* We don't normally check the RB invariants here (neither the
> +     absence of red+red nor the equal-black-depth), so that we can use
> +     this check even while the tree is temporarily breaking some of
> +     those invarints.  You can enable them if you want.  */
> +  if (false)
> +    {
> +      /* If a node is red then both of its children are black.  Red
> +         nodes cannot have red parents.  */
> +      if (node->red)
> +        {
> +          eassert (node->left == ITREE_NULL
> +                   || node->left->red == false);
> +          eassert (node->right == ITREE_NULL
> +                   || node->right->red == false);
> +          eassert (node->parent == ITREE_NULL || !node->parent->red);
> +        }
> +    }

Since we'll be recursing into the children, the first two easserts seem
redundant with the third (IOW the new code just does the same as the old
code, only more verbosely and less efficiently :-( ).
What am I missing?

> +  result.complete = left_result.complete && right_result.complete;
> +  if (result.complete)

I think all calls to `check_tree` should be complete traversals.

Most of the invariants checked in it are already checked incrementally
via sprinkled assertions elsewhere, so it's only really useful when
debugging a concrete known issue where the "local" checks aren't
good enough.

We could also include a few "cheap" calls to `check_tree` via `eassert`
(i.e. calls which we know shouldn't be algorithmically too expensive
because we're already traversing the whole tree for some other reason,
e.g. when killing a buffer (e.g. to verify that, at the end of the day,
we still preversed the RB invariants :-) or maybe during GC).

> +    {
> +      /* Every path from a node to a descendent leaf contains the same
> +         number of black nodes.  Often said this way: all nodes have
> +         the same "black height".  */
> +      eassert (left_result.black_height == right_result.black_height);

IIUC this assertion should be conditionalized in the same way as the
red+red check, since this invariant can be temporarily false.


        Stefan