1 comment:
Patch Set #2, Line 430: *stolen_base = ALIGN_DOWN(range_entry_end(r) - size, POWER_OF_2(align));
Don't we need to handle the from_top logic in memranges_find_entry() for region size checking? We're […]
Then, let me convince you. :)
The check in memranges_find_entry() guarantees that there is enough
(>= size) space between `r->begin` aligned up and `r->end`. Thus,
`r->end + 1 - size` is above or equal to `r->begin` aligned up. And
aligning it down would result in `r->begin` aligned up in the worst
case.
Long story:
I guess what we have to prove is that every `stolen_base` with
(1) stolen_base = ALIGN_DOWN(range_entry_end(r) - size, POWER_OF_2(align))
is above `r->begin`
(2) stolen_base >= r->begin
We divide (1) into two cases:
(1.1) range_entry_end(r) - size < ALIGN_UP(r->begin, POWER_OF_2(align))
(1.2) range_entry_end(r) - size >= ALIGN_UP(r->begin, POWER_OF_2(align))
(1.1) is what we check in memranges_find_entry().
For (1.2) we can see via (1)
(3) stolen_base >= ALIGN_DOWN(ALIGN_UP(r->begin, POWER_OF_2(align), POWER_OF_2(align))
Aligning down what is already aligned has no effect, thus
(4) stolen_base >= ALIGN_UP(r->begin, POWER_OF_2(align)) >= r->begin
To view, visit change 41957. To unsubscribe, or for help writing mail filters, visit settings.