[RFC PATCH] xen/pdx: reject regions crossing a lookup table index

[RFC PATCH] xen/pdx: reject regions crossing a lookup table index

[Weiqi Wang]

From: Weiqi Wang <weiqi.wang-2@postgrad.manchester.ac.uk>

pdx_is_region_compressible() only looks up the table entry of the first
page, and checks the region against [pfn_base, pfn_base +
pdx_region_size).  pfn_base need not be aligned to the table index
granularity, so that window can extend into the next index, which belongs
to a different range with a different offset.  A region whose tail lies
there is reported compressible, yet its last page on its own is not, and
translates through the wrong offset.

Also require the first and last page of the region to use the same table
index.

This can be reached from the coverage check in srat_parse_regions() when an
e820 RAM range is not covered by the SRAT ranges, which is the case that
check is meant to catch.

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:
    RFC because this was discussed when the offset compression was reviewed.
    In the v2 thread [1] Jan asked whether pdx_is_region_compressible() is
    correct when a region crosses a lookup table slot boundary.  The thread
    concluded it was not an issue, on the basis that pages contiguous in MFN
    space are also contiguous in PDX space.  The reproducer below is a case
    where that does not hold for the code as merged: the region is reported
    compressible, its last page on its own is not, and that page round-trips
    to a different PFN.
    
    The ranges are as srat_parse_regions() would see them.  The RAM range is
    not covered by either SRAT range, which is the situation the coverage
    check in srat_parse_regions() is meant to detect.  Built from
    tools/tests/pdx like test-pdx-offset, on staging (e4da182973) plus patch
    "xen/pdx: fix merging of a range contained in the previous one":
    
      region [0x75757ffef9, 0x8122007e00) compressible: 1
      last page compressible: 0
      last page: pfn 0x8122007dff -> pdx 0x2122047dff -> pfn 0x2d7ee07dff
    
    With this patch the region is reported not compressible, and
    srat_parse_regions() disables compression.
    
    8<----------------------------------------------------------------------
    /* Build like test-pdx-offset, e.g. from tools/tests/pdx:
     *   gcc -D__XEN_TOOLS__ -DCONFIG_PDX_OFFSET_COMPRESSION \
     *       -I../../include -o repro-window repro-window.c
     * (after generating pdx.h as the Makefile does). */
    #include "harness.h"
    #include "../../xen/common/pdx.c"
    
    int main(void)
    {
        /* Two SRAT-like ranges, in PFNs. */
        pfn_pdx_add_region(pfn_to_paddr(0xdffffe0000UL),
                           pfn_to_paddr(0xe000000000UL - 0xdffffe0000UL));
        pfn_pdx_add_region(pfn_to_paddr(0xc5cde0000UL),
                           pfn_to_paddr(0x4cd7000000UL - 0xc5cde0000UL));
        if ( !pfn_pdx_compression_setup(0) )
            return puts("compression not enabled"), EXIT_FAILURE;
    
        /* A RAM range not covered by either, as srat_parse_regions() checks. */
        unsigned long s = 0x75757ffef9UL, e = 0x8122007e00UL;
    
        printf("region [%#lx, %#lx) compressible: %d\n", s, e,
               pdx_is_region_compressible(pfn_to_paddr(s), e - s));
        printf("last page compressible: %d\n",
               pdx_is_region_compressible(pfn_to_paddr(e - 1), 1));
        printf("last page: pfn %#lx -> pdx %#lx -> pfn %#lx\n",
               e - 1, pfn_to_pdx(e - 1), pdx_to_pfn(pfn_to_pdx(e - 1)));
    
        return pdx_is_region_compressible(pfn_to_paddr(s), e - s) &&
               pdx_to_pfn(pfn_to_pdx(e - 1)) != e - 1 ? EXIT_FAILURE : EXIT_SUCCESS;
    }
    8<----------------------------------------------------------------------
    
    Other callers that rely on the same answer are mem_hotadd_check() and
    the EFI ram_range_valid() check.  I have not run those paths.
    
    One behavioural change to check: with npages == 0 the new condition
    compares against pfn - 1.  The callers I looked at never pass 0.
    
    Model checking (ESBMC, 2 SRAT ranges and 2 e820 RAM ranges, all free
    below 2^40 PFNs, the srat_parse_regions() coverage check modelled) finds
    no accepted RAM page that fails to round-trip with both patches applied.
    It also finds no layout where the coverage check now rejects what setup
    accepted, with RAM equal to the SRAT ranges.  This is bounded to 2 ranges.
    
    The existing tests in tools/tests/pdx pass in both mask and offset mode.
    
    I have not reproduced this in a boot: the layout needs RAM near 2^51
    bytes, which I could not set up under QEMU.
    
    [1] https://www.mail-archive.com/xen-devel@lists.xenproject.org/msg194095.html

 xen/common/pdx.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/xen/common/pdx.c b/xen/common/pdx.c
index 23655ef3bd..52928faa15 100644
--- a/xen/common/pdx.c
+++ b/xen/common/pdx.c
@@ -324,7 +324,8 @@ bool pdx_is_region_compressible(paddr_t base, unsigned long npages)
     unsigned long pfn_base = pfn_bases[PFN_TBL_IDX(pfn)];
 
     return pfn >= pfn_base &&
-           pfn + npages <= pfn_base + pdx_region_size;
+           pfn + npages <= pfn_base + pdx_region_size &&
+           PFN_TBL_IDX(pfn) == PFN_TBL_IDX(pfn + npages - 1);
 }
 
 static int __init cf_check cmp_node(const void *a, const void *b)
-- 
2.34.1

Re: [RFC PATCH] xen/pdx: reject regions crossing a lookup table index

[Jan Beulich]

On 04.10.2026 21:04, Weiqi Wang wrote:
> From: Weiqi Wang <weiqi.wang-2@postgrad.manchester.ac.uk>
> 
> pdx_is_region_compressible() only looks up the table entry of the first
> page, and checks the region against [pfn_base, pfn_base +
> pdx_region_size).  pfn_base need not be aligned to the table index
> granularity, so that window can extend into the next index, which belongs
> to a different range with a different offset.  A region whose tail lies
> there is reported compressible, yet its last page on its own is not, and
> translates through the wrong offset.
> 
> Also require the first and last page of the region to use the same table
> index.
> 
> This can be reached from the coverage check in srat_parse_regions() when an
> e820 RAM range is not covered by the SRAT ranges, which is the case that
> check is meant to catch.
> 
> 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:
>     RFC because this was discussed when the offset compression was reviewed.
>     In the v2 thread [1] Jan asked whether pdx_is_region_compressible() is
>     correct when a region crosses a lookup table slot boundary.  The thread
>     concluded it was not an issue, on the basis that pages contiguous in MFN
>     space are also contiguous in PDX space.  The reproducer below is a case
>     where that does not hold for the code as merged: the region is reported
>     compressible, its last page on its own is not, and that page round-trips
>     to a different PFN.
>     
>     The ranges are as srat_parse_regions() would see them.  The RAM range is
>     not covered by either SRAT range, which is the situation the coverage
>     check in srat_parse_regions() is meant to detect.  Built from
>     tools/tests/pdx like test-pdx-offset, on staging (e4da182973) plus patch
>     "xen/pdx: fix merging of a range contained in the previous one":
>     
>       region [0x75757ffef9, 0x8122007e00) compressible: 1
>       last page compressible: 0
>       last page: pfn 0x8122007dff -> pdx 0x2122047dff -> pfn 0x2d7ee07dff
>     
>     With this patch the region is reported not compressible, and
>     srat_parse_regions() disables compression.
>     
>     8<----------------------------------------------------------------------
>     /* Build like test-pdx-offset, e.g. from tools/tests/pdx:
>      *   gcc -D__XEN_TOOLS__ -DCONFIG_PDX_OFFSET_COMPRESSION \
>      *       -I../../include -o repro-window repro-window.c
>      * (after generating pdx.h as the Makefile does). */
>     #include "harness.h"
>     #include "../../xen/common/pdx.c"
>     
>     int main(void)
>     {
>         /* Two SRAT-like ranges, in PFNs. */
>         pfn_pdx_add_region(pfn_to_paddr(0xdffffe0000UL),
>                            pfn_to_paddr(0xe000000000UL - 0xdffffe0000UL));
>         pfn_pdx_add_region(pfn_to_paddr(0xc5cde0000UL),
>                            pfn_to_paddr(0x4cd7000000UL - 0xc5cde0000UL));
>         if ( !pfn_pdx_compression_setup(0) )
>             return puts("compression not enabled"), EXIT_FAILURE;
>     
>         /* A RAM range not covered by either, as srat_parse_regions() checks. */
>         unsigned long s = 0x75757ffef9UL, e = 0x8122007e00UL;
>     
>         printf("region [%#lx, %#lx) compressible: %d\n", s, e,
>                pdx_is_region_compressible(pfn_to_paddr(s), e - s));
>         printf("last page compressible: %d\n",
>                pdx_is_region_compressible(pfn_to_paddr(e - 1), 1));
>         printf("last page: pfn %#lx -> pdx %#lx -> pfn %#lx\n",
>                e - 1, pfn_to_pdx(e - 1), pdx_to_pfn(pfn_to_pdx(e - 1)));
>     
>         return pdx_is_region_compressible(pfn_to_paddr(s), e - s) &&
>                pdx_to_pfn(pfn_to_pdx(e - 1)) != e - 1 ? EXIT_FAILURE : EXIT_SUCCESS;
>     }
>     8<----------------------------------------------------------------------
>     
>     Other callers that rely on the same answer are mem_hotadd_check() and
>     the EFI ram_range_valid() check.  I have not run those paths.
>     
>     One behavioural change to check: with npages == 0 the new condition
>     compares against pfn - 1.  The callers I looked at never pass 0.
>     
>     Model checking (ESBMC, 2 SRAT ranges and 2 e820 RAM ranges, all free
>     below 2^40 PFNs, the srat_parse_regions() coverage check modelled) finds
>     no accepted RAM page that fails to round-trip with both patches applied.
>     It also finds no layout where the coverage check now rejects what setup
>     accepted, with RAM equal to the SRAT ranges.  This is bounded to 2 ranges.
>     
>     The existing tests in tools/tests/pdx pass in both mask and offset mode.
>     
>     I have not reproduced this in a boot: the layout needs RAM near 2^51
>     bytes, which I could not set up under QEMU.

I don't quite understand this part: SRAT not covering all E820 regions isn't
tied to huge addresses, is it?

>     [1] https://www.mail-archive.com/xen-devel@lists.xenproject.org/msg194095.html

Hmm, indeed you now provide an example of the concern raised there. I think
we indeed ...

> --- a/xen/common/pdx.c
> +++ b/xen/common/pdx.c
> @@ -324,7 +324,8 @@ bool pdx_is_region_compressible(paddr_t base, unsigned long npages)
>      unsigned long pfn_base = pfn_bases[PFN_TBL_IDX(pfn)];
>  
>      return pfn >= pfn_base &&
> -           pfn + npages <= pfn_base + pdx_region_size;
> +           pfn + npages <= pfn_base + pdx_region_size &&
> +           PFN_TBL_IDX(pfn) == PFN_TBL_IDX(pfn + npages - 1);
>  }

... need this extra check (as we want to cope with SRAT and E820 not fully
agreeing). Roger?

Jan

Re: [RFC PATCH] xen/pdx: reject regions crossing a lookup table index

[Roger Pau Monné]

On Sun, Oct 04, 2026 at 08:04:09PM +0100, Weiqi Wang wrote:
> From: Weiqi Wang <weiqi.wang-2@postgrad.manchester.ac.uk>
> 
> pdx_is_region_compressible() only looks up the table entry of the first
> page, and checks the region against [pfn_base, pfn_base +
> pdx_region_size).  pfn_base need not be aligned to the table index
> granularity, so that window can extend into the next index, which belongs
> to a different range with a different offset.  A region whose tail lies
> there is reported compressible, yet its last page on its own is not, and

can there be multiple pages that overlap into the next region?  Using
"its last page on its own is not" makes it look it's only a single
page whose translation is wrong.

> translates through the wrong offset.
> 
> Also require the first and last page of the region to use the same table
> index.

The "Also" at the start of the sentence seems misplaced to me, I would
rather start the sentence with "Require ..."

> This can be reached from the coverage check in srat_parse_regions() when an
> e820 RAM range is not covered by the SRAT ranges, which is the case that
> check is meant to catch.
> 
> Found with the ESBMC bounded model checker.  The counterexample was
> confirmed by running it natively against the unmodified code.

"The counterexample" is not part of the commit log, so it feel odd to
name it here, as people going through the commit history won't see it.

> 
> 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:
>     RFC because this was discussed when the offset compression was reviewed.
>     In the v2 thread [1] Jan asked whether pdx_is_region_compressible() is
>     correct when a region crosses a lookup table slot boundary.  The thread
>     concluded it was not an issue, on the basis that pages contiguous in MFN
>     space are also contiguous in PDX space.  The reproducer below is a case
>     where that does not hold for the code as merged: the region is reported
>     compressible, its last page on its own is not, and that page round-trips
>     to a different PFN.
>     
>     The ranges are as srat_parse_regions() would see them.  The RAM range is
>     not covered by either SRAT range, which is the situation the coverage
>     check in srat_parse_regions() is meant to detect.  Built from
>     tools/tests/pdx like test-pdx-offset, on staging (e4da182973) plus patch
>     "xen/pdx: fix merging of a range contained in the previous one":
>     
>       region [0x75757ffef9, 0x8122007e00) compressible: 1
>       last page compressible: 0
>       last page: pfn 0x8122007dff -> pdx 0x2122047dff -> pfn 0x2d7ee07dff
>     
>     With this patch the region is reported not compressible, and
>     srat_parse_regions() disables compression.
>     
>     8<----------------------------------------------------------------------
>     /* Build like test-pdx-offset, e.g. from tools/tests/pdx:
>      *   gcc -D__XEN_TOOLS__ -DCONFIG_PDX_OFFSET_COMPRESSION \
>      *       -I../../include -o repro-window repro-window.c
>      * (after generating pdx.h as the Makefile does). */
>     #include "harness.h"
>     #include "../../xen/common/pdx.c"
>     
>     int main(void)
>     {
>         /* Two SRAT-like ranges, in PFNs. */
>         pfn_pdx_add_region(pfn_to_paddr(0xdffffe0000UL),
>                            pfn_to_paddr(0xe000000000UL - 0xdffffe0000UL));
>         pfn_pdx_add_region(pfn_to_paddr(0xc5cde0000UL),
>                            pfn_to_paddr(0x4cd7000000UL - 0xc5cde0000UL));
>         if ( !pfn_pdx_compression_setup(0) )
>             return puts("compression not enabled"), EXIT_FAILURE;
>     
>         /* A RAM range not covered by either, as srat_parse_regions() checks. */
>         unsigned long s = 0x75757ffef9UL, e = 0x8122007e00UL;
>     
>         printf("region [%#lx, %#lx) compressible: %d\n", s, e,
>                pdx_is_region_compressible(pfn_to_paddr(s), e - s));
>         printf("last page compressible: %d\n",
>                pdx_is_region_compressible(pfn_to_paddr(e - 1), 1));
>         printf("last page: pfn %#lx -> pdx %#lx -> pfn %#lx\n",
>                e - 1, pfn_to_pdx(e - 1), pdx_to_pfn(pfn_to_pdx(e - 1)));
>     
>         return pdx_is_region_compressible(pfn_to_paddr(s), e - s) &&
>                pdx_to_pfn(pfn_to_pdx(e - 1)) != e - 1 ? EXIT_FAILURE : EXIT_SUCCESS;

I think we want this testing added to test-pdx.c, however it will
require some expansion so that test cases can also provide an array of
memory regions to use with pdx_is_region_compressible() different from
the regions to be compressed.

>     }
>     8<----------------------------------------------------------------------
>     
>     Other callers that rely on the same answer are mem_hotadd_check() and
>     the EFI ram_range_valid() check.  I have not run those paths.
>     
>     One behavioural change to check: with npages == 0 the new condition
>     compares against pfn - 1.  The callers I looked at never pass 0.
>     
>     Model checking (ESBMC, 2 SRAT ranges and 2 e820 RAM ranges, all free
>     below 2^40 PFNs, the srat_parse_regions() coverage check modelled) finds
>     no accepted RAM page that fails to round-trip with both patches applied.
>     It also finds no layout where the coverage check now rejects what setup
>     accepted, with RAM equal to the SRAT ranges.  This is bounded to 2 ranges.
>     
>     The existing tests in tools/tests/pdx pass in both mask and offset mode.
>     
>     I have not reproduced this in a boot: the layout needs RAM near 2^51
>     bytes, which I could not set up under QEMU.
>     
>     [1] https://www.mail-archive.com/xen-devel@lists.xenproject.org/msg194095.html
> 
>  xen/common/pdx.c | 3 ++-
>  1 file changed, 2 insertions(+), 1 deletion(-)
> 
> diff --git a/xen/common/pdx.c b/xen/common/pdx.c
> index 23655ef3bd..52928faa15 100644
> --- a/xen/common/pdx.c
> +++ b/xen/common/pdx.c
> @@ -324,7 +324,8 @@ bool pdx_is_region_compressible(paddr_t base, unsigned long npages)
>      unsigned long pfn_base = pfn_bases[PFN_TBL_IDX(pfn)];
>  
>      return pfn >= pfn_base &&
> -           pfn + npages <= pfn_base + pdx_region_size;
> +           pfn + npages <= pfn_base + pdx_region_size &&
> +           PFN_TBL_IDX(pfn) == PFN_TBL_IDX(pfn + npages - 1);

The fix itself LGTM.

Thanks for chasing this.

Regards, Roger.