* [PATCH v2] xen/pdx: fix offset-compression merge of a contained range
@ 2026-10-05 10:27 Weiqi Wang
2026-10-05 11:54 ` Jan Beulich
2026-10-05 16:13 ` Roger Pau Monné
0 siblings, 2 replies; 3+ messages in thread
From: Weiqi Wang @ 2026-10-05 10:27 UTC (permalink / raw)
To: xen-devel
Cc: roger, jbeulich, andrew.cooper3, anthony.perard, michal.orzel,
julien, sstabellini, lucas.cordeiro, Weiqi Wang
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,
+ },
#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);
if ( i + 1 < nr_ranges )
memmove(&ranges[i], &ranges[i + 1],
--
2.34.1
^ permalink raw reply related [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: 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
end of thread, other threads:[~2026-10-05 16:13 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
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é
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.