seL4 icon indicating copy to clipboard operation
seL4 copied to clipboard

Published 20 hours ago • verified publisher icon seL4

mcs: refactor refill_budget_check to ease verification

Open michaelmcinerney opened this issue 5 months ago • 1 comments

This refactors refill_budget_check and schedule_used to ease verification by limiting heap access via refill_head and refill_tail, and providing (inlined) named functions for both the condition and bodies of the loops.

michaelmcinerney avatar Sep 24 '24 04:09 michaelmcinerney