Madvise.lean
Declarations on this page (14)
Linux Virtual Memory madvise Syscall
Models the Linux 7.3 madvise (__NR_madvise = 233) syscall (mm/ do_madvise), including synchronous MADV_DONTNEED zero-fill (Memory.), asynchronous MADV_FREE lazy-reclaim marking (Memory., mm/ and mm/), and no-op behavioral, transparent-hugepage, and coredump advice constants (mm/, include/).
@[expose] public sectionnamespace Arm64namespace Memorydef zeroNonFrozen
Zero-fill all non-frozen mapped bytes in [base, base + len), clearing lazyFree := false and preserving their protection bits (m.) and anon state; frozen and unmapped bytes (and bytes outside the range) are unchanged. Used for madvise(..., MADV_DONTNEED) on private anonymous memory (mm/ madvise_dontneed_free, which synchronously zaps PTEs so subsequent faults allocate fresh zero pages). Never touches frozen bytes.
def madvFreeNonFrozen
Mark all non-frozen mapped bytes in [base, base + len) with lazyFree := true, preserving their protection bits (m.), anon state, and byte values; frozen and unmapped bytes (and bytes outside the range) are unchanged. Used for madvise(..., MADV_FREE) on private anonymous memory (mm/ madvise_free_single_vma, where Linux 7.3 marks folios lazyfree so ttu_anon_lazyfree_folio may asynchronously reclaim unwritten pages to zero at any later point until dirtied by a store). Never touches frozen bytes.
end Memorydef MADV_NORMAL
Linux madvise advice constants (include/).
def MADV_NORMAL : BitVec 64 := 0#64def MADV_RANDOM
def MADV_RANDOM : BitVec 64 := 1#64def MADV_SEQUENTIAL
def MADV_SEQUENTIAL : BitVec 64 := 2#64def MADV_WILLNEED
def MADV_WILLNEED : BitVec 64 := 3#64def MADV_DONTNEED
def MADV_DONTNEED : BitVec 64 := 4#64def MADV_FREE
def MADV_FREE : BitVec 64 := 8#64def MADV_HUGEPAGE
def MADV_HUGEPAGE : BitVec 64 := 14#64def MADV_NOHUGEPAGE
def MADV_NOHUGEPAGE : BitVec 64 := 15#64def MADV_DONTDUMP
def MADV_DONTDUMP : BitVec 64 := 16#64def MADV_DODUMP
def MADV_DODUMP : BitVec 64 := 17#64def SYS_MADVISE
Linux AArch64 madvise syscall number (__NR_madvise = 233, include/, mm/).
def SYS_MADVISE : BitVec 64 := 233#64def execMadvise
madvise(addr, len, advice) (__NR_madvise = 233, mm/ do_madvise) on non-frozen mapped memory. Models:
-
MADV_DONTNEED(4): synchronously zero-fills private anonymous memory and clearslazyFree; -
MADV_FREE(8): marks private anonymous memorylazyFree:= true so reading before an intervening store fails closed (.Exception, preventing proofs from assumingload1 == load2across asynchronousttu_anon_lazyfree_folioreclaim on Linux7.3); -
pure behavioral, transparent-hugepage (
VM_HUGEPAGE/VM_NOHUGEPAGE), and coredump hints (MADV_NORMAL= 0,MADV_RANDOM= 1,MADV_SEQUENTIAL= 2,MADV_WILLNEED= 3,MADV_HUGEPAGE= 14,MADV_NOHUGEPAGE= 15,MADV_DONTDUMP= 16,MADV_DODUMP= 17); -
[INTENTIONAL_SCOPE]:MADV_HUGEPAGE= 14 andMADV_NOHUGEPAGE= 15 (mm//huge_memory.c mm/khugepaged.c hugepage_madvise) assume aCONFIG_TRANSPARENT_HUGEPAGE=yLinux7.3kernel profile on normal user memory (!VM_IO && !VM_PFNMAP && !VM_DAX), where setting or clearingVM_HUGEPAGE/VM_NOHUGEPAGEalways succeeds with0(whereas a kernel built withCONFIG_TRANSPARENT_HUGEPAGE=nor special device VMAs would return-EINVAL); -
[INTENTIONAL_SCOPE]:MADV_DONTNEEDandMADV_FREEon non-anonymous (!isAnon, e.g. file-backed ELF.data) memory fail closed with .Exception"madvise on non-anonymous memory" (on Linux7.3,MADV_FREEreturns-EINVALwhen!vma_is_anonymousinmm/, andmadvise.c:821 MADV_DONTNEEDre-faults underlying file bytes instead of zeroing); all otheradvicevalues fail closed with .Exception"unmodeled madvise advice".
def execMadvise (s : State) : State :=
let addr := s.readReg64 Reg.x0
let len := (s.readReg64 Reg.x1).toNat
let advice := s.readReg64 Reg.x2
let size := pageAlignUp len
let isNoopHint :=
advice == MADV_NORMAL || advice == MADV_RANDOM || advice == MADV_SEQUENTIAL ||
advice == MADV_WILLNEED || advice == MADV_HUGEPAGE || advice == MADV_NOHUGEPAGE ||
advice == MADV_DONTDUMP || advice == MADV_DODUMP
if advice != MADV_DONTNEED && advice != MADV_FREE && !isNoopHint then
s.setStatus (.Exception "unmodeled madvise advice")
else if addr.toNat % PAGE_SIZE != 0 || !decide (addr.toNat + size ≤ 2 ^ 64) then
(s.writeReg64 Reg.x0 (-EINVAL)).advancePC
else if !decide (addr.toNat + size ≤ 2 ^ 48) then
s.setStatus (.Exception "madvise range exceeds user VA space")
else if len == 0 then
(s.writeReg64 Reg.x0 0#64).advancePC
else if !s.mem.allPerm (fun p => !p.frozen) addr size then
s.setStatus (.Exception "madvise on frozen memory")
else if !s.mem.allPerm (·.mapped) addr size then
if s.mem.canMap addr size then
(s.writeReg64 Reg.x0 (-ENOMEM)).advancePC
else
s.setStatus (.Exception "madvise on partially mapped range")
else if (advice == MADV_DONTNEED || advice == MADV_FREE) && !s.mem.allAnon addr size then
s.setStatus (.Exception "madvise on non-anonymous memory")
else if advice == MADV_DONTNEED then
((s.setMem (s.mem.zeroNonFrozen addr size)).writeReg64 Reg.x0 0#64).advancePC
else if advice == MADV_FREE then
((s.setMem (s.mem.madvFreeNonFrozen addr size)).writeReg64 Reg.x0 0#64).advancePC
else
(s.writeReg64 Reg.x0 0#64).advancePCend Arm64