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

[Jan Beulich <jbeulich@suse.com>]

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