[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
vfs
using vfs-permission
,
afs-asm
,
seekflag
,
eraseblock
procedures vfs_recover# bool : dir-heap × file-heap × bool : open-files × nat × error nondeterministic;
vfs_format# nat × bool × nat × metadata : dir-heap × file-heap × bool : open-files × nat × error nondeterministic;
vfs_sync# dir-heap × file-heap : bool : error nondeterministic;
vfs_fsync# path × bool × user × dir-heap × file-heap : bool : error nondeterministic;
vfs_fsyncdir# path × bool × user × dir-heap × file-heap : bool : error nondeterministic;
vfs_may_lookup# nat × user × dir-heap × file-heap × bool : inode × error nonfunctional nondeterministic;
vfs_may_create# nat × dentry × user × dir-heap × file-heap × bool : inode × error nonfunctional nondeterministic;
vfs_may_link# nat × user × dir-heap × file-heap × bool : inode × dentry × error nonfunctional nondeterministic;
vfs_may_delete# nat × bool × user × dir-heap × file-heap × bool : inode × dentry × inode × bool × error
nonfunctional
nondeterministic;
vfs_may_delete_check# nat × user × dir-heap × file-heap × bool : inode × bool × dentry × inode × error
nonfunctional
nondeterministic;
vfs_may_open# nat × bool × file-mode × user × dir-heap × file-heap × bool : inode × error nonfunctional nondeterministic;
vfs_put_inode# inode × open-files × bool : error × dir-heap × file-heap nonfunctional ;
vfs_walk# path × user × dir-heap × file-heap × bool : nat × error nonfunctional nondeterministic;
vfs_create# path × metadata × user : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_mkdir# path × metadata × user : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_rmdir# path × user × open-files : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_unlink# path × user × open-files : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_rename# path × path × user × open-files : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_link# path × path × user : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_open# path × file-mode × user × dir-heap × file-heap × bool : nat × error × open-files × nat nonfunctional nondeterministic;
vfs_close# nat × user × bool : error × open-files × dir-heap × file-heap nonfunctional nondeterministic;
vfs_truncate# path × nat × user : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_seek# nat × seekflag × user × dir-heap × file-heap × bool : nat × error × open-files nonfunctional nondeterministic;
vfs_readmeta# path × user × dir-heap × file-heap × bool : metadata × nat × nat × error nonfunctional nondeterministic;
vfs_writemeta# path × metadata × user : error × dir-heap × file-heap × bool nonfunctional nondeterministic;
vfs_readdir# path × user × dir-heap × file-heap × bool : stringset × error nonfunctional nondeterministic;
vfs_read_block# nat × nat × inode × dir-heap × file-heap × bool : buffer × nat × bool × error nonfunctional nondeterministic;
vfs_read_loop# nat × nat × inode × bool × dir-heap × file-heap × bool : buffer × nat × error nonfunctional nondeterministic;
vfs_read# nat × user × dir-heap × file-heap × bool : buffer × nat × error × open-files nonfunctional nondeterministic;
vfs_writepage# inode × nat × buffer × nat × nat × nat × dir-heap : error × file-heap × bool nonfunctional nondeterministic;
vfs_write_block# nat × inode × buffer × nat × dir-heap : nat × bool × error × file-heap × bool nonfunctional nondeterministic;
vfs_write_loop# nat × inode × nat × buffer × dir-heap : nat × error × file-heap × bool nonfunctional nondeterministic;
vfs_write# nat × buffer × user : nat × error × open-files × dir-heap × file-heap × bool nonfunctional nondeterministic;
variables OF : open-files flexible;
PATH : path flexible;
PATH' : path flexible;
FD : nat flexible;
USER : user flexible;
MODE : file-mode flexible;
WHENCE : seekflag flexible;
BUF : buffer flexible;
BUF0 : buffer flexible;
PBUF : buffer flexible;
MAXINO : nat flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
N2 : nat flexible;
OFFSET : nat flexible;
START : nat flexible;
END : nat flexible;
TOTAL : nat flexible;
DONE : bool flexible;
ISDIR : bool flexible;
ISDIR0 : bool flexible;
ISRENAME : bool flexible;
DEL_INO : nat flexible;
NLINK : nat flexible;
isdir : bool;
isrename : bool;
DEL_INODE : inode flexible;
DENT_INODE : inode flexible;
OLD_DENT_INODE : inode flexible;
NEW_DENT_INODE : inode flexible;
NAMES0 : stringset flexible;
NAME : string flexible;
state variables OF : open-files flexible;
MAXINO : nat flexible;
initialization procedure vfs_format#
if ERR = ESUCCESS
sequential
invariants of : ⊦ of-cons(OF, DIRS, FILES);
maxino : ⊦ dom OF < MAXINO;
recovery procedure vfs_recover#
if ERR = ESUCCESS
declarations recover:
vfs_recover#(DOSYNC; DIRS, FILES, ASYNCED; OF, MAXINO, ERR)
precondition true;
postcondition true;
{{OF := ∅; MAXINO := 0; afs_recovery#(DOSYNC; DIRS, FILES; ASYNCED, ERR)}
}
format:
vfs_format#(N, DOSYNC, SIZE, MD; DIRS, FILES, ASYNCED; OF, MAXINO, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE then {OF := ∅; MAXINO := 0; afs_format#(N, DOSYNC, SIZE, MD; DIRS; FILES, ASYNCED, ERR)} else abort
}
sync:vfs_sync#(DIRS, FILES; ASYNCED; ERR) precondition true; postcondition true;{afs_sync#(DIRS, FILES; ; ASYNCED, ERR)}
fsync:
vfs_fsync#(PATH, ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR)
precondition true;
postcondition true;
{let INO = ROOT_INO, MODE = MODE_R, INODE = ?
in {ERR := ESUCCESS; vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_fsync#(INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR);
if ERR = ESUCCESS then afs_sync#(DIRS, FILES; ; ASYNCED, ERR)}
}
fsyncdir:
vfs_fsyncdir#(PATH, ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR)
precondition true;
postcondition ⌊ERR⌋ ∨ ERR = ESUCCESS;
{let INO = ROOT_INO, MODE = MODE_R, NAMES = ∅, ISDIR = true, INODE = ?, C_INODE = ?
in {ERR := ESUCCESS; vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR);
while NAMES ≠ ∅ ∧ ERR = ESUCCESS
do choose NAME
with NAME ∈ NAMES
in {let DENT = negdentry(NAME)
in {afs_lookup#(INODE.ino, DIRS, FILES, ASYNCED; DENT, ERR);
if ERR = ESUCCESS then afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; C_INODE, ERR)};
if ERR = ESUCCESS
then if C_INODE.directory
then let PATH' = PATH + NAME in vfs_fsyncdir#(PATH', ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR)
else afs_fsync#(C_INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR);
NAMES := NAMES -- NAME};
if ERR = ESUCCESS then afs_sync#(DIRS, FILES; ; ASYNCED, ERR)}
}
may-lookup
: vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR)
{afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then if ¬ INODE.directory then ERR := ENOENT else if ¬ px(USER, INODE.meta) then ERR := EACCESS
}
;
may-create
: vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR)
{afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if ¬ INODE.directory
then ERR := ENOTDIR
else if ¬ px(USER, INODE.meta) ∨ ¬ pw(USER, INODE.meta)
then ERR := EACCESS
else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR);
if ERR = ESUCCESS then ERR := EEXISTS else if ERR = ENOENT then ERR := ESUCCESS}
}
;
may-link
: vfs_may_link#(INO, USER, DIRS, FILES, ASYNCED; INODE, DENT, ERR)
{afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if ¬ INODE.directory
then ERR := ENOTDIR
else if ¬ px(USER, INODE.meta)
then ERR := EACCESS
else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR);
if ERR = ESUCCESS then afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS ∧ INODE.directory then ERR := EISDIR}
}
;
may-delete
: vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DENT_INODE, ISDIR, ERR)
{afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if ¬ INODE.directory
then ERR := ENOTDIR
else if ¬ px(USER, INODE.meta) ∨ ¬ pw(USER, INODE.meta)
then ERR := EACCESS
else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR);
if ERR = ESUCCESS
then {afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; DENT_INODE, ERR);
if ERR = ESUCCESS
then {ISDIR := DENT_INODE.directory;
if ISDIR
then if DENT_INODE.ino = ROOT_INO
then ERR := EACCESS
else if ISRENAME ∧ ¬ pw(USER, DENT_INODE.meta)
then ERR := EACCESS
else if ¬ ISRENAME ∧ DENT_INODE.size ≠ 0 then ERR := ENOTEMPTY}}}
}
;
may-delete-check
: vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DENT_INODE, ERR)
{let ISDIR0 = ISDIR, ISRENAME = false
in {vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DENT_INODE, ISDIR, ERR);
if ISDIR0 ∧ ¬ ISDIR then ERR := ENOTDIR; if ¬ ISDIR0 ∧ ISDIR then ERR := EISDIR}
}
;
may-open
: vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR)
{afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if ¬(INODE.directory ↔ ISDIR)
then ERR := (INODE.directory ⊃ EISDIR;ENOTDIR)
else if (MODE = MODE_R ∨ MODE = MODE_RW) ∧ ¬ pr(USER, INODE.meta) ∨ (MODE = MODE_W ∨ MODE = MODE_RW) ∧ ¬ pw(USER, INODE.meta)
then ERR := EACCESS
}
;
put-inode
: vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)
{if ERR = ESUCCESS ∧ ¬ is-open(DEL_INODE.ino, OF) then afs_evict#(DEL_INODE, ASYNCED; ERR, DIRS, FILES)}
;
walk
: vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR)
{ERR := ESUCCESS;
let PATH = PATH
in while PATH ≠ ε ∧ ERR = ESUCCESS
do {choose INODE with true in vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then let DENT = negdentry(PATH.head)
in {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then {INO := DENT.ino; PATH := PATH.tail}}}
}
;
create:
vfs_create#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{if PATH = ε
then ERR := EEXISTS
else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), INODE = ?, C_INODE = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then afs_create#(MD; INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)}
}
mkdir:
vfs_mkdir#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{if PATH = ε
then ERR := EEXISTS
else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), INODE = ?, C_INODE = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then afs_mkdir#(MD; INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)}
}
rmdir:
vfs_rmdir#(PATH, USER, OF; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{if PATH = ε
then ERR := EACCESS
else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), ISDIR = true, INODE = ?, DEL_INODE = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS
then {afs_rmdir#(; INODE, DEL_INODE, DENT, ERR, DIRS, FILES; ASYNCED);
vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}}
}
unlink:
vfs_unlink#(PATH, USER, OF; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{if PATH = ε
then ERR := EACCESS
else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), ISDIR = false, INODE = ?, DEL_INODE = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS
then {afs_unlink#(; INODE, DEL_INODE, DENT, ERR, DIRS, FILES; ASYNCED);
vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}}
}
renam:
vfs_rename#(PATH, PATH', USER, OF; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{choose OLD_DENT, NEW_DENT, ISDIR, INODE, OLD_INODE, NEW_INODE, DEL_INODE, OLD_DENT_INODE, NEW_DENT_INODE
with true
in if PATH = ε ∨ PATH' = ε ∨ PATH ⊑ PATH'
then ERR := EACCESS
else {let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH)
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS
then let ISRENAME = true
in vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DEL_INODE, ISDIR, ERR);
OLD_INODE := INODE; OLD_DENT := DENT; OLD_DENT_INODE := DEL_INODE};
if ERR = ESUCCESS
then let INO = ROOT_INO, DENT = negdentry(PATH'.last), PATH = parent(PATH')
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR);
if ERR = ENOENT
then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR)
else if ERR = ESUCCESS
then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR)};
NEW_INODE := INODE; NEW_DENT := DENT; NEW_DENT_INODE := DEL_INODE};
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS
then let DENT = NEW_DENT
in {afs_rename#
(; OLD_INODE, NEW_INODE, OLD_DENT_INODE, NEW_DENT_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED);
if DENT.dentry? then vfs_put_inode#(NEW_DENT_INODE, OF, ASYNCED; ERR, DIRS, FILES)}}
}
link:
vfs_link#(PATH, PATH', USER; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{choose OLD_DENT, NEW_DENT, INODE, NEW_INODE, C_INODE
with true
in if PATH = ε ∨ PATH' = ε
then ERR := EISDIR
else {let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH)
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_link#(INO, USER, DIRS, FILES, ASYNCED; INODE, DENT, ERR); C_INODE := INODE;
OLD_DENT := DENT};
if ERR = ESUCCESS
then let INO = ROOT_INO, DENT = negdentry(PATH'.last), PATH = parent(PATH')
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR);
NEW_INODE := INODE, NEW_DENT := DENT};
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then afs_link#(OLD_DENT; NEW_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES; ASYNCED)}
}
open:
vfs_open#(PATH, MODE, USER, DIRS, FILES, ASYNCED; FD, ERR, OF, MAXINO)
precondition true;
postcondition true;
{let INO = ROOT_INO, INODE = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then {OF[MAXINO] := mkfile(INO, MODE, 0); FD := MAXINO; MAXINO := MAXINO + 1}}
}
close:
vfs_close#(FD, USER, ASYNCED; ERR, OF, DIRS, FILES)
precondition true;
postcondition true;
{{ERR := ESUCCESS;
if ¬ FD ∈ OF
then ERR := EBADFD
else let DEL_INO = OF[FD].ino
in choose DEL_INODE
with true
in {afs_iget#(DEL_INO, DIRS, FILES, ASYNCED; DEL_INODE, ERR);
if ERR = ESUCCESS then {OF := OF -- FD; vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}}}
}
truncate:
vfs_truncate#(PATH, N, USER; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{let INO = ROOT_INO, MODE = MODE_W, PAGENO = 0, PBUF-OPT = none, INODE = ?, MODIFIED = ?
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then PAGENO := INODE.size / VFS_PAGE_SIZE;
if ERR = ESUCCESS then afs_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED)}
}
seek:
vfs_seek#(FD, WHENCE, USER, DIRS, FILES, ASYNCED; N, ERR, OF)
precondition true;
postcondition true;
{{ERR := ESUCCESS;
if ¬ FD ∈ OF
then ERR := EBADFD
else {if WHENCE = SEEK_CUR
then N := OF[FD].pos + N
else if WHENCE = SEEK_END
then choose INODE
with true
in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then N := INODE.size + N};
if ERR = ESUCCESS then OF[FD].pos := N}}
}
readmeta:
vfs_readmeta#(PATH, USER, DIRS, FILES, ASYNCED; MD, NLINK, SIZE, ERR)
precondition true;
postcondition true;
{let INO = ROOT_INO
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS
then choose INODE
with true
in {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if pr(USER, INODE.meta)
then {MD := INODE.meta, SIZE := INODE.size;
if INODE.directory then NLINK := INODE.nsubdirs + 2 else NLINK := INODE.nlink}
else ERR := EACCESS}}
}
writemeta:
vfs_writemeta#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED)
precondition true;
postcondition true;
{let INO = ROOT_INO
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS
then choose INODE
with true
in {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if pw(USER, INODE.meta)
then {INODE.meta := MD; afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED)}
else ERR := EACCESS}}
}
readdir:
vfs_readdir#(PATH, USER, DIRS, FILES, ASYNCED; NAMES, ERR)
precondition true;
postcondition true;
{let INO = ROOT_INO, ISDIR = true, MODE = MODE_R
in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR);
if ERR = ESUCCESS
then choose INODE
with true
in {vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR)}}
}
read-block
: vfs_read_block#(START, END, INODE, DIRS, FILES, ASYNCED; BUF, TOTAL, DONE, ERR)
{let PAGENO = (START + TOTAL) / VFS_PAGE_SIZE, OFFSET = (START + TOTAL) % VFS_PAGE_SIZE, PBUF = mkbuf(VFS_PAGE_SIZE)
in let N = min(END - START + TOTAL, VFS_PAGE_SIZE - OFFSET, INODE.size - START + TOTAL)
in if N ≠ 0
then {afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR);
if ERR = ESUCCESS then {BUF := copy(PBUF, OFFSET, BUF, TOTAL, N); TOTAL := TOTAL + N}}
else DONE := true
}
;
read-loop
: vfs_read_loop#(START, END, INODE, DONE, DIRS, FILES, ASYNCED; BUF, TOTAL, ERR)
{while ERR = ESUCCESS ∧ ¬ DONE do vfs_read_block#(START, END, INODE, DIRS, FILES, ASYNCED; BUF, TOTAL, DONE, ERR)}
;
read:
vfs_read#(FD, USER, DIRS, FILES, ASYNCED; BUF, N, ERR, OF)
precondition N ≤ # BUF;
postcondition true;
{if N ≤ # BUF
then {ERR := ESUCCESS;
if ¬ FD ∈ OF
then ERR := EBADFD
else if OF[FD].mode ≠ MODE_R ∧ OF[FD].mode ≠ MODE_RW
then ERR := EBADFD
else choose INODE
with true
in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if INODE.directory
then ERR := EISDIR
else let START = OF[FD].pos, END = OF[FD].pos + N, TOTAL = 0
in if START ≤ INODE.size
then {let DONE = false
in vfs_read_loop#(START, END, INODE, DONE, DIRS, FILES, ASYNCED; BUF, TOTAL, ERR);
if TOTAL ≠ 0 then ERR := ESUCCESS; OF[FD].pos := OF[FD].pos + TOTAL; N := TOTAL}
else N := 0}}
else abort
}
write-page
: vfs_writepage#(INODE, PAGENO, BUF, TOTAL, OFFSET, N, DIRS; ERR, FILES, ASYNCED)
{let PBUF = mkbuf(VFS_PAGE_SIZE)
in {afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR);
if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS
then {PBUF := copy(BUF, TOTAL, PBUF, OFFSET, N); afs_writepage#(INODE, PAGENO, PBUF, DIRS; ERR, FILES; ASYNCED)}}
}
;
write-block
: vfs_write_block#(START, INODE, BUF, END, DIRS; TOTAL, DONE, ERR, FILES, ASYNCED)
{let PAGENO = (START + TOTAL) / VFS_PAGE_SIZE, OFFSET = (START + TOTAL) % VFS_PAGE_SIZE
in let N = min(END - START + TOTAL, VFS_PAGE_SIZE - OFFSET)
in if N ≠ 0
then {vfs_writepage#(INODE, PAGENO, BUF, TOTAL, OFFSET, N, DIRS; ERR, FILES, ASYNCED);
if ERR = ESUCCESS then TOTAL := TOTAL + N}
else DONE := true
}
;
write-loop
: vfs_write_loop#(START, INODE, END, BUF, DIRS; TOTAL, ERR, FILES, ASYNCED)
{let DONE = false
in while ERR = ESUCCESS ∧ ¬ DONE do vfs_write_block#(START, INODE, BUF, END, DIRS; TOTAL, DONE, ERR, FILES, ASYNCED)
}
;
write:
vfs_write#(FD, BUF, USER; N, ERR, OF, DIRS, FILES, ASYNCED)
precondition N ≤ # BUF;
postcondition true;
{if N ≤ # BUF
then {ERR := ESUCCESS;
if ¬ FD ∈ OF
then ERR := EBADFD
else if OF[FD].mode ≠ MODE_W ∧ OF[FD].mode ≠ MODE_RW
then ERR := EBADFD
else if N ≠ 0
then choose INODE, MODIFIED
with true
in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR);
if ERR = ESUCCESS
then if INODE.directory
then ERR := EISDIR
else let START = OF[FD].pos, END = OF[FD].pos + N, TOTAL = 0, PAGENO = 0, PBUF-OPT = none
in {if ERR = ESUCCESS then PAGENO := INODE.size / VFS_PAGE_SIZE;
if ERR = ESUCCESS
then afs_truncate#
(INODE.size, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED);
if ERR = ESUCCESS
then vfs_write_loop#(START, INODE, END, BUF, DIRS; TOTAL, ERR, FILES, ASYNCED);
if TOTAL ≠ 0 then ERR := ESUCCESS;
if ERR = ESUCCESS
then let SIZE = INODE.size
in {N := TOTAL, END := START + TOTAL;
if TOTAL ≠ 0 ∧ SIZE < END
then {INODE.size := END; afs_check_commit#(DIRS, FILES; ERR; ASYNCED);
if ERR = ESUCCESS then afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED)};
if ERR ≠ ESUCCESS then N := (START ≤ SIZE ⊃ SIZE - START;0), ERR := ESUCCESS;
OF[FD].pos := START + N}}}}
else abort
}
end data asm specification