| root[q + str '] = dnode(md1, ∅), dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), dirs[entries[str]] = mkdir(0, md0, # links(entries[str], dirs), m2, ∅), c_inode = p_inode0, dent = mkdentry(str, entries[str]), err = ESUCCESS, fs = abs-files(files), inode = mkinode(ino1, md, true, # links(ino1, dirs), m1, # entries), p_ino = p_inode.ino, p_inode = inode, p_inode0 = mkinode(entries[str], md0, true, # links(entries[str], dirs), m2, 0), root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), entries[str] ∈ dirs, ino1 ∈ dirs, str ∈ entries, psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [dirs[p_ino].entries := dirs[p_ino].entries -- dent.name; dirs[p_ino].size := dirs[p_ino].size - 1; dirs[p_ino].nsubdirs := dirs[p_ino].nsubdirs - 1; let ino = dent.ino in afs_drop_nlink#(ino; dirs, files); dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS; asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1)) |
dirs0[entries[str]] = mkdir(0, md0, # links(entries[str], dirs0), m2, ∅), dirs0[ino1] = mkdir(# entries, md, # links(ino1, dirs0), m1, entries), root[q + str '] = dnode(md1, ∅), c_inode = p_inode0, dent = mkdentry(str, entries[str]), err = ESUCCESS, fs = abs-files(files), inode = mkinode(ino1, md, true, # links(ino1, dirs0), m1, # entries), p_ino = p_inode.ino, p_inode = inode, p_inode0 = mkinode(entries[str], md0, true, # links(entries[str], dirs0), m2, 0), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pre-rmdir(p_inode, c_inode, dent, dirs0, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries, ino1 ∈ dirs0, entries[str] ∈ dirs0, dirs ≡ dirs0[p_ino, dirs0[p_ino].entries:= (dirs0[p_ino].entries -- dent.name)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [dirs[p_ino].size := dirs[p_ino].size - 1; dirs[p_ino].nsubdirs := dirs[p_ino].nsubdirs - 1; let ino = dent.ino in afs_drop_nlink#(ino; dirs, files); dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS; asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1))