This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| recover | cache_recovery#(DOSYNC; DIRS, FILES, ASYNCED, ICACHE, DCACHE, PCACHE; SYNC, ERR) {SYNC := DOSYNC; afs_recovery#(DOSYNC; DIRS, FILES; ASYNCED, ERR); if ERR = ESUCCESS then icache_recovery#(; ; ICACHE, ERR); if ERR = ESUCCESS then dcache_recovery#(; ; DCACHE, ERR); if ERR = ESUCCESS then pcache_recovery#(; ; PCACHE, ERR) } | An Axiom |
| format | cache_format#(N, DOSYNC, SIZE, MD; DIRS, FILES, ASYNCED, ICACHE, DCACHE, PCACHE; SYNC, ERR) {if SIZE = LEB_SIZE then {SYNC := DOSYNC; afs_format#(N, DOSYNC, SIZE, MD; DIRS; FILES, ASYNCED, ERR); if ERR = ESUCCESS then icache_format#(; ; ICACHE, ERR); if ERR = ESUCCESS then dcache_format#(; ; DCACHE, ERR); if ERR = ESUCCESS then pcache_format#(; ; PCACHE, ERR)} else abort } | An Axiom |
| check-commit | cache_check_commit#(DIRS, FILES; ERR, ASYNCED){afs_check_commit#(DIRS, FILES; ERR; ASYNCED)} | An Axiom |
| lookup | cache_lookup#(P_INO, DIRS, FILES, ASYNCED; DENT, ERR, DCACHE) {if pre-lookup(P_INO, DENT, DIRS, FILES) then let HIT = false, NAME = DENT.name in {dcache_get#(P_INO, NAME, DCACHE; HIT, DENT, ERR); if ¬ HIT ∨ ERR ≠ ESUCCESS then {afs_lookup#(P_INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then dcache_set#(P_INO, NAME, DENT; ERR, DCACHE)}} else abort } | An Axiom |
| create | cache_create#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-create(P_INODE, DENT, MD, DIRS, FILES) then {afs_create#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(P_INODE, DIRTY; ERR, ICACHE); icache_set#(C_INODE, DIRTY; ERR, ICACHE); dcache_set#(P_INODE.ino, DENT.name, DENT; ERR, DCACHE)}} else abort } | An Axiom |
| unlink | cache_unlink#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-unlink(P_INODE, C_INODE, DENT, DIRS, FILES) then {afs_unlink#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(C_INODE, DIRTY; ERR, ICACHE); icache_set#(P_INODE, DIRTY; ERR, ICACHE); dcache_delete#(P_INODE.ino, DENT.name; ERR, DCACHE)}} else abort } | An Axiom |
| mkdir | cache_mkdir#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-mkdir(P_INODE, DENT, MD, DIRS, FILES) then {afs_mkdir#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(P_INODE, DIRTY; ERR, ICACHE); icache_set#(C_INODE, DIRTY; ERR, ICACHE); dcache_set#(P_INODE.ino, DENT.name, DENT; ERR, DCACHE)}} else abort } | An Axiom |
| rmdir | cache_rmdir#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-rmdir(P_INODE, C_INODE, DENT, DIRS, FILES) then {afs_rmdir#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(C_INODE, DIRTY; ERR, ICACHE); icache_set#(P_INODE, DIRTY; ERR, ICACHE); dcache_delete#(P_INODE.ino, DENT.name; ERR, DCACHE)}} else abort } | An Axiom |
| link | cache_link#(OLD_DENT; P_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, DIRS, FILES) then {afs_link#(OLD_DENT; P_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(P_INODE, DIRTY; ERR, ICACHE); icache_set#(C_INODE, DIRTY; ERR, ICACHE); dcache_set#(P_INODE.ino, NEW_DENT.name, NEW_DENT; ERR, DCACHE)}} else abort } | An Axiom |
| renam | cache_rename# (; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED) {if pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, DIRS, FILES) then let DENTP = NEW_DENT.dentry? in {afs_rename#(; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(OLD_PARENT_INODE, DIRTY; ERR, ICACHE); icache_set#(NEW_PARENT_INODE, DIRTY; ERR, ICACHE); if DENTP then icache_set#(NEW_CHILD_INODE, DIRTY; ERR, ICACHE); dcache_delete#(OLD_PARENT_INODE.ino, OLD_DENT.name; ERR, DCACHE); dcache_set#(NEW_PARENT_INODE.ino, NEW_DENT.name, NEW_DENT; ERR, DCACHE)}} else abort } | An Axiom |
| readpage | cache_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR, PCACHE) {if pre-readpage(INODE, PAGENO, PBUF, DIRS, FILES) then let HIT = false, INO = INODE.ino in {pcache_get#(INO, PAGENO, PCACHE; HIT, PBUF, ERR); if ¬ HIT ∨ ERR ≠ ESUCCESS then {afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR); if ERR = ESUCCESS ∧ PBUF ≠ zeropage then let DIRTY = false in pcache_set#(INO, PAGENO, PBUF, DIRTY; ERR, PCACHE)}} else abort } | An Axiom |
| writepage | cache_writepage#(INODE, PAGENO, PBUF, SYNC, DIRS; ERR, FILES, PCACHE, ASYNCED) {if pre-writepage(INODE, PAGENO, PBUF, DIRS, FILES) then let DIRTY = true in {if SYNC then {afs_writepage#(INODE, PAGENO, PBUF, DIRS; ERR, FILES; ASYNCED); DIRTY := false} else ERR := ESUCCESS; if ERR = ESUCCESS then pcache_set#(INODE.ino, PAGENO, PBUF, DIRTY; ERR, PCACHE)} else abort } | An Axiom |
| readdir | cache_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR) {if pre-readdir(INODE.ino, DIRS, FILES) then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR) else abort} | An Axiom |
| evict | cache_evict#(INODE, ASYNCED; ERR, DIRS, FILES, ICACHE, PCACHE) {if pre-evict(INODE, DIRS, FILES) then let DIRP = INODE.directory in {afs_evict#(INODE, ASYNCED; ERR, DIRS, FILES); if ERR = ESUCCESS ∧ INODE.nlink = 0 then {icache_delete#(INODE.ino; ERR, ICACHE); if ¬ DIRP then pcache_evict#(INODE.ino; ERR, PCACHE)}} else abort } | An Axiom |
| truncate | cache_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED, ICACHE, PCACHE) {if pre-truncate(INODE, N, PAGENO, PBUF-OPT, DIRS, FILES) then let INO = INODE.ino, SIZE = INODE.size, SOME_BUF = PBUF-OPT.some?, HIT = false, OLD_DIRTY = false in {ERR := ESUCCESS; if PBUF-OPT.none? then let PBUF = ? in {pcache_check_page#(INO, PAGENO, PCACHE; HIT, OLD_DIRTY, ERR); if ERR = ESUCCESS ∧ HIT then pcache_get#(INO, PAGENO, PCACHE; HIT, PBUF, ERR); if ERR = ESUCCESS ∧ HIT then PBUF-OPT := some(PBUF)}; if ERR = ESUCCESS then afs_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED); if ERR = ESUCCESS then let DIRTY = false in {icache_set#(INODE, DIRTY; ERR, ICACHE); pcache_truncate#(INODE.ino, SIZE, N; ERR, PCACHE); if MODIFIED then pcache_set#(INODE.ino, PAGENO, PBUF-OPT.buf, DIRTY; ERR, PCACHE)}; if (¬ MODIFIED ∨ ERR ≠ ESUCCESS) ∧ ¬ SOME_BUF then PBUF-OPT := none} else abort } | An Axiom |
| write_inode | cache_write_inode#(INODE, SYNC; ERR, DIRS, FILES, ICACHE, ASYNCED) {if pre-write-inode(INODE, DIRS, FILES) then let DIRTY = true, INODE0 = ?, HIT = false in {if SYNC ∨ INODE.directory then {afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED); DIRTY := false} else ERR := ESUCCESS; if ERR = ESUCCESS then icache_get#(INODE.ino, ICACHE; HIT, INODE0, ERR); if ERR = ESUCCESS ∧ HIT then {INODE0.meta := INODE.meta; if ¬ INODE.directory then INODE0.size := INODE.size; icache_set#(INODE0, DIRTY; ERR, ICACHE)} else if DIRTY then ERR := EFAIL} else abort } | An Axiom |
| sync | cache_sync#(DIRS, FILES; ASYNCED; ERR){afs_sync#(DIRS, FILES; ; ASYNCED, ERR)} | An Axiom |
| iget | cache_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR, ICACHE) {if pre-iget(INO, DIRS, FILES) then let HIT = false, DIRTY = false in {icache_get#(INO, ICACHE; HIT, INODE, ERR); if ¬ HIT ∨ ERR ≠ ESUCCESS then {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then icache_set#(INODE, DIRTY; ERR, ICACHE)}} else abort } | An Axiom |
| fsync | cache_fsync#(INODE, ISDATASYNC, SYNC; DIRS, FILES, ICACHE, PCACHE, ASYNCED; ERR) {if valid-file-inode(INODE, DIRS, FILES) then {ERR := ESUCCESS; if ¬ SYNC then {cache_fsync-pages#(INODE, DIRS; ERR, FILES, PCACHE, ASYNCED); if ERR = ESUCCESS ∧ ¬ ISDATASYNC then cache_fsync-inode#(; INODE, ERR, DIRS, FILES, ICACHE, ASYNCED); if ERR = ESUCCESS then afs_fsync#(INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR)}} else abort } | An Axiom |
| fsyncdir | cache_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR){afs_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR)} | An Axiom |
| fsync-pages | cache_fsync-pages#(INODE, DIRS; ERR, FILES, PCACHE, ASYNCED) {ERR := ESUCCESS; let N = 0, INO = INODE.ino, HIT = ?, DIRTY = ? in while N * VFS_PAGE_SIZE < INODE.size ∧ ERR = ESUCCESS do {/* (fsync-pages-overwrite : invariant afs-cons(DIRS, FILES) ∧ pcache-cons(PCACHE, DIRS, FILES) ∧ getinode(INO, DIRS, FILES) = getinode(INO, DIRS, FILES`) ∧ INO = INODE.ino ∧ INO ∈ FILES ∧ (∀ KEY. (KEY ∈ PCACHE ↔ KEY ∈ PCACHE`) ∧ PCACHE[KEY].page = (PCACHE`)[KEY].page ∧ (PCACHE[KEY].dirty → (PCACHE`)[KEY].dirty)) ∧ ( ERR = ESUCCESS → (∀ PAGENO. (PAGENO < N ⊃ (PAGENO ∈ FILES[INO].content ↔ PAGENO ∈ (FILES` ⊕ PCACHE`)[INO].content) ∧ FILES[INO].content[PAGENO] = (FILES` ⊕ PCACHE`)[INO].content[PAGENO] ; (PAGENO ∈ FILES[INO].content ↔ PAGENO ∈ (FILES`)[INO].content) ∧ FILES[INO].content[PAGENO] = (FILES`)[INO].content[PAGENO] )))) */; pcache_check_page#(INO, N, PCACHE; HIT, DIRTY, ERR); if HIT ∧ DIRTY then let PBUF = ? in {pcache_get#(INO, N, PCACHE; HIT, PBUF, ERR); if ERR = ESUCCESS then afs_writepage#(INODE, N, PBUF, DIRS; ERR, FILES; ASYNCED); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then {DIRTY := false; pcache_set_status#(INO, N, DIRTY; ERR, PCACHE)}}; N := N + 1} } | An Axiom |
| fsync-inode | cache_fsync-inode#(; INODE, ERR, DIRS, FILES, ICACHE, ASYNCED) {let INO = INODE.ino, HIT = ?, DIRTY = ? in {icache_check_inode#(INO, ICACHE; HIT, DIRTY, ERR); if ERR = ESUCCESS ∧ HIT ∧ DIRTY then icache_get#(INO, ICACHE; HIT, INODE, ERR); if ERR = ESUCCESS ∧ HIT ∧ DIRTY then afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED); if ERR = ESUCCESS then {DIRTY := false; icache_set_status#(INO, DIRTY; ERR, ICACHE)}} } | An Axiom |
| inv-iget | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-iget(ino, dirs, files) ⊦ ⟪cache_iget#(ino, dirs, files, asynced0; inode, err, icache)⟫ (icache-cons(icache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A Proof Obligation |
| inv-recover | dirs = dirs0 \ orphans(dirs0, files), files0 = files \ orphans(dirs0, files), asynced, icache-cons(icache, dirs0, files), dcache-cons(dcache, dirs0, files), pcache-cons(pcache, dirs0, files), synced(dirs0, icache, pcache), asynced0 → synced(files, icache, pcache), afs-cons(dirs0, files) ⊦ ⟪cache_recovery#(asynced1; dirs, files0, asynced2, icache0, dcache0, pcache0; asynced3, err)⟫ ( err = ESUCCESS → asynced2 ∧ icache-cons(icache0, dirs, files0) ∧ dcache-cons(dcache0, dirs, files0) ∧ pcache-cons(pcache0, dirs, files0) ∧ synced(dirs, icache0, pcache0) ∧ (asynced3 → synced(files0, icache0, pcache0)) ∧ afs-cons(dirs, files0)) | A Proof Obligation |
| inv-check-commit | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files) ⊦ ⟪cache_check_commit#(dirs, files; err, asynced0)⟫ true | A Proof Obligation |
| inv-lookup | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-lookup(p_ino, dent, dirs, files) ⊦ ⟪cache_lookup#(p_ino, dirs, files, asynced0; dent, err, dcache)⟫ dcache-cons(dcache, dirs, files) | A Proof Obligation |
| inv-create | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-create(p_inode, dent, md, dirs, files) ⊦ ⟪cache_create#(md; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-unlink | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-unlink(p_inode, c_inode, dent, dirs, files) ⊦ ⟪cache_unlink#(; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-mkdir | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-mkdir(p_inode, dent, md, dirs, files) ⊦ ⟪cache_mkdir#(md; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-rmdir | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files) ⊦ ⟪cache_rmdir#(; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-link | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files) ⊦ ⟪cache_link#(old_dent; p_inode, c_inode, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-renam | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-readpage | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-readpage(inode, pageno, buf, dirs, files) ⊦ ⟪cache_readpage#(inode, pageno, dirs, files, asynced0; buf, err, pcache)⟫ (pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A Proof Obligation |
| inv-writepage | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-writepage(inode, pageno, buf, dirs, files) ⊦ ⟪cache_writepage#(inode, pageno, buf, asynced, dirs; err, files, pcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-readdir | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-readdir(inode.ino, dirs, files) ⊦ ⟪cache_readdir#(inode, dirs, files, asynced0; strings, err)⟫ true | A Proof Obligation |
| inv-evict | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-evict(inode, dirs, files) ⊦ ⟪cache_evict#(inode, asynced0; err, dirs, files, icache, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-truncate | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-truncate(inode, n, pageno, buf-opt, dirs, files) ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced0, err, dirs, files, asynced1, icache, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-write_inode | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), pre-write-inode(inode, dirs, files) ⊦ ⟪cache_write_inode#(inode, asynced; err, dirs, files, icache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-sync | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files) ⊦ ⟪cache_sync#(dirs, files; asynced0; err)⟫ true | A Proof Obligation |
| inv-format | size = LEB_SIZE ⊦ ⟪cache_format#(n, asynced, size, md; dirs, files, asynced0, icache, dcache, pcache; asynced1, err)⟫ ( err = ESUCCESS → asynced0 ∧ icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced1 → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-fsync | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files), valid-file-inode(inode, dirs, files) ⊦ ⟪cache_fsync#(inode, asynced0, asynced; dirs, files, icache, pcache, asynced1; err)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-fsyncdir | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), afs-cons(dirs, files) ⊦ ⟪cache_fsyncdir#(inode, asynced0, dirs, files, asynced1; ; err)⟫ true | A Proof Obligation |
| fsync-inode-inv | valid-file-inode(inode, dirs, files), icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache) ⊦ ⟪cache_fsync-inode#(; inode, err, dirs, files, icache, asynced)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ valid-file-inode(inode, dirs, files)) | A User Theorem |
| fsync-pages-inv | valid-file-inode(inode, dirs, files), icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache) ⊦ ⟪cache_fsync-pages#(inode, dirs; err, files, pcache, asynced)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ valid-file-inode(inode, dirs, files)) | A User Theorem |
| inv-rename-dentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-wb-inode(old_child_inode, dirs, files), valid-wb-inode(new_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files), valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files), old_child_inode.ino = old_dent.ino, new_child_inode.ino = new_dent.ino ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-rename-dir-dentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-dir-inode(old_child_inode, dirs, files), valid-dir-inode(new_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, old_child_inode.ino = old_dent.ino, new_child_inode.ino = new_dent.ino, new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files) ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-rename-dir-negdentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-negdentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-dir-inode(old_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, old_child_inode.ino = old_dent.ino ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-rename-file-dentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-file-inode(old_child_inode, dirs, files), valid-file-inode(new_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, old_child_inode.ino = old_dent.ino, new_child_inode.ino = new_dent.ino ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-rename-file-negdentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-negdentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-file-inode(old_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, old_child_inode.ino = old_dent.ino ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-rename-negdentry | icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-negdentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-wb-inode(old_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, old_child_inode.ino = old_dent.ino ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-truncate-buff-none-cached | valid-file-inode(inode, dirs, files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.none?, datakey(inode.ino, pageno) ∈ pcache, icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache) ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced0, err, dirs, files, asynced1, icache, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-truncate-buff-none-uncached | valid-file-inode(inode, dirs, files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.none?, ¬ datakey(inode.ino, pageno) ∈ pcache, icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache) ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced0, err, dirs, files, asynced1, icache, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |
| inv-truncate-buff-some | valid-file-inode(inode, dirs, files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.some?, # buf-opt.buf = VFS_PAGE_SIZE, icache-cons(icache, dirs, files), dcache-cons(dcache, dirs, files), pcache-cons(pcache, dirs, files), afs-cons(dirs, files), synced(dirs, icache, pcache), asynced → synced(files, icache, pcache) ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced0, err, dirs, files, asynced1, icache, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))) | A User Theorem |