[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
aubifs
using aubifs-pre,
aubifs-replay
,
aubifs-internal-asm
procedures aubifs_iget_check# nat × node-index × node-index × key-set × key-set × node-store × address-list × bool : bool × inode × error
nonfunctional
nondeterministic;
aubifs_iget# nat × node-index × node-index × key-set × key-set × node-store × address-list × bool : inode × error
nonfunctional
nondeterministic;
aubifs_lookup# nat × node-index × node-index × key-set × key-set × node-store × address-list × bool : dentry × error
nonfunctional
nondeterministic;
aubifs_create#
metadata × node-index × key-set × key-set : inode × inode × dentry × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_mkdir#
metadata × node-index × key-set × key-set : inode × inode × dentry × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_unlink# node-index × key-set : inode × inode × dentry × error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rmdir# node-index × key-set : inode × inode × dentry × error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_link#
dentry × node-index × key-set × key-set : inode × inode × dentry × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rename#
node-index × key-set : inode × inode × inode × inode × dentry × dentry × error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rename_overwrite_reparent#
bool × inode × node-index × key-set
: inode × inode × inode × dentry × dentry × error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rename_overwrite_keep_parent#
bool × inode × node-index × key-set : inode × inode × dentry × dentry × error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rename_new_reparent#
bool × inode × node-index × key-set × key-set : inode × inode × dentry × dentry × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_rename_new_keep_parent#
bool × inode × node-index × key-set × key-set : inode × dentry × dentry × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_readpage# inode × nat × node-index × node-index × key-set × key-set × node-store × address-list × bool : buffer × error
nonfunctional
nondeterministic;
aubifs_writepage# inode × nat × buffer × node-index × key-set × key-set : error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_readdir# inode × node-index × node-index × key-set × key-set × node-store × address-list × bool : stringset × error
nonfunctional
nondeterministic;
aubifs_truncate#
nat × nat × node-index × key-set × key-set : buffer-opt × inode × bool × error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_write_inode# inode × node-index × key-set × key-set : error × node-index × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_evict# inode × node-index × key-set × node-store × address-list × bool : error × node-index × key-set
nonfunctional
nondeterministic;
aubifs_replay# bool : node-index × node-index × key-set × key-set × node-store × address-list × bool : error nondeterministic;
aubifs_replaylog# address-list × node-index × key-set × key-set × node-store × address-list × bool : error × node-index
nonfunctional
nondeterministic;
aubifs_replayorphans# node-index × key-set × node-store × address-list × bool : key-set × error × node-index × key-set
nonfunctional
nondeterministic;
aubifs_replayone# address × node-index × key-set × key-set × node-store × address-list × bool : error × node-index
nonfunctional
nondeterministic;
aubifs_check_commit# node-index × key-set : error × node-index × key-set × node-store × address-list × bool
nonfunctional
nondeterministic;
aubifs_gc# node-index × key-set × key-set : node-index × node-store × address-list × bool nonfunctional nondeterministic;
aubifs_format# nat × bool × nat × metadata : node-index × node-index × key-set × key-set × node-store × address-list × bool : error
nondeterministic;
aubifs_sync# node-index × node-index × key-set × key-set × node-store × address-list : bool : error nondeterministic;
aubifs_fsync# inode × bool : : error ;
aubifs_fsyncdir# inode × bool : : error ;
variables FS0 : node-store flexible;
RI0 : node-index flexible;
FI0 : node-index flexible;
RO0 : key-set flexible;
FO0 : key-set flexible;
LOG0 : address-list flexible;
OLD_INO : nat flexible;
P_INO : nat flexible;
NEW_INO : nat flexible;
P_INODE : inode flexible;
C_INODE : inode flexible;
INODE : inode flexible;
OLD_INODE : inode flexible;
NEW_INODE : inode flexible;
DENTRY_INODE : inode flexible;
OLD_DENT_INODE : inode flexible;
NEW_DENT_INODE : inode flexible;
PARENT_INODE : inode flexible;
OLD_PARENT_INODE : inode flexible;
OLD_CHILD_INODE : inode flexible;
NEW_PARENT_INODE : inode flexible;
NEW_CHILD_INODE : inode flexible;
A_OLD_PARENT_INODE : inode flexible;
A_NEW_PARENT_INODE : inode flexible;
A_DENTRY_INODE : inode flexible;
A_NEW_CHILD_INODE : inode flexible;
DENT : dentry flexible;
DENT0 : dentry flexible;
OLD_DENT : dentry flexible;
NEW_DENT : dentry flexible;
PAGENO : nat flexible;
OFFSET : nat flexible;
END : nat flexible;
INO : nat flexible;
N : nat flexible;
SIZE : nat flexible;
LINK : nat flexible;
SUBDIRS : nat flexible;
PBUF : buffer flexible;
ADR : address flexible;
ADR1 : address flexible;
ADR2 : address flexible;
ADR3 : address flexible;
ADR4 : address flexible;
ADR5 : address flexible;
KEY : key flexible;
KS : key-set flexible;
AX : address-list flexible;
MD : metadata flexible;
IS_DIR : bool flexible;
OVERWRITE : bool flexible;
REPARENT : bool flexible;
IDENTITY : bool flexible;
ERR : error flexible;
NAMES : stringset flexible;
MODIFIED : bool flexible;
ISDATASYNC : bool flexible;
PBUF-OPT : buffer-opt flexible;
pageno : nat;
initialization procedure aubifs_format#
if ERR = ESUCCESS
sequential
invariants ubifs-cons : ⊦ ubifs-cons(FS, RI, RO, FI, FO, LOG);
replay-cons : ⊦ replay-cons-strong(FS, RI, RO, FI, FO, LOG);
file-node-cons : ⊦ file-node-cons(FS, RI);
orphans-cons : ⊦ orphans-cons(FS, RI, RO);
recovery procedure aubifs_replay#
if ERR = ESUCCESS
declarations iget-check
: aubifs_iget_check#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, INODE, ERR)
{choose ND, KEY
with true
in if ERR = ESUCCESS
then {KEY := inodekey(INO); aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR);
if ERR = ESUCCESS ∧ EXISTS
then INODE := mkinode(INO, ND.meta, ND.directory, ND.nlink, (ND.directory ⊃ ND.nsubdirs;0), ND.size)}
}
;
iget:
aubifs_iget#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; INODE, ERR)
precondition pre-iget(INO, FS, RI);
postcondition true;
{if pre-iget(INO, FS, RI)
then let EXISTS = ? in {ERR := ESUCCESS; aubifs_iget_check#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, INODE, ERR)}
else abort
}
lookup:
aubifs_lookup#(P_INO, RI, FI, RO, FO, FS, LOG, CSYNCED; DENT, ERR)
precondition pre-lookup(P_INO, DENT, FS, RI, RO);
postcondition true;
{if pre-lookup(P_INO, DENT, FS, RI, RO)
then choose EXISTS, ND, KEY
with true
in {ERR := ESUCCESS; KEY := dentrykey(P_INO, DENT.name);
aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR);
if ERR = ESUCCESS
then if EXISTS then DENT := mkdentry(DENT.name, ND.ino), ERR := ESUCCESS else DENT := negdentry(DENT.name), ERR := ENOENT}
else abort
}
create:
aubifs_create#(MD, FI, RO, FO; P_INODE, C_INODE, DENT, ERR, RI, FS, LOG, CSYNCED)
precondition pre-create(P_INODE, DENT, MD, FS, RI, RO);
postcondition true;
{if pre-create(P_INODE, DENT, MD, FS, RI, RO)
then choose ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3
with true
in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name);
aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY3);
ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size + 1);
ND2 := dentrynode(KEY2, KEY3.ino); ND3 := inodenode(KEY3, MD, false, 1, 0, 0);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); DENT := mkdentry(DENT.name, KEY3.ino);
P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size);
C_INODE := mkinode(KEY3.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
mkdir:
aubifs_mkdir#(MD, FI, RO, FO; P_INODE, C_INODE, DENT, ERR, RI, FS, LOG, CSYNCED)
precondition pre-mkdir(P_INODE, DENT, MD, FS, RI, RO);
postcondition true;
{if pre-mkdir(P_INODE, DENT, MD, FS, RI, RO)
then choose ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3
with true
in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name);
aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY3);
ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs + 1, P_INODE.size + 1);
ND2 := dentrynode(KEY2, KEY3.ino); ND3 := inodenode(KEY3, MD, true, 1, 0, 0);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); DENT := mkdentry(DENT.name, KEY3.ino);
P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size);
C_INODE := mkinode(KEY3.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
unlink:
aubifs_unlink#(FI, FO; P_INODE, C_INODE, DENT, ERR, RI, RO, FS, LOG, CSYNCED)
precondition pre-unlink(P_INODE, C_INODE, DENT, FS, RI, RO);
postcondition true;
{if pre-unlink(P_INODE, C_INODE, DENT, FS, RI, RO)
then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3
with INO = C_INODE.ino
in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); KEY3 := inodekey(C_INODE.ino);
ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size - 1);
ND2 := dentrynode(KEY2, 0);
ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink - 1, C_INODE.nsubdirs, C_INODE.size);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_remove#(KEY2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
if C_INODE.nlink = 1 then aubifs_core_orphans_insert#(KEY3, RI, FI, FO, FS, LOG, CSYNCED; RO);
DENT := negdentry(DENT.name);
P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size);
C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
rmdir:
aubifs_rmdir#(FI, FO; P_INODE, C_INODE, DENT, ERR, RI, RO, FS, LOG, CSYNCED)
precondition pre-rmdir(P_INODE, C_INODE, DENT, FS, RI, RO);
postcondition true;
{if pre-rmdir(P_INODE, C_INODE, DENT, FS, RI, RO)
then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3
with INO = C_INODE.ino
in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); KEY3 := inodekey(C_INODE.ino);
ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs - 1, P_INODE.size - 1);
ND2 := dentrynode(KEY2, 0);
ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink - 1, C_INODE.nsubdirs, C_INODE.size);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_remove#(KEY2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_orphans_insert#(KEY3, RI, FI, FO, FS, LOG, CSYNCED; RO); DENT := negdentry(DENT.name);
P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size);
C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
link:
aubifs_link#(OLD_DENT, FI, RO, FO; P_INODE, C_INODE, NEW_DENT, ERR, RI, FS, LOG, CSYNCED)
precondition pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, FS, RI, RO);
postcondition true;
{if pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, FS, RI, RO)
then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3
with INO = C_INODE.ino
in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, NEW_DENT.name); KEY3 := inodekey(INO);
ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size + 1);
ND2 := dentrynode(KEY2, INO);
ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink + 1, C_INODE.nsubdirs, C_INODE.size);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); NEW_DENT := mkdentry(NEW_DENT.name, INO);
P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size);
C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
renam:
aubifs_rename#
(FI, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED)
precondition pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO);
postcondition true;
{if pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO)
then let OVERWRITE = NEW_DENT.dentry?, REPARENT = OLD_PARENT_INODE.ino ≠ NEW_PARENT_INODE.ino, IS_DIR = OLD_CHILD_INODE.directory
in if REPARENT
then if OVERWRITE
then aubifs_rename_overwrite_reparent#
(IS_DIR, OLD_CHILD_INODE, FI, FO
; OLD_PARENT_INODE, NEW_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED)
else aubifs_rename_new_reparent#
(IS_DIR, OLD_CHILD_INODE, FI, RO, FO
; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED)
else {if OVERWRITE
then aubifs_rename_overwrite_keep_parent#
(IS_DIR, OLD_CHILD_INODE, FI, FO
; OLD_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED)
else aubifs_rename_new_keep_parent#
(IS_DIR, OLD_CHILD_INODE, FI, RO, FO; OLD_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED);
NEW_PARENT_INODE := OLD_PARENT_INODE}
else abort
}
rename-overwrite-reparent:
aubifs_rename_overwrite_reparent#
(IS_DIR, OLD_CHILD_INODE, FI, FO
; OLD_PARENT_INODE, NEW_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED
)
precondition pre-rename-overwrite-reparent
(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
;
postcondition true;
{if pre-rename-overwrite-reparent
(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
then choose KEY1, KEY2, KEY3, KEY4, KEY5, ND1, ND2, ND3, ND4, ND5, ADR1, ADR2, ADR3, ADR4, ADR5
with true
in {KEY1 := dentrykey(OLD_PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0);
KEY2 := dentrykey(NEW_PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino);
KEY3 := inodekey(OLD_PARENT_INODE.ino);
ND3
:= inodenode
(KEY3, OLD_PARENT_INODE.meta, OLD_PARENT_INODE.directory, OLD_PARENT_INODE.nlink,
OLD_PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0), OLD_PARENT_INODE.size - 1);
KEY4 := inodekey(NEW_PARENT_INODE.ino);
ND4
:= inodenode
(KEY4, NEW_PARENT_INODE.meta, NEW_PARENT_INODE.directory, NEW_PARENT_INODE.nlink, NEW_PARENT_INODE.nsubdirs,
NEW_PARENT_INODE.size);
KEY5 := inodekey(NEW_DENT.ino);
ND5
:= inodenode
(KEY5, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink - 1, NEW_CHILD_INODE.nsubdirs,
NEW_CHILD_INODE.size);
aubifs_core_journal_add5#(ND1, ND2, ND3, ND4, ND5, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, ADR5, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY5, ADR5, FI, RO, FO, FS, LOG, CSYNCED; RI);
if ND5.nlink = 0 then aubifs_core_orphans_insert#(KEY5, RI, FI, FO, FS, LOG, CSYNCED; RO);
NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name);
OLD_PARENT_INODE := mkinode(OLD_PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size);
NEW_CHILD_INODE := mkinode(NEW_CHILD_INODE.ino, ND5.meta, ND5.directory, ND5.nlink, ND5.nsubdirs, ND5.size)}}
else abort
}
rename-overwrite-keep-parent:
aubifs_rename_overwrite_keep_parent#
(IS_DIR, OLD_CHILD_INODE, FI, FO; PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED)
precondition pre-rename-overwrite-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
;
postcondition true;
{if pre-rename-overwrite-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
then choose KEY1, KEY2, KEY3, KEY4, ND1, ND2, ND3, ND4, ADR1, ADR2, ADR3, ADR4
with true
in let IDENTITY = OLD_DENT = NEW_DENT
in {KEY1 := dentrykey(PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0);
KEY2 := dentrykey(PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino);
KEY3 := inodekey(PARENT_INODE.ino); KEY4 := inodekey(NEW_DENT.ino);
if ¬ IDENTITY
then {ND3
:= inodenode
(KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0),
PARENT_INODE.size - 1);
ND4
:= inodenode
(KEY4, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink - 1, NEW_CHILD_INODE.nsubdirs,
NEW_CHILD_INODE.size)}
else {ND3
:= inodenode
(KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs, PARENT_INODE.size);
ND4
:= inodenode
(KEY4, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink, NEW_CHILD_INODE.nsubdirs,
NEW_CHILD_INODE.size)};
aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI);
if ND4.nlink = 0 then aubifs_core_orphans_insert#(KEY4, RI, FI, FO, FS, LOG, CSYNCED; RO);
NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name);
PARENT_INODE := mkinode(PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size);
NEW_CHILD_INODE := mkinode(NEW_CHILD_INODE.ino, ND4.meta, ND4.directory, ND4.nlink, ND4.nsubdirs, ND4.size)}}
else abort
}
rename-new-reparent:
aubifs_rename_new_reparent#
(IS_DIR, OLD_CHILD_INODE, FI, RO, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED)
precondition pre-rename-new-reparent(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
;
postcondition true;
{if pre-rename-new-reparent(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
then choose KEY1, KEY2, KEY3, KEY4, ND1, ND2, ND3, ND4, ADR1, ADR2, ADR3, ADR4
with true
in {KEY1 := dentrykey(OLD_PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0);
KEY2 := dentrykey(NEW_PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino);
KEY3 := inodekey(OLD_PARENT_INODE.ino);
ND3
:= inodenode
(KEY3, OLD_PARENT_INODE.meta, OLD_PARENT_INODE.directory, OLD_PARENT_INODE.nlink,
OLD_PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0), OLD_PARENT_INODE.size - 1);
KEY4 := inodekey(NEW_PARENT_INODE.ino);
ND4
:= inodenode
(KEY4, NEW_PARENT_INODE.meta, NEW_PARENT_INODE.directory, NEW_PARENT_INODE.nlink,
NEW_PARENT_INODE.nsubdirs + (IS_DIR ⊃ 1;0), NEW_PARENT_INODE.size + 1);
aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI);
NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name);
OLD_PARENT_INODE := mkinode(OLD_PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size);
NEW_PARENT_INODE := mkinode(NEW_PARENT_INODE.ino, ND4.meta, ND4.directory, ND4.nlink, ND4.nsubdirs, ND4.size)}}
else abort
}
rename-new-keep-parent:
aubifs_rename_new_keep_parent#(IS_DIR, OLD_CHILD_INODE, FI, RO, FO; PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED)
precondition pre-rename-new-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, FS, RI, RO)
∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
;
postcondition true;
{if pre-rename-new-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, FS, RI, RO) ∧ (IS_DIR ↔ OLD_CHILD_INODE.directory)
then choose KEY1, KEY2, KEY3, ND1, ND2, ND3, ADR1, ADR2, ADR3
with true
in {KEY1 := dentrykey(PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0);
KEY2 := dentrykey(PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino);
KEY3 := inodekey(PARENT_INODE.ino);
ND3
:= inodenode(KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs, PARENT_INODE.size);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI);
NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name);
PARENT_INODE := mkinode(PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}}
else abort
}
readpage:
aubifs_readpage#(INODE, PAGENO, RI, FI, RO, FO, FS, LOG, CSYNCED; PBUF, ERR)
precondition pre-readpage(INODE, PAGENO, PBUF, FS, RI);
postcondition true;
{if pre-readpage(INODE, PAGENO, PBUF, FS, RI)
then choose KEY, EXISTS, ND
with true
in {ERR := ESUCCESS; KEY := datakey(INODE.ino, PAGENO);
aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR);
if ERR = ESUCCESS then if EXISTS then PBUF := copy(ND.data, 0, PBUF, 0, VFS_PAGE_SIZE) else PBUF := fill(PBUF, zero)}
else abort
}
writepage:
aubifs_writepage#(INODE, PAGENO, PBUF, FI, RO, FO; ERR, RI, FS, LOG, CSYNCED)
precondition pre-writepage(INODE, PAGENO, PBUF, FS, RI);
postcondition true;
{if pre-writepage(INODE, PAGENO, PBUF, FS, RI)
then choose EXISTS, KEY1, ADR1, ND1
with EXISTS
in let INO = INODE.ino
in {KEY1 := datakey(INO, PAGENO); ND1 := datanode(KEY1, PBUF);
aubifs_core_journal_add1#(ND1, RI, FI, RO, FO; ADR1, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI)
else if ¬ EXISTS then aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI)}
else abort
}
readdir:
aubifs_readdir#(INODE, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES, ERR)
precondition pre-readdir(INODE.ino, FS, RI);
postcondition true;
{if pre-readdir(INODE.ino, FS, RI)
then choose KEY
with true
in {KEY := inodekey(INODE.ino); aubifs_core_index_entries#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES; ERR)}
else abort
}
truncate:
aubifs_truncate#(N, PAGENO, FI, RO, FO; PBUF-OPT, INODE, MODIFIED, ERR, RI, FS, LOG, CSYNCED)
precondition pre-truncate(INODE, N, PAGENO, PBUF-OPT, FS, RI, RO);
postcondition true;
{if pre-truncate(INODE, N, PAGENO, PBUF-OPT, FS, RI, RO)
then choose ADR1, ADR2, ADR3, EXISTS
with true
in let KEY1 = inodekey(INODE.ino), KEY2 = inodekey(INODE.ino), OFFSET = INODE.size % VFS_PAGE_SIZE, SIZE = min(N, INODE.size)
in let KEY3 = datakey(INODE.ino, PAGENO), ND1 = truncnode(KEY1, SIZE),
ND2 = inodenode(KEY2, INODE.meta, INODE.directory, INODE.nlink, INODE.nsubdirs, N), ND3 = ?
in {if INODE.size ≤ N ∧ OFFSET ≠ 0
then if PBUF-OPT.some?
then {ND3 := datanode(KEY3, PBUF-OPT.buf); EXISTS := true, ERR := ESUCCESS}
else aubifs_core_index_lookup#(KEY3, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND3; ERR)
else EXISTS := false, ERR := ESUCCESS;
if ERR = ESUCCESS
then if EXISTS
then {ND3.data := fill(ND3.data, zero, OFFSET, VFS_PAGE_SIZE - OFFSET);
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS then aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI)}
else aubifs_core_journal_add2#(ND1, ND2, RI, FI, RO, FO; ADR1, ADR2, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS
then {aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_truncate#(KEY1, SIZE, FI, RO, FO, FS, LOG, CSYNCED; RI); MODIFIED := EXISTS;
INODE := mkinode(INODE.ino, ND2.meta, ND2.directory, ND2.nlink, ND2.nsubdirs, ND2.size);
if MODIFIED then PBUF-OPT := some(ND3.data)}}
else abort
}
write-inode:
aubifs_write_inode#(INODE, FI, RO, FO; ERR, RI, FS, LOG, CSYNCED)
precondition pre-write-inode(INODE, FS, RI, RO);
postcondition true;
{if pre-write-inode(INODE, FS, RI, RO)
then choose KEY, ND, ADR
with true
in {KEY := inodekey(INODE.ino); ND := inodenode(KEY, INODE.meta, INODE.directory, INODE.nlink, INODE.nsubdirs, INODE.size);
aubifs_core_journal_add1#(ND, RI, FI, RO, FO; ADR, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS then aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)}
else abort
}
evict:
aubifs_evict#(INODE, FI, FO, FS, LOG, CSYNCED; ERR, RI, RO)
precondition pre-evict(INODE.ino, FS, RI, RO);
postcondition true;
{if pre-evict(INODE.ino, FS, RI, RO)
then {choose EXISTS, KEY
with KEY = inodekey(INODE.ino)
in {aubifs_core_orphans_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS);
if EXISTS
then {aubifs_core_index_truncate#(KEY, 0, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO);
aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI)}};
ERR := ESUCCESS}
else abort
}
replay:
aubifs_replay#(DOSYNC; RI, FI, RO, FO, FS, LOG, CSYNCED; ERR)
precondition true;
postcondition true;
{let AX = ?, KS = ?
in {aubifs_core_recover#(DOSYNC; AX, KS, FI, RO, FO, LOG, FS; RI, CSYNCED, ERR);
if ERR = ESUCCESS then aubifs_replayorphans#(FI, FO, FS, LOG, CSYNCED; KS, ERR, RI, RO);
if ERR = ESUCCESS then aubifs_replaylog#(AX, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI);
if ERR = ESUCCESS then aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)}
}
replaylog
: aubifs_replaylog#(AX, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI)
{while ERR = ESUCCESS ∧ AX ≠ []
do {/* (replaylog-prog
: invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ )
∧ (ERR = ESUCCESS → (∃ ax0. AX` = ax0 + AX ∧ replay-safe(AX, FS, RI) ∧ RI = replay-log(ax0, FS`, RI`)))
wfbound # AX)
*/;
let ADR = AX.head in aubifs_replayone#(ADR, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI); AX := AX.tail}
}
;
replayorphans
: aubifs_replayorphans#(FI, FO, FS, LOG, CSYNCED; KS, ERR, RI, RO)
{while KS ≠ ∅
do {/* (replayorphans-prepost: invariant KS = RO ∧ RO ⊆ RO` ∧ RI ⊖ RO = RI` ⊖ RO` ∧ KS.inodes? wfbound # KS) */;
choose KEY
with KEY ∈ KS
in {aubifs_core_index_truncate#(KEY, 0, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI);
aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO); KS := KS -- KEY}}
}
;
replayone
: aubifs_replayone#(ADR, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI)
{choose ND, EXISTS
with true
in {aubifs_core_journal_get#(ADR, RI, FI, RO, FO, FS, LOG, CSYNCED; ND; ERR);
if ERR = ESUCCESS
then {if ND.inode?
then if ND.nlink ≠ 0 ∨ ND.key.ino = ROOT_INO
then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)
else {if ¬ ND.directory then aubifs_core_index_truncate#(ND.key, 0, FI, RO, FO, FS, LOG, CSYNCED; RI);
if ERR = ESUCCESS then aubifs_core_index_remove#(ND.key, FI, RO, FO, FS, LOG, CSYNCED; RI)};
if ND.dentry?
then if ND.ino ≠ 0
then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)
else aubifs_core_index_remove#(ND.key, FI, RO, FO, FS, LOG, CSYNCED; RI);
if ND.data?
then {let KEY = inodekey(ND.key.ino)
in aubifs_core_index_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS; ERR);
if ERR = ESUCCESS ∧ EXISTS then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)};
if ND.trunc? then aubifs_core_index_truncate#(ND.key, ND.size, FI, RO, FO, FS, LOG, CSYNCED; RI)}}
}
;
check-commit:
aubifs_check_commit#(RI, RO; ERR, FI, FO, FS, LOG, CSYNCED)
precondition true;
postcondition true;
{aubifs_core_check_commit#(RI, RO; FI, FO, FS, LOG, CSYNCED; ERR)
}
gc:
aubifs_gc#(FI, RO, FO; RI, FS, LOG, CSYNCED)
precondition orphans-cons(FS, RI, RO);
postcondition true;
{if orphans-cons(FS, RI, RO) then aubifs_core_journal_gc#(FI, RO, FO; RI, FS, LOG; CSYNCED) else abort
}
format:
aubifs_format#(VOLSIZE, DOSYNC, SIZE, MD; RI, FI, RO, FO, FS, LOG, CSYNCED; ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {aubifs_core_format#(VOLSIZE, SIZE, DOSYNC; ; RI, FI, RO, FO, FS, LOG, CSYNCED, ERR);
if ERR = ESUCCESS
then let KEY = inodekey(ROOT_INO), ADR = ?
in let ND = inodenode(KEY, MD, true, 0, 0, 0)
in {aubifs_core_journal_add1#(ND, RI, FI, RO, FO; ADR, FS, LOG; CSYNCED, ERR);
if ERR = ESUCCESS then aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI);
if ERR = ESUCCESS then aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)}}
else abort
}
sync:
aubifs_sync#(RI, FI, RO, FO, FS, LOG; CSYNCED; ERR)
precondition true;
postcondition true;
{aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)
}
fsync:aubifs_fsync#(INODE, ISDATASYNC; ; ERR) precondition true; postcondition true;{ERR := ESUCCESS}
fsyncdir:aubifs_fsyncdir#(INODE, ISDATASYNC; ; ERR) precondition true; postcondition true;{ERR := ESUCCESS}
end data asm specification