| dirs0[ino2] = mkdir(# entries, md1, # links(ino2, dirs0), m3, entries), files[entries0[str]] = mkfile(m, md, # links(entries0[str], dirs0), content), dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), c_inode = mkinode(entries0[str], md, false, # links(entries0[str], dirs0), 0, m), err = ESUCCESS, fs = abs-files(files), new_dent = negdentry(str0), new_inode = mkinode(ino2, md1, true, # links(ino2, dirs0), m3, # entries), old_dent = mkdentry(str, entries0[str]), p_ino = p_inode.ino, p_inode = new_inode, old_dent.dentry?, root.dir?, root[q].dir?, root[q0].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q0, ROOT_INO, ino2, dirs0, files), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pre-link(p_inode, c_inode, old_dent, new_dent, dirs0, files), pw(user, md1), px(user, md0), px(user, md1), px-parent(user, q0, ROOT_INO, dirs0, files), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries0, entries0[str] ∈ files, ino1 ∈ dirs0, ino2 ∈ dirs0, dirs1 ≡ dirs0[p_ino, dirs0[p_ino].entries:= dirs0[p_ino].entries[new_dent.name, old_dent.ino]], dirs ≡ dirs1[p_ino, dirs1[p_ino].size:= (dirs1[p_ino].size + 1)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO ⊦ [let ino = old_dent.ino in afs_inc_nlink#(ino; dirs, files); new_dent := mkdentry(new_dent.name, old_dent.ino); 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(old_dent.ino, dirs, files); err := ESUCCESS; asynced := ?] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_link#(q + str ', q0 + str0 ', user, fs, abs-of(of); err2, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err2)), root[q + str '].dir?, str0 ∈ entries, entries0[str] ∈ dirs0 |
dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), files[entries0[str]] = mkfile(m, md, # links(entries0[str], dirs0), content), dirs0[ino2] = mkdir(# entries, md1, # links(ino2, dirs0), m3, entries), c_inode = mkinode(entries0[str], md, false, # links(entries0[str], dirs0), 0, m), err = ESUCCESS, fs = abs-files(files), ino = old_dent.ino, new_dent = negdentry(str0), new_inode = mkinode(ino2, md1, true, # links(ino2, dirs0), m3, # entries), old_dent = mkdentry(str, entries0[str]), p_ino = p_inode.ino, p_inode = new_inode, old_dent.dentry?, root[q0].dir?, root[q].dir?, root.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), ispath(q0, ROOT_INO, ino2, dirs0, files), of-cons(of, dirs0, files), pre-link(p_inode, c_inode, old_dent, new_dent, dirs0, files), pw(user, md1), px(user, md1), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files), px-parent(user, q0, ROOT_INO, dirs0, files), ino2 ∈ dirs0, ino1 ∈ dirs0, entries0[str] ∈ files, str ∈ entries0, dirs ≡ dirs1[p_ino, dirs1[p_ino].size:= (dirs1[p_ino].size + 1)], dirs1 ≡ dirs0[p_ino, dirs0[p_ino].entries:= dirs0[p_ino].entries[new_dent.name, old_dent.ino]], psynced → asynced0, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [afs_inc_nlink#(ino; dirs, files); new_dent := mkdentry(new_dent.name, old_dent.ino); 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(old_dent.ino, dirs, files); err := ESUCCESS; asynced := ?] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_link#(q + str ', q0 + str0 ', user, fs, abs-of(of); err2, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err2)), root[q + str '].dir?, entries0[str] ∈ dirs0, str0 ∈ entries