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: |
|---|---|---|
| format | pcache_format#(; ; PCACHE, ERR){PCACHE := ∅; ERR := ESUCCESS} | An Axiom |
| recovery | pcache_recovery#(; ; PCACHE, ERR){PCACHE := ∅; ERR := ESUCCESS} | An Axiom |
| get | pcache_get#(INO, PAGENO, PCACHE; HIT, BUF, ERR) {let KEY = datakey(INO, PAGENO) in if KEY ∈ PCACHE then let PE = PCACHE[KEY] in {BUF := PE.page; HIT := true} else HIT := false; ERR := ESUCCESS} | An Axiom |
| set | pcache_set#(INO, PAGENO, BUF, DIRTY; ERR, PCACHE){let KEY = datakey(INO, PAGENO), PE = mkpentry(DIRTY, BUF) in PCACHE[KEY] := PE} | An Axiom |
| delete | pcache_delete#(INO, PAGENO; ERR, PCACHE){let KEY = datakey(INO, PAGENO) in PCACHE := PCACHE -- KEY} | An Axiom |
| truncate | pcache_truncate#(INO, SIZE, N; ERR, PCACHE){if ∀ key. key ∈ PCACHE → key.data? then PCACHE := truncate(INO, min(N, SIZE), PCACHE) else abort} | An Axiom |
| evict | pcache_evict#(INO; ERR, PCACHE){if ∀ key. key ∈ PCACHE → key.data? then PCACHE := evict(INO, PCACHE) else abort} | An Axiom |
| check-page | pcache_check_page#(INO, PAGENO, PCACHE; HIT, DIRTY, ERR) {let KEY = datakey(INO, PAGENO) in if KEY ∈ PCACHE then {HIT := true; DIRTY := PCACHE[KEY].dirty} else HIT := false} | An Axiom |
| set-status | pcache_set_status#(INO, PAGENO, DIRTY; ERR, PCACHE) {let KEY = datakey(INO, PAGENO), PE = ? in if KEY ∈ PCACHE then {PE := PCACHE[KEY]; PE := mkpentry(DIRTY, PE.page); PCACHE[KEY] := PE} else ERR := EFAIL } | An Axiom |
| inv-recovery | ⊦ ⟪pcache_recovery#(; ; pcache, err)⟫ true | A Proof Obligation |
| inv-evict | ∀ key. key ∈ pcache → key.data? ⊦ ⟪pcache_evict#(ino; err, pcache)⟫ ∀ key. key ∈ pcache → key.data? ∧ key.ino ≠ ino | A Proof Obligation |
| inv-truncate | ∀ key. key ∈ pcache → key.data? ⊦ ⟪pcache_truncate#(ino, size, n; err, pcache)⟫ ∀ key. key ∈ pcache → key.data? ∧ (key.ino = ino → key.part * VFS_PAGE_SIZE < min(n, size)) | A Proof Obligation |
| crash-neutral-recovery | ⊦ ⟨pcache_recovery#(; ; pcache, err)⟩ true | A Proof Obligation |
| crash-neutral-truncate | ∀ key. key ∈ pcache → key.data? ⊦ ⟨pcache_truncate#(ino, size, n; err, pcache)⟩ true | A Proof Obligation |
| crash-neutral-evict | ∀ key. key ∈ pcache → key.data? ⊦ ⟨pcache_evict#(ino; err, pcache)⟩ true | A Proof Obligation |
| crash-neutral-delete | ⊦ ⟨pcache_delete#(ino, pageno; err, pcache)⟩ true | A Proof Obligation |
| crash-neutral-set-status | ⊦ ⟨pcache_set_status#(ino, pageno, boolvar; err, pcache)⟩ true | A Proof Obligation |
| crash-neutral-check-page | ⊦ ⟨pcache_check_page#(ino, pageno, pcache; boolvar, boolvar0, err)⟩ true | A Proof Obligation |
| crash-neutral-set | ⊦ ⟨pcache_set#(ino, pageno, buf, boolvar; err, pcache)⟩ true | A Proof Obligation |
| crash-neutral-get | ⊦ ⟨pcache_get#(ino, pageno, pcache; boolvar, buf, err)⟩ true | A Proof Obligation |