[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



From: Weiqi Wang <weiqi.wang-2@xxxxxxxxxxxxxxxxxxxxxxxxx>

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@xxxxxxxxxxxxxxxxxxxxxxxxx>
---

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@xxxxxxxxxxxxxxxxxxxx/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




 


Rackspace

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.