Re: [PATCH v2] xen/pdx: fix offset-compression merge of a contained range

[Jan Beulich <jbeulich@xxxxxxxx>]

On 05.10.2026 12:27, Weiqi Wang wrote:
> From: Weiqi Wang <weiqi.wang-2@xxxxxxxxxxxxxxxxxxxxxxxxx>
> 
> When sorting and merging overlapping ranges in
> pfn_pdx_compression_setup(), the merged range is set to end where the
> second range ends.  If the second range is fully contained in the first,
> this truncates the first range, and the tail of it is then neither
> compressible nor translated correctly.
> 
> Keep the end of the merged range as the maximum of both ends.
> 
> On x86 the ranges come from the SRAT memory affinity entries, and
> overlapping entries for the same node are tolerated with a warning by the
> NUMA code.  The caller's subsequent coverage check catches the truncated
> range, so the effect is that PDX compression is disabled with a "RAM
> region ... not covered" message rather than memory being mistranslated.
> 
> Add a test case that fails without this change.
> 
> Found with the ESBMC bounded model checker.  The counterexample was
> confirmed by running it natively against the unmodified code.
> 
> Fixes: c5c45bcbd6a1 ("pdx: introduce a new compression algorithm based on 
> region offsets")
> Assisted-by: Claude Code:claude-opus-5-5 # finding the issue with ESBMC, 
> patch creation
> Signed-off-by: Weiqi Wang <weiqi.wang-2@xxxxxxxxxxxxxxxxxxxxxxxxx>

Reviewed-by: Jan Beulich <jbeulich@xxxxxxxx>

I think though that ...

> --- a/tools/tests/pdx/test-pdx.c
> +++ b/tools/tests/pdx/test-pdx.c
> @@ -87,6 +87,18 @@ int main(int argc, char **argv)
>              },
>              .compress = true,
>          },
> +        /* Range contained in a previous one. */
> +        {
> +            .ranges = {
> +                { .start =                                                 0,
> +                  .end   =                          ((1UL << MAX_ORDER) * 1) 
> },
> +                { .start = (1UL << (MAX_ORDER * 2)) |                      0,

... these lines now want padding with two more inner spaces, so that in
particular the multiplication aligns with ...

> +                  .end   = (1UL << (MAX_ORDER * 2)) | ((1UL << MAX_ORDER) * 
> 4) },
> +                { .start = (1UL << (MAX_ORDER * 2)) | ((1UL << MAX_ORDER) * 
> 1),
> +                  .end   = (1UL << (MAX_ORDER * 2)) | ((1UL << MAX_ORDER) * 
> 2) },

... these. Happy to adjust while committing.

Jan