diff --git a/thesis.tex b/thesis.tex index 6d39dc2..07ec663 100644 --- a/thesis.tex +++ b/thesis.tex @@ -6367,25 +6367,33 @@ state on the next start of the operating system. \subsubsection{File linking and unlinking} % At this point the implementation of \fsname{} is almost feature -complete. We are missing two dual file operations: linking and -unlinking. The former enables us to make shallow copies of files and -the latter enables us to remove copies. The interface is given below. +complete. However, we have yet to implement two dual file operations: +linking and unlinking. The former enables us to associate a new +filename with an existing i-node, thus providing a mechanism for +making shallow copies of files (i.e. the file contents are +shared). The latter lets us dissociate a filename from an i-node, thus +providing a means for removing files. The interface of linking and +unlinking is given below. % \[ \dec{FileLU} \defas \{\ULink : \Record{\String;\String} \opto \UnitType; \UUnlink : \String \opto \UnitType\} \] % The $\ULink$ operation is parameterised by two strings. The first -string is intended to be the name of the original file and the second -string is the name of the copy. The $\UUnlink$ operation takes a -single string argument, which is the name of the file to be removed. +string is the name of the \emph{source} file and the second string is +the \emph{destination} name (i.e. the new name). The $\UUnlink$ +operation takes a single string argument, which is the name of the +file to be removed. + +As before, we bundle the low level operations on the file system state +into their own functions. We start with file linking. % \[ \bl \flink : \Record{\String;\String;\FileSystem} \to \FileSystem \eff \{\Fail : \UnitType \opto \Zero\}\\ \flink\,\Record{src;dest;fs} \defas \bl - \If\;\dec{has}\,\Record{dest;fs.dir}\;\Then\;fs\\ + \If\;\dec{has}\,\Record{dest;fs.dir}\;\Then\;\Do\;\Fail\,\Unit\\ \Else\; \bl \Let\;ino \revto \lookup~\Record{src;fs.dir}\;\In\\ @@ -6399,10 +6407,34 @@ single string argument, which is the name of the file to be removed. \el \] % +The function $\flink$ checks whether the destination filename, $dest$, +already exists in the directory. If it exists then the function raises +the $\Fail$ exception. Otherwise it looks up the index of the i-node, +$ino$, associated with the source file, $src$. Next, the directory is +extended with the destination filename, which gets associated with +this index, meaning $src$ and $dest$ both share the same +i-node. Finally, the link count of the i-node at index $ino$ gets +incremented, and the function returns the updated file system state. +% + +The semantics of file unlinking is slightly more complicated as an +i-node may become unlinked, meaning that it needs to garbage collected +along with its file contents in the data region. To implement file +removal we make use of another standard operation on association +lists. +% \[ \remove : \Record{\alpha;\Record{\alpha;\beta}} \to \Record{\alpha;\beta} \] % +The first parameter to $\remove$ is the key associated with the entry +to be removed from the association list, which is given as the second +parameter. If the association list does not have an entry for the +given key, then the function behaves as the identity. The behaviour of +the function in case of multiple entries for a single key does not +matter as our system is carefully set up to ensure that each key has +an unique entry. +% \[ \bl \funlink : \Record{\String;\FileSystem} \to \FileSystem \eff \{\Fail : \UnitType \opto \Zero\}\\ @@ -6428,7 +6460,7 @@ single string argument, which is the name of the file to be removed. \el\\ \In\;\Record{fs\;\With\;dir = dir'; ilist = ilist'; dreg = dreg'} \el\\ - \Else\; fs + \Else\; \Do\;\Fail\,\Unit \el \el \] @@ -6453,7 +6485,7 @@ single string argument, which is the name of the file to be removed. \bl \faild\,\Record{\Unit; \lambda\Unit.\\ \quad\bl - \Let\;fs = \funlink\,\Record{src;dest;\Uget\,\Unit}\\ + \Let\;fs = \funlink\,\Record{fname;\Uget\,\Unit}\\ \In\;\Uput~fs}; resume\,\Unit \el \el