[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. 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,

Theorem fsyncdir

vfs_fsyncdir#(PATH, ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR) {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)} }