[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
cache
using afs-asm, icache-asm,
dcache-asm, pcache-asm
procedures cache_recovery# bool : dir-heap × file-heap × bool × icache × dcache × pcache : bool × error nondeterministic;
cache_format# nat × bool × nat × metadata : dir-heap × file-heap × bool × icache × dcache × pcache : bool × error nondeterministic;
cache_sync# dir-heap × file-heap : bool : error nondeterministic;
cache_fsync# inode × bool × bool : dir-heap × file-heap × icache × pcache × bool : error nondeterministic;
cache_fsync-pages# inode × dir-heap : error × file-heap × pcache × bool nonfunctional nondeterministic;
cache_fsync-inode# : inode × error × dir-heap × file-heap × icache × bool nonfunctional nondeterministic;
cache_fsyncdir# inode × bool × dir-heap × file-heap × bool : : error nondeterministic;
cache_check_commit# dir-heap × file-heap : error × bool nonfunctional nondeterministic;
cache_iget# nat × dir-heap × file-heap × bool : inode × error × icache nonfunctional nondeterministic;
cache_lookup# nat × dir-heap × file-heap × bool : dentry × error × dcache nonfunctional nondeterministic;
cache_create# metadata : inode × inode × dentry × error × dir-heap × file-heap × icache × dcache × bool
nonfunctional
nondeterministic;
cache_unlink# : inode × inode × dentry × error × dir-heap × file-heap × icache × dcache × bool nonfunctional nondeterministic;
cache_mkdir# metadata : inode × inode × dentry × error × dir-heap × file-heap × icache × dcache × bool
nonfunctional
nondeterministic;
cache_rmdir# : inode × inode × dentry × error × dir-heap × file-heap × icache × dcache × bool nonfunctional nondeterministic;
cache_link# dentry : inode × inode × dentry × error × dir-heap × file-heap × icache × dcache × bool nonfunctional nondeterministic;
cache_rename# : inode × inode × inode × inode × dentry × dentry × error × dir-heap × file-heap × icache × dcache × bool
nonfunctional
nondeterministic;
cache_readpage# inode × nat × dir-heap × file-heap × bool : buffer × error × pcache nonfunctional nondeterministic;
cache_writepage# inode × nat × buffer × bool × dir-heap : error × file-heap × pcache × bool nonfunctional nondeterministic;
cache_readdir# inode × dir-heap × file-heap × bool : stringset × error nonfunctional nondeterministic;
cache_evict# inode × bool : error × dir-heap × file-heap × icache × pcache nonfunctional ;
cache_truncate# nat × nat : buffer-opt × inode × bool × error × dir-heap × file-heap × bool × icache × pcache
nonfunctional
nondeterministic;
cache_write_inode# inode × bool : error × dir-heap × file-heap × icache × bool nonfunctional nondeterministic;
variables DENTP : bool flexible;
DIRP : bool flexible;
SYNC : bool flexible;
SOME_BUF : bool flexible;
OLD_DIRTY : bool flexible;
INODE0 : inode flexible;
N0 : nat flexible;
state variables SYNC : bool flexible;
initialization procedure cache_format#
if ERR = ESUCCESS
sequential
invariants icache-cons : ⊦ icache-cons(ICACHE, DIRS, FILES);
dcache-cons : ⊦ dcache-cons(DCACHE, DIRS, FILES);
pcache-cons : ⊦ pcache-cons(PCACHE, DIRS, FILES);
dirs-synced : ⊦ synced(DIRS, ICACHE, PCACHE);
files-synced : ⊦ SYNC → synced(FILES, ICACHE, PCACHE);
recovery procedure cache_recovery#
if ERR = ESUCCESS
declarations recover:
cache_recovery#(DOSYNC; DIRS, FILES, ASYNCED, ICACHE, DCACHE, PCACHE; SYNC, ERR)
precondition true;
postcondition true;
{{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)}
}
format:
cache_format#(N, DOSYNC, SIZE, MD; DIRS, FILES, ASYNCED, ICACHE, DCACHE, PCACHE; SYNC, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{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
}
sync:cache_sync#(DIRS, FILES; ASYNCED; ERR) precondition true; postcondition true;{afs_sync#(DIRS, FILES; ; ASYNCED, ERR)}
fsync:
cache_fsync#(INODE, ISDATASYNC, SYNC; DIRS, FILES, ICACHE, PCACHE, ASYNCED; ERR)
precondition valid-file-inode(INODE, DIRS, FILES);
postcondition true;
{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
}
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}
}
;
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)}}
}
;
fsyncdir:
cache_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR)
precondition true;
postcondition true;
{afs_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR)
}
check-commit:
cache_check_commit#(DIRS, FILES; ERR, ASYNCED)
precondition true;
postcondition true;
{afs_check_commit#(DIRS, FILES; ERR; ASYNCED)
}
iget:
cache_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR, ICACHE)
precondition pre-iget(INO, DIRS, FILES);
postcondition true;
{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
}
lookup:
cache_lookup#(P_INO, DIRS, FILES, ASYNCED; DENT, ERR, DCACHE)
precondition pre-lookup(P_INO, DENT, DIRS, FILES);
postcondition true;
{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
}
create:
cache_create#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED)
precondition pre-create(P_INODE, DENT, MD, DIRS, FILES);
postcondition true;
{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
}
unlink:
cache_unlink#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED)
precondition pre-unlink(P_INODE, C_INODE, DENT, DIRS, FILES);
postcondition true;
{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
}
mkdir:
cache_mkdir#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED)
precondition pre-mkdir(P_INODE, DENT, MD, DIRS, FILES);
postcondition true;
{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
}
rmdir:
cache_rmdir#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED)
precondition pre-rmdir(P_INODE, C_INODE, DENT, DIRS, FILES);
postcondition true;
{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
}
link:
cache_link#(OLD_DENT; P_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES, ICACHE, DCACHE, ASYNCED)
precondition pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, DIRS, FILES);
postcondition true;
{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
}
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
)
precondition pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, DIRS, FILES);
postcondition true;
{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
}
readpage:
cache_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR, PCACHE)
precondition pre-readpage(INODE, PAGENO, PBUF, DIRS, FILES);
postcondition true;
{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
}
writepage:
cache_writepage#(INODE, PAGENO, PBUF, SYNC, DIRS; ERR, FILES, PCACHE, ASYNCED)
precondition pre-writepage(INODE, PAGENO, PBUF, DIRS, FILES);
postcondition true;
{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
}
readdir:
cache_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR)
precondition pre-readdir(INODE.ino, DIRS, FILES);
postcondition true;
{if pre-readdir(INODE.ino, DIRS, FILES) then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR) else abort
}
evict:
cache_evict#(INODE, ASYNCED; ERR, DIRS, FILES, ICACHE, PCACHE)
precondition pre-evict(INODE, DIRS, FILES);
postcondition true;
{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
}
truncate:
cache_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED, ICACHE, PCACHE)
precondition pre-truncate(INODE, N, PAGENO, PBUF-OPT, DIRS, FILES);
postcondition true;
{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
}
write_inode:
cache_write_inode#(INODE, SYNC; ERR, DIRS, FILES, ICACHE, ASYNCED)
precondition pre-write-inode(INODE, DIRS, FILES);
postcondition true;
{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
}
end data asm specification