[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
posix
using posix-pre,
eraseblock
procedures posix_format# nat × bool × nat × metadata : : directory-tree × file-data-store × open-file-handles × bool × error
nondeterministic;
posix_recover# bool : directory-tree × file-data-store × open-file-handles : bool × error nondeterministic;
posix_mkdir# path × metadata × user × file-data-store × open-file-handles : error × directory-tree : bool nondeterministic;
posix_rmdir# path × user × file-data-store × open-file-handles : error × directory-tree : bool nondeterministic;
posix_create# path × metadata × user × open-file-handles : error × directory-tree × file-data-store : bool nondeterministic;
posix_open# path × file-mode × user × directory-tree × file-data-store : nat × error × open-file-handles
nonfunctional
nondeterministic;
posix_close# nat × user × directory-tree : error × file-data-store × open-file-handles nonfunctional nondeterministic;
posix_read# nat × user × directory-tree × file-data-store : buffer × nat × error × open-file-handles nonfunctional nondeterministic;
posix_write# nat × buffer × user × directory-tree : nat × error × file-data-store × open-file-handles : bool nondeterministic;
posix_seek# nat × seekflag × user × directory-tree × file-data-store : nat × error × open-file-handles
nonfunctional
nondeterministic;
posix_rename# path × path × user × open-file-handles : error × directory-tree × file-data-store : bool nondeterministic;
posix_link# path × path × user × file-data-store × open-file-handles : error × directory-tree : bool nondeterministic;
posix_unlink# path × user × open-file-handles : error × directory-tree × file-data-store : bool nondeterministic;
posix_truncate# path × nat × user × directory-tree × open-file-handles : error × file-data-store : bool nondeterministic;
posix_readmeta# path × user × directory-tree × file-data-store × open-file-handles : metadata × nat × nat × error
nonfunctional
nondeterministic;
posix_writemeta# path × metadata × user × open-file-handles : error × directory-tree × file-data-store : bool nondeterministic;
posix_readdir# path × user × directory-tree × file-data-store × open-file-handles : stringset × error
nonfunctional
nondeterministic;
posix_sync# : : bool × error nondeterministic;
posix_fsync# path × bool × user × directory-tree × file-data-store × open-file-handles : : bool × error nondeterministic;
posix_fsyncdir# path × bool × user : : bool × error nondeterministic;
variables NAMES : stringset flexible;
DIR : directory-tree flexible;
TREE : directory-tree flexible;
ROOT : directory-tree flexible;
FS : file-data-store flexible;
PATH : path flexible;
PATH' : path flexible;
MD : metadata flexible;
N : nat flexible;
N0 : nat flexible;
NLINK : nat flexible;
SIZE : nat flexible;
FID : fid flexible;
FD : nat flexible;
OFH : open-file-handles flexible;
FDATA : file-data flexible;
BUF : buffer flexible;
FH : file-handle flexible;
USER : user flexible;
MODE : file-mode flexible;
WHENCE : seekflag flexible;
E : error flexible;
ERR : error flexible;
EXISTS : bool flexible;
PSYNCED : bool flexible;
DOSYNC : bool flexible;
ISDATASYNC : bool flexible;
psynced : bool;
state variables ROOT : directory-tree flexible;
FS : file-data-store flexible;
OFH : open-file-handles flexible;
PSYNCED : bool flexible;
initialization procedure posix_format#
if ERR = ESUCCESS
sequential
invariants root : ⊦ ROOT.dir?;
fids : ⊦ fids-cons(ROOT, FS, OFH);
crash predicate posix-crash(ROOT`, FS`, OFH`, ROOT, FS, OFH)
with crash-neutrality
synchronized predicate
PSYNCED
recovery procedure posix_recover#
if ERR = ESUCCESS
declarations format:
posix_format#(N, DOSYNC, SIZE, MD; ; ROOT, FS, OFH, PSYNCED, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then { ROOT := dnode(MD, ∅), FS := ∅, OFH := ∅, PSYNCED := true, ERR := ESUCCESS
or {ROOT := ?, FS := ?, OFH := ?, PSYNCED := ?; choose E with ⌊E⌋ in ERR := E}}
else abort
}
recover:
posix_recover#(DOSYNC; ROOT, FS, OFH; PSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR ≠ ESUCCESS then ROOT := ?, FS := ?, OFH := ?, PSYNCED := ? else PSYNCED := true}
}
mkdir:
posix_mkdir#(PATH, MD, USER, FS, OFH; ERR, ROOT; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-mkdir(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then ROOT[PATH] := dnode(MD, ∅);
PSYNCED := ?}
}
rmdir:
posix_rmdir#(PATH, USER, FS, OFH; ERR, ROOT; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-rmdir(PATH, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then ROOT := ROOT -- PATH; PSYNCED := ?}
}
create:
posix_create#(PATH, MD, USER, OFH; ERR, ROOT, FS; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-create(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then choose FID with ¬ FID ∈ FS in {ROOT[PATH] := fnode(FID); FS[FID] := mkfile(MD, mkbuf(0))}; PSYNCED := ?}
}
open:
posix_open#(PATH, MODE, USER, ROOT, FS; FD, ERR, OFH)
precondition true;
postcondition true;
{{choose E with pre-open(PATH, MODE, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then let FID = ROOT[PATH].fid in choose N with ¬ N ∈ OFH in {OFH[N] := mkfh(FID, MODE, 0); FD := N}}
}
close:
posix_close#(FD, USER, ROOT; ERR, FS, OFH)
precondition true;
postcondition true;
{{choose E with pre-close(FD, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then let FID = OFH[FD].fid in {OFH := OFH -- FD; if ¬ FID ∈ OFH.fids ∧ ¬ FID ∈ ROOT.fids then FS := FS -- FID}}
}
read:
posix_read#(FD, USER, ROOT, FS; BUF, N, ERR, OFH)
precondition N ≤ # BUF;
postcondition true;
{if N ≤ # BUF
then {choose E with pre-read(FD, N, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then let FH = OFH[FD]
in let FDATA = FS[FH.fid]
in choose N0
with N0 ≤ N ∧ FH.pos + N0 ≤ # FDATA.content
in {N := N0; BUF := copy(FDATA.content, FH.pos, BUF, 0, N); OFH[FD].pos := FH.pos + N}
ifnone N := 0
else N := ?}
else abort
}
write:
posix_write#(FD, BUF, USER, ROOT; N, ERR, FS, OFH; PSYNCED)
precondition N ≤ # BUF;
postcondition true;
{if N ≤ # BUF
then {choose E with pre-write(FD, BUF, N, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then let FH = OFH[FD]
in let FDATA = FS[FH.fid]
in choose N0
with N0 ≤ N
in {N := N0; FDATA.content := splice(BUF, 0, FDATA.content, FH.pos, N); FS[FH.fid] := FDATA;
OFH[FD].pos := FH.pos + N}
else N := ?;
PSYNCED := ?}
else abort
}
seek:
posix_seek#(FD, WHENCE, USER, ROOT, FS; N, ERR, OFH)
precondition true;
postcondition true;
{{choose E with pre-seek(FD, N, WHENCE, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then let FH = OFH[FD]
in let FDATA = FS[FH.fid]
in {if WHENCE = SEEK_CUR then N := FH.pos + N else if WHENCE = SEEK_END then N := # FDATA.content + N; OFH[FD].pos := N}}
}
renam:
posix_rename#(PATH, PATH', USER, OFH; ERR, ROOT, FS; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-renam(PATH, PATH', E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then let DIR = ROOT[PATH], EXISTS = PATH' ∈ ROOT, TREE = ROOT[PATH']
in {ROOT := (ROOT -- PATH)[PATH', DIR];
if EXISTS ∧ ¬ TREE.dir? ∧ ¬ TREE.fid ∈ OFH.fids ∧ ¬ TREE.fid ∈ ROOT.fids then FS := FS -- TREE.fid};
PSYNCED := ?}
}
link:
posix_link#(PATH, PATH', USER, FS, OFH; ERR, ROOT; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-link(PATH, PATH', E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then let FID = ROOT[PATH].fid in ROOT[PATH'] := fnode(FID); PSYNCED := ?}
}
unlink:
posix_unlink#(PATH, USER, OFH; ERR, ROOT, FS; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-unlink(PATH, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then let FID = ROOT[PATH].fid in {ROOT := ROOT -- PATH; if ¬ FID ∈ OFH.fids ∧ ¬ FID ∈ ROOT.fids then FS := FS -- FID};
PSYNCED := ?}
}
truncate:
posix_truncate#(PATH, N, USER, ROOT, OFH; ERR, FS; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-truncate(PATH, N, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then let FID = ROOT[PATH].fid in let BUF = FS[FID].content in FS[FID].content := resize(BUF, N); PSYNCED := ?}
}
readmeta:
posix_readmeta#(PATH, USER, ROOT, FS, OFH; MD, NLINK, SIZE, ERR)
precondition true;
postcondition true;
{{choose E with pre-readmeta(PATH, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS
then if ROOT[PATH].dir?
then MD := ROOT[PATH].meta, NLINK := # ROOT[PATH].subdirs + 2, SIZE := # ROOT[PATH].entries
else let FID = ROOT[PATH].fid in MD := FS[FID].meta, NLINK := count(FID, ROOT.fids), SIZE := # FS[FID].content}
}
writemeta:
posix_writemeta#(PATH, MD, USER, OFH; ERR, ROOT, FS; PSYNCED)
precondition true;
postcondition true;
{{choose E with pre-writemeta(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then if ROOT[PATH].dir? then ROOT[PATH].meta := MD else let FID = ROOT[PATH].fid in FS[FID].meta := MD;
PSYNCED := ?}
}
readdir:
posix_readdir#(PATH, USER, ROOT, FS, OFH; NAMES, ERR)
precondition true;
postcondition true;
{{choose E with pre-readdir(PATH, E, USER, ROOT, FS, OFH) in ERR := E;
if ERR = ESUCCESS then NAMES := dom ROOT[PATH].entries else NAMES := ?}
}
sync:
posix_sync#(; ; PSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); PSYNCED := ERR = ESUCCESS}
}
fsync:
posix_fsync#(PATH, ISDATASYNC, USER, ROOT, FS, OFH; ; PSYNCED, ERR)
precondition true;
postcondition true;
{{choose E with pre-fsync(PATH, ISDATASYNC, E, USER, ROOT, FS, OFH) in ERR := E; PSYNCED := ?}
}
fsyncdir:
posix_fsyncdir#(PATH, ISDATASYNC, USER; ; PSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); PSYNCED := ?}
}
end data asm specification