sync-var.tex

这是我们参加06年全国开源软件的竞赛作品

\maybeclearpage
\section{The {\cf Sync\-Var} structure}


The {\cf \small Sync\-Var}\marginref{SyncVar}{str-SyncVar}{strSyncVar} structure provides \textbf{Id}-style synchronous variables (or memory cells). These variables have two states: \textit{empty} and \textit{full}. An attempt to read a value from an empty variable blocks the calling thread until there is a value available. An attempt to put a value into a variable that is full results in the {\cf \small Put}\marginref{Put}{exn-SYNC_VAR.Put}{exnSYNCVARPut} exception being raised. There are two kinds of synchronous variables: I-variables are write-once, while M-variables are mutable. 
\begin{synopsis}
\item {\kw{signature}} \textcf{SYNC\_\linebreak[0]VAR}\label{sig-SYNC_VAR}
\item {\STRUCTURE} \textcf{SyncVar: SYNC\_\linebreak[0]VAR}\label{str-SyncVar}
\end{synopsis}

\begin{interface}
\Nopagebreak
\item {\index{Put@Put!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{exception}} \textcf{Put}

\Nopagebreak
\item {\index{ivar@ivar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{ivar}
\Nopagebreak
\item {\index{iVar@iVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}ivar}\)}

\Nopagebreak
\item {\index{iPut@iPut!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iPut: \((\alpha\mtoksep{}\mbox{\cf{}ivar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}

\Nopagebreak
\item {\index{iGet@iGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGet: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\)}

\Nopagebreak
\item {\index{iGetEvt@iGetEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGetEvt: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}

\Nopagebreak
\item {\index{iGetPoll@iGetPoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGetPoll: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}

\Nopagebreak
\item {\index{sameIVar@sameIVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf sameIVar: \((\alpha\mtoksep{}\mbox{\cf{}ivar}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}ivar})\rightarrow \mbox{\cf{}bool}\)}

\Nopagebreak
\item {\index{mvar@mvar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{mvar}
\Nopagebreak
\item {\index{mVar@mVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}

\Nopagebreak
\item {\index{mVarInit@mVarInit!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVarInit: \(\alpha\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}

\Nopagebreak
\item {\index{mPut@mPut!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mPut: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}

\Nopagebreak
\item {\index{mTake@mTake!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTake: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}

\Nopagebreak
\item {\index{mTakeEvt@mTakeEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTakeEvt: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}

\Nopagebreak
\item {\index{mGet@mGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGet: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}

\Nopagebreak
\item {\index{mGetEvt@mGetEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGetEvt: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}

\Nopagebreak
\item {\index{mTakePoll@mTakePoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTakePoll: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}

\item {\index{mGetPoll@mGetPoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGetPoll: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}

\Nopagebreak
\item {\index{mSwap@mSwap!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mSwap: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \alpha\)}

\Nopagebreak
\item {\index{mSwapEvt@mSwapEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mSwapEvt: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}

\Nopagebreak
\item {\index{sameMVar@sameMVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf sameMVar: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}mvar})\rightarrow \mbox{\cf{}bool}\)}

\end{interface}

\begin{descr}
\item {\index{Put@Put!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{exception}} \textcf{Put}\label{exn-SYNC_VAR.Put}


\begin{speccomment}
\item 

	This exception is raised when an attempt is made to put a 	value into a value that is already full (see {\cf \small i\-Put} and 	{\cf \small m\-Put}).     \end{speccomment}
\item {\index{ivar@ivar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{ivar}\label{ty-SYNC_VAR.ivar}

\begin{speccomment}
\item 

	This is the type constructor for I-structured variables. 	I-structured variables are write-once variables that provide 	synchronization on read operations. 	They are especially useful for one-shot communications, such 	as reply messages in client/server protocols.     \end{speccomment}
\item {\index{iVar@iVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}ivar}\)}\label{val-SYNC_VAR.iVar}


\begin{speccomment}
\item {\cf \small i\-Var ()           } 
creates a new empty I-variable.     \end{speccomment}
\item {\index{iPut@iPut!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iPut: \((\alpha\mtoksep{}\mbox{\cf{}ivar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}\label{val-SYNC_VAR.iPut}\linebreak[3]\hspace*{\fill}\mbox{~~~~\textrm{raises}~{\cf Put}}


\begin{speccomment}
\item {\cf \small i\-Put (\mbox{\cf \small \textit{iv}}, \mbox{\cf \small \textit{x}})           } 
fills the I-variable \mbox{\cf \small \textit{iv}} with the value \mbox{\cf \small \textit{x}}. 	  Any threads that are blocked on \mbox{\cf \small \textit{iv}} will be resumed. 	  If \mbox{\cf \small \textit{iv}} already has a value in it, then the {\cf \small Put} 	  exception is raised.     \end{speccomment}
\item {\index{iGet@iGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGet: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\)}\label{val-SYNC_VAR.iGet}


\begin{speccomment}
\item {\cf \small i\-Get \mbox{\cf \small \textit{iv}}           } 
returns the contents of the I-variable \mbox{\cf \small \textit{iv}}. 	  If the variable is empty, then the calling thread blocks until 	  the variable becomes full.     \end{speccomment}
\item {\index{iGetEvt@iGetEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGetEvt: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-SYNC_VAR.iGetEvt}


\begin{speccomment}
\item {\cf \small i\-Get\-Evt \mbox{\cf \small \textit{iv}}           } 
returns an event-value that represents the {\cf \small i\-Get} 	  operation on \mbox{\cf \small \textit{iv}}.     \end{speccomment}
\item {\index{iGetPoll@iGetPoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGetPoll: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}\label{val-SYNC_VAR.iGetPoll}


\begin{speccomment}
\item 

	  This is a non-blocking version of {\cf \small i\-Get}. 	  If the corresponding blocking form would block, then it returns 	  {\cf \small NONE}; otherwise 	  it returns {\cf \small SOME} 	  of the variable's contents.     \end{speccomment}
\item {\index{sameIVar@sameIVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf sameIVar: \((\alpha\mtoksep{}\mbox{\cf{}ivar}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}ivar})\rightarrow \mbox{\cf{}bool}\)}\label{val-SYNC_VAR.sameIVar}


\begin{speccomment}
\item {\cf \small same\-IVar (\mbox{\cf \small \textit{iv1}}, \mbox{\cf \small \textit{iv2}})           } 
returns {\cf \small true}, if the \mbox{\cf \small \textit{iv1}} and \mbox{\cf \small \textit{iv2}} are the 	  same I-variable.     \end{speccomment}
\item {\index{mvar@mvar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{mvar}\label{ty-SYNC_VAR.mvar}

\begin{speccomment}
\item 

	This is the type constructor for M-structured variables. 	Unlike {\cf \small ivar} values, M-structured variables may be 	updated multiple times. 	Like I-variables, however, they may only be written if they 	are empty.     \end{speccomment}
\item {\index{mVar@mVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}\label{val-SYNC_VAR.mVar}


\begin{speccomment}
\item {\cf \small m\-Var ()           } 
creates a new empty M-variable.     \end{speccomment}
\item {\index{mVarInit@mVarInit!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVarInit: \(\alpha\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}\label{val-SYNC_VAR.mVarInit}


\begin{speccomment}
\item {\cf \small m\-Var x           } 
creates a new M-variable initialized to \mbox{\cf \small \textit{x}}.     \end{speccomment}
\item {\index{mPut@mPut!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mPut: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}\label{val-SYNC_VAR.mPut}\linebreak[3]\hspace*{\fill}\mbox{~~~~\textrm{raises}~{\cf Put}}


\begin{speccomment}
\item {\cf \small m\-Put (\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{x}})           } 
fills the M-variable \mbox{\cf \small \textit{mv}} with the value \mbox{\cf \small \textit{x}}. 	  Any threads that are blocked on \mbox{\cf \small \textit{mv}} will be resumed. 	  If \mbox{\cf \small \textit{mv}} already has a value in it, then the {\cf \small Put} 	  exception is raised.     \end{speccomment}
\item {\index{mTake@mTake!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTake: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}\label{val-SYNC_VAR.mTake}


\begin{speccomment}
\item {\cf \small m\-Take \mbox{\cf \small \textit{mv}}         } 
removes and returns the contents of the M-variable \mbox{\cf \small \textit{mv}} 	making it empty. 	If the variable is already empty, then the calling thread 	is blocked until a value is available.     \end{speccomment}
\item {\index{mTakeEvt@mTakeEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTakeEvt: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-SYNC_VAR.mTakeEvt}


\begin{speccomment}
\item {\cf \small m\-Take\-Evt \mbox{\cf \small \textit{mv}}           } 
returns an event-value that represents the {\cf \small m\-Take} 	  operation on \mbox{\cf \small \textit{mv}}.     \end{speccomment}
\item {\index{mGet@mGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGet: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}\label{val-SYNC_VAR.mGet}


\begin{speccomment}
\item {\cf \small m\-Get \mbox{\cf \small \textit{mv}}           } 
returns the contents of the M-variable \mbox{\cf \small \textit{mv}} without emptying 	  the variable; if the variable is empty, then the thread blocks until 	  a value is available. 	  It is equivalent to the code: 	  
\begin{code}
let val x = mTake \mbox{\cf \small \textit{mv}} in mPut(\mbox{\cf \small \textit{mv}}, x); x end
	  
\end{code}
     \end{speccomment}
\item {\index{mGetEvt@mGetEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGetEvt: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-SYNC_VAR.mGetEvt}


\begin{speccomment}
\item {\cf \small m\-Get\-Evt \mbox{\cf \small \textit{mv}}           } 
returns an event-value that represents the {\cf \small m\-Get} 	  operation on \mbox{\cf \small \textit{mv}}.     \end{speccomment}
\item {\index{mTakePoll@mTakePoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTakePoll: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}\label{val-SYNC_VAR.mTakePoll}

\item {\index{mGetPoll@mGetPoll!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGetPoll: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}\label{val-SYNC_VAR.mGetPoll}


\begin{speccomment}
\item 

	  These are non-blocking versions of {\cf \small m\-Take} and 	  {\cf \small m\-Get} (respectively). 	  If the corresponding blocking form would block, then they return 	  {\cf \small NONE}; otherwise 	  they return {\cf \small SOME} 	  of the variable's contents.     \end{speccomment}
\item {\index{mSwap@mSwap!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mSwap: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \alpha\)}\label{val-SYNC_VAR.mSwap}


\begin{speccomment}
\item {\cf \small m\-Swap (\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{new\-V}})           } 
puts the value \mbox{\cf \small \textit{new\-V}} into the M-variable \mbox{\cf \small \textit{mv}} and returns 	  the previous contents. 	  If the variable is empty, then the thread blocks until 	  a value is available. 	  It is equivalent to the code: 	  
\begin{code}
let val x = mTake \mbox{\cf \small \textit{mv}} in mPut(\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{new\-V}}); x end
	  
\end{code}
 	  except that {\cf \small m\-Swap} is executed atomically.     \end{speccomment}
\item {\index{mSwapEvt@mSwapEvt!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mSwapEvt: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-SYNC_VAR.mSwapEvt}


\begin{speccomment}
\item {\cf \small m\-Swap\-Evt \mbox{\cf \small \textit{mv}}           } 
returns an event-value that represents the {\cf \small m\-Swap} 	  operation on \mbox{\cf \small \textit{mv}} and \mbox{\cf \small \textit{new\-V}}.     \end{speccomment}
\item {\index{sameMVar@sameMVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf sameMVar: \((\alpha\mtoksep{}\mbox{\cf{}mvar}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}mvar})\rightarrow \mbox{\cf{}bool}\)}\label{val-SYNC_VAR.sameMVar}


\begin{speccomment}
\item {\cf \small same\-MVar (\mbox{\cf \small \textit{mv1}}, \mbox{\cf \small \textit{mv2}})           } 
returns {\cf \small true}, if \mbox{\cf \small \textit{mv1}} and \mbox{\cf \small \textit{mv2}} are the same 	  M-variable.   \end{speccomment}
\end{descr}


I-variables provide a useful mechanism for implementing the reply communication in request/reply protocols. They may also be used to implement incremental data structures and streams.

A disciplined use of M-variables can provide an atomic read-modify-write operation.
\begin{seealso}
{\cf CML} (\pageref{str-CML})
\end{seealso}