* Re: [PATCH v2] xen/pdx: fix offset-compression merge of a contained range
2026-10-05 10:27 [PATCH v2] xen/pdx: fix offset-compression merge of a contained range Weiqi Wang
@ 2026-10-05 11:54 ` Jan Beulich
2026-10-05 16:13 ` Roger Pau Monné
1 sibling, 0 replies; 3+ messages in thread
From: Jan Beulich @ 2026-10-05 11:54 UTC (permalink / raw)
To: Weiqi Wang
Cc: roger, andrew.cooper3, anthony.perard, michal.orzel, julien,
sstabellini, lucas.cordeiro, Weiqi Wang, xen-devel
On 05.10.2026 12:27, Weiqi Wang wrote:
> From: Weiqi Wang <weiqi.wang-2@postgrad.manchester.ac.uk>
>
> 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@postgrad.manchester.ac.uk>
Reviewed-by: Jan Beulich <jbeulich@suse.com>
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
^ permalink raw reply [flat|nested] 3+ messages in thread* Re: [PATCH v2] xen/pdx: fix offset-compression merge of a contained range
2026-10-05 10:27 [PATCH v2] xen/pdx: fix offset-compression merge of a contained range Weiqi Wang
2026-10-05 11:54 ` Jan Beulich
@ 2026-10-05 16:13 ` Roger Pau Monné
1 sibling, 0 replies; 3+ messages in thread
From: Roger Pau Monné @ 2026-10-05 16:13 UTC (permalink / raw)
To: Weiqi Wang
Cc: xen-devel, jbeulich, andrew.cooper3, anthony.perard, michal.orzel,
julien, sstabellini, lucas.cordeiro, Weiqi Wang
On Mon, Oct 05, 2026 at 11:27:13AM +0100, Weiqi Wang wrote:
> From: Weiqi Wang <weiqi.wang-2@postgrad.manchester.ac.uk>
>
> 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@postgrad.manchester.ac.uk>
> ---
>
> Notes:
> Changes in v2:
> - clarify in the title that this is the offset-compression instance (Jan)
> - parenthesise the test multiplications against the binary ORs (Jan)
>
> Also seen in a real boot: the hypervisor alone under QEMU (pc, 8 GiB),
> built from defconfig, with no -numa and a hand-built SRAT passed with
> -acpitable. Memory affinity entries, all PXM 0:
>
> [0, 3G) [4G, 9G) [5G, 6G) [1T, 1T+1G)
>
> The third entry lies inside the second. The NUMA code prints "overlaps
> with itself" for it and accepts it. Without this patch:
>
> (XEN) PFN compression using lookup table shift 23 and region size 0x200000
> (XEN) range 0 [0000000000000, 000000017ffff] PFN IDX 0 : 0000000000000
> (XEN) range 1 [0000010000000, 000001003ffff] PFN IDX 32 : 000000fe00000
> (XEN) PFN compression disabled, RAM region [0x100000000, 0x23fffffff] not covered
>
> With it, the same output as without the third entry:
>
> (XEN) PFN compression using lookup table shift 28 and region size 0x400000
> (XEN) range 0 [0000000000000, 000000023ffff] PFN IDX 0 : 0000000000000
> (XEN) range 1 [0000010000000, 000001003ffff] PFN IDX 1 : 000000fc00000
>
> tools/tests/pdx/test-pdx.c | 12 ++++++++++++
> xen/common/pdx.c | 5 +++--
> 2 files changed, 15 insertions(+), 2 deletions(-)
>
> diff --git a/tools/tests/pdx/test-pdx.c b/tools/tests/pdx/test-pdx.c
> index 4de8d43d86..8d271a488f 100644
> --- 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,
> + .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) },
> + },
> + .compress = true,
> + },
You place this in the __LP64__ protected section, but AFAICT this is
not needed? Those values all fit in a 32bit integer.
Also, I think the example could be simpler:
/* Range contained in a previous one. */
{
.ranges = {
/* Overlapping ranges. */
{ .start = 0, .end = (1UL << MAX_ORDER) * 2 },
{ .start = 0, .end = (1UL << MAX_ORDER) * 1 },
/* Extra range to force offset compression to be engaged. */
{ .start = (1UL << MAX_ORDER) * 3,
.end = (1UL << MAX_ORDER) * 4 },
},
#ifdef CONFIG_PDX_OFFSET_COMPRESSION
.compress = true,
#else
.compress = false,
#endif
},
FWIW, we could also make the fully contained range not start at 0, to
avoid the sorting from reordering those, but I think that's not
possible given the (current) compare function cmp_node().
> #endif
> /* PDX compression, 2 ranges covered by the lower mask. */
> {
> diff --git a/xen/common/pdx.c b/xen/common/pdx.c
> index e7e16e193e..23655ef3bd 100644
> --- a/xen/common/pdx.c
> +++ b/xen/common/pdx.c
> @@ -393,8 +393,9 @@ bool __init pfn_pdx_compression_setup(paddr_t base)
> (ranges[i - 1].base_pfn + ranges[i - 1].pages) )
> continue;
>
> - ranges[i - 1].pages = ranges[i].base_pfn + ranges[i].pages -
> - ranges[i - 1].base_pfn;
> + ranges[i - 1].pages = max(ranges[i - 1].pages,
> + ranges[i].base_pfn + ranges[i].pages -
> + ranges[i - 1].base_pfn);
The fix LGTM, thanks.
Regards, Roger.
^ permalink raw reply [flat|nested] 3+ messages in thread