Re: [PATCH v2 2/2] arm64: tlb: Use the TLBI RANGE feature in arm64

Catalin Marinas
2020-07-14T10:36:38Z

On Fri, Jul 10, 2020 at 05:44:20PM +0800, Zhenyu Ye wrote:
> +#define __TLBI_RANGE_PAGES(num, scale) (((num) + 1) << (5 * (scale) + 1))
> +#define MAX_TLBI_RANGE_PAGES __TLBI_RANGE_PAGES(31, 3)
> +
> +#define TLBI_RANGE_MASK GENMASK_ULL(4, 0)
> +#define __TLBI_RANGE_NUM(range, scale) \
> + (((range) >> (5 * (scale) + 1)) & TLBI_RANGE_MASK)
[...]
> + int num = 0;
> + int scale = 0;
[...]
> + start += __TLBI_RANGE_PAGES(num, scale) << PAGE_SHIFT;
[...]

Since num is an int, __TLBI_RANGE_PAGES is still an int. Shifting it by
PAGE_SHIFT can overflow as the maximum would be 8GB for 4K pages (or
128GB for 64K pages). I think we probably get away with this because of
some implicit type conversion but I'd rather make __TLBI_RANGE_PAGES an
explicit unsigned long:

#define __TLBI_RANGE_PAGES(num, scale) ((unsigned long)((num) + 1) << (5 * (scale) + 1))

Without this change, the CBMC check fails (see below for the test). In
the kernel, we don't have this problem as we encode the address via
__TLBI_VADDR_RANGE and it doesn't overflow.

The good part is that CBMC reckons the algorithm is correct ;).

---------------8<------tlbinval.c---------------------------
// SPDX-License-Identifier: GPL-2.0-only
/*
* Check with:
* cbmc --unwind 6 tlbinval.c
*/

#define PAGE_SHIFT (12)
#define PAGE_SIZE (1 << PAGE_SHIFT)
#define VA_RANGE (1UL << 48)

#define __round_mask(x, y) ((__typeof__(x))((y)-1))
#define round_up(x, y) ((((x)-1) | __round_mask(x, y))+1)
#define round_down(x, y) ((x) & ~__round_mask(x, y))

#define __TLBI_RANGE_PAGES(num, scale) ((unsigned long)((num) + 1) << (5 * (scale) + 1))
#define MAX_TLBI_RANGE_PAGES __TLBI_RANGE_PAGES(31, 3)

#define TLBI_RANGE_MASK 0x1fUL
#define __TLBI_RANGE_NUM(pages, scale) \
((((pages) >> (5 * (scale) + 1)) & TLBI_RANGE_MASK) - 1)

static unsigned long inval_start;
static unsigned long inval_end;

static void tlbi(unsigned long start, unsigned long size)
{
unsigned long end = start + size;

if (inval_end == 0) {
inval_start = start;
inval_end = end;
return;
}

/* contiguous ranges in ascending order only */
__CPROVER_assert(start == inval_end, "Contiguous TLBI ranges");

inval_end = end;
}

static void __flush_tlb_range(unsigned long start, unsigned long end,
unsigned long stride)
{
int num = 0;
int scale = 0;
unsigned long pages;

start = round_down(start, stride);
end = round_up(end, stride);
pages = (end - start) >> PAGE_SHIFT;

if (pages >= MAX_TLBI_RANGE_PAGES) {
tlbi(0, VA_RANGE);
return;
}

while (pages > 0) {
__CPROVER_assert(scale <= 3, "Scale in range");
if (pages % 2 == 1) {
tlbi(start, stride);
start += stride;
pages -= stride >> PAGE_SHIFT;
continue;
}

num = __TLBI_RANGE_NUM(pages, scale);
__CPROVER_assert(num <= 30, "Num in range");
if (num >= 0) {
tlbi(start, __TLBI_RANGE_PAGES(num, scale) << PAGE_SHIFT);
start += __TLBI_RANGE_PAGES(num, scale) << PAGE_SHIFT;
pages -= __TLBI_RANGE_PAGES(num, scale);
}
scale++;
}
}

static unsigned long nondet_ulong(void);

int main(void)
{
unsigned long stride = nondet_ulong();
unsigned long start = round_down(nondet_ulong(), stride);
unsigned long end = round_up(nondet_ulong(), stride);

__CPROVER_assume(stride == PAGE_SIZE ||
stride == PAGE_SIZE << (PAGE_SHIFT - 3) ||
stride == PAGE_SIZE << (2 * (PAGE_SHIFT - 3)));
__CPROVER_assume(start < end);
__CPROVER_assume(end <= VA_RANGE);

__flush_tlb_range(start, end, stride);

__CPROVER_assert((inval_start == 0 && inval_end == VA_RANGE) ||
(inval_start == start && inval_end == end),
"Correct invalidation");

return 0;
}