xen/pdx: fix offset-compression merge of a contained range

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, and confirmed by running the
failing case natively against the unmodified code.

Fixes: c5c45bcbd6 ("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>
This commit is contained in:
Weiqi Wang authored and Jan Beulich committed 2026-10-12 09:41:55 +02:00
1 parent a92d2ba89b
commit c161c11875
2 files changed
+19 -2

No files matched your search

+16
View File
@@ -88,6 +88,22 @@ int main(int argc, char **argv)
.compress = true, .compress = true,
}, },
#endif #endif
/* 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
},
/* PDX compression, 2 ranges covered by the lower mask. */ /* PDX compression, 2 ranges covered by the lower mask. */
{ {
.ranges = { .ranges = {
+3 -2
View File
@@ -393,8 +393,9 @@ bool __init pfn_pdx_compression_setup(paddr_t base)
(ranges[i - 1].base_pfn + ranges[i - 1].pages) ) (ranges[i - 1].base_pfn + ranges[i - 1].pages) )
continue; continue;
ranges[i - 1].pages = ranges[i].base_pfn + ranges[i].pages - ranges[i - 1].pages = max(ranges[i - 1].pages,
ranges[i - 1].base_pfn; ranges[i].base_pfn + ranges[i].pages -
ranges[i - 1].base_pfn);
if ( i + 1 < nr_ranges ) if ( i + 1 < nr_ranges )
memmove(&ranges[i], &ranges[i + 1], memmove(&ranges[i], &ranges[i + 1],
Reference in new issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.