cml.tex

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

\begin{speccomment}
\item {\cf \small same\-Tid (\mbox{\cf \small \textit{tid1}}, \mbox{\cf \small \textit{tid2}})           } 
returns true, if the two thread IDs are the same ID.     \end{speccomment}
\item {\index{compareTid@compareTid!CML@\textcf{CML}}}{\kw{val}} {\cf compareTid: \((\mbox{\cf{}thread\_id}\mtoksep{}\verb,*,\mtoksep{}\mbox{\cf{}thread\_id})\rightarrow \mbox{\cf{}order}\)}\label{val-CML.compareTid}


\begin{speccomment}
\item {\cf \small compare\-Tid (\mbox{\cf \small \textit{tid1}}, \mbox{\cf \small \textit{tid2}})           } 
compares the two thread IDs and returns their order in the total 	  ordering of thread IDs. 	  The precise semantics of this ordering is left unspecified, other 	  than to say it is a total order.     \end{speccomment}
\item {\index{hashTid@hashTid!CML@\textcf{CML}}}{\kw{val}} {\cf hashTid: \(\mbox{\cf{}thread\_id}\rightarrow \mbox{\cf{}word}\)}\label{val-CML.hashTid}


\begin{speccomment}
\item {\cf \small hash\-Tid \mbox{\cf \small \textit{tid}}           } 
returns a hashing of the thread ID \mbox{\cf \small \textit{tid}}.     \end{speccomment}
\item {\index{tidToString@tidToString!CML@\textcf{CML}}}{\kw{val}} {\cf tidToString: \(\mbox{\cf{}thread\_id}\rightarrow \mbox{\cf{}string}\)}\label{val-CML.tidToString}


\begin{speccomment}
\item {\cf \small tid\-To\-String \mbox{\cf \small \textit{tid}}           } 
returns a string representation of the thread ID \mbox{\cf \small \textit{tid}}.     \end{speccomment}
\item {\index{joinEvt@joinEvt!CML@\textcf{CML}}}{\kw{val}} {\cf joinEvt: \(\mbox{\cf{}thread\_id}\rightarrow \mbox{\cf{}unit}\;\mbox{\cf{}event}\)}\label{val-CML.joinEvt}


\begin{speccomment}
\item {\cf \small join\-Evt \mbox{\cf \small \textit{tid}}           } 
creates an event value for synchronizing on the termination of 	  the thread with the ID \mbox{\cf \small \textit{tid}}. 	  There are three ways that a thread may terminate: the function that 	  was passed to {\cf \small spawn} may return; it may call the {\cf \small exit} 	  function, or it may have an uncaught exception. 	  Note that {\cf \small join\-Evt} does not distinguish between these 	  cases; it also does not become enabled if the named thread deadlocks 	  (even if it is garbage collected).     \end{speccomment}
\item {\index{channel@channel!CML@\textcf{CML}}}{\kw{val}} {\cf channel: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}chan}\)}\label{val-CML.channel}


\begin{speccomment}
\item {\cf \small channel ()           } 
creates a new synchronous channel.     \end{speccomment}
\item {\index{sameChannel@sameChannel!CML@\textcf{CML}}}{\kw{val}} {\cf sameChannel: \((\alpha\mtoksep{}\mbox{\cf{}chan}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}chan})\rightarrow \mbox{\cf{}bool}\)}\label{val-CML.sameChannel}


\begin{speccomment}
\item {\cf \small same\-Channel (\mbox{\cf \small \textit{ch1}}, \mbox{\cf \small \textit{ch2}})           } 
returns true, if the two channels are the same channel.     \end{speccomment}
\item {\index{send@send!CML@\textcf{CML}}}{\kw{val}} {\cf send: \((\alpha\mtoksep{}\mbox{\cf{}chan}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}\label{val-CML.send}


\begin{speccomment}
\item {\cf \small send (\mbox{\cf \small \textit{ch}}, \mbox{\cf \small \textit{a}})           } 
sends the message \mbox{\cf \small \textit{a}} on the synchronous channel \mbox{\cf \small \textit{ch}}. 	  This operation blocks the calling thread until there is another 	  thread attempting a {\cf \small recv} operation on the channel \mbox{\cf \small \textit{ch}}.     \end{speccomment}
\item {\index{recv@recv!CML@\textcf{CML}}}{\kw{val}} {\cf recv: \(\alpha\mtoksep{}\mbox{\cf{}chan}\rightarrow \alpha\)}\label{val-CML.recv}


\begin{speccomment}
\item {\cf \small recv \mbox{\cf \small \textit{ch}}           } 
receives a message from the channel \mbox{\cf \small \textit{ch}}. 	  This operation blocks the calling thread until there is another 	  thread attempting a {\cf \small send} operation on the channel \mbox{\cf \small \textit{ch}}.     \end{speccomment}
\item {\index{sendEvt@sendEvt!CML@\textcf{CML}}}{\kw{val}} {\cf sendEvt: \((\alpha\mtoksep{}\mbox{\cf{}chan}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\;\mbox{\cf{}event}\)}\label{val-CML.sendEvt}

\item {\index{recvEvt@recvEvt!CML@\textcf{CML}}}{\kw{val}} {\cf recvEvt: \(\alpha\mtoksep{}\mbox{\cf{}chan}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.recvEvt}


\begin{speccomment}
\item 

	  These functions create event values to represent the {\cf \small send} 	  and {\cf \small recv} operations.     \end{speccomment}
\item {\index{sendPoll@sendPoll!CML@\textcf{CML}}}{\kw{val}} {\cf sendPoll: \((\alpha\mtoksep{}\mbox{\cf{}chan}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}bool}\)}\label{val-CML.sendPoll}


\begin{speccomment}
\item {\cf \small send (\mbox{\cf \small \textit{ch}}, \mbox{\cf \small \textit{a}})           } 
attempts to send the message \mbox{\cf \small \textit{a}} on the synchronous channel \mbox{\cf \small \textit{ch}}. 	  If this operation can complete without blocking the calling thread, then 	  the message is sent and {\cf \small true} is returned. 	  Otherwise, no communication is preformed and {\cf \small false} is returned. 	  This function is not recommended for general use; it is provided 	  as an efficiency aid for certain kinds of protocols.     \end{speccomment}
\item {\index{recvPoll@recvPoll!CML@\textcf{CML}}}{\kw{val}} {\cf recvPoll: \(\alpha\mtoksep{}\mbox{\cf{}chan}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}\label{val-CML.recvPoll}


\begin{speccomment}
\item {\cf \small recv\-Poll \mbox{\cf \small \textit{ch}}           } 
attempts to receive a message from the channel \mbox{\cf \small \textit{ch}}. 	  If there is no other thread offering to {\cf \small send} a message 	  on \mbox{\cf \small \textit{ch}}, then this returns 	  {\cf \small NONE}, otherwise it 	  returns {\cf \small SOME} wrapped 	  around the message. 	  This function is not recommended for general use; it is provided 	  as an efficiency aid for certain kinds of protocols.     \end{speccomment}
\item {\index{wrap@wrap!CML@\textcf{CML}}}{\kw{val}} {\cf wrap: \((\alpha\mtoksep{}\mbox{\cf{}event}\mtoksep{}\verb,*,(\alpha\rightarrow \beta))\rightarrow \beta\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.wrap}


\begin{speccomment}
\item {\cf \small wrap (\mbox{\cf \small \textit{ev}}, \mbox{\cf \small \textit{f}})           } 
wraps the post-synchronization action \mbox{\cf \small \textit{f}} around the event 	  value \mbox{\cf \small \textit{ev}}.     \end{speccomment}
\item {\index{wrapHandler@wrapHandler!CML@\textcf{CML}}}{\kw{val}} {\cf wrapHandler: \((\alpha\mtoksep{}\mbox{\cf{}event}\mtoksep{}\verb,*,(\mbox{\cf{}exn}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}))\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.wrapHandler}


\begin{speccomment}
\item {\cf \small wrap\-Handler (\mbox{\cf \small \textit{ev}}, \mbox{\cf \small \textit{f}})           } 
wraps the exception handler function \mbox{\cf \small \textit{f}} around the event 	  value \mbox{\cf \small \textit{ev}}. 	  If, during execution of some post-synchronization action in 	  \mbox{\cf \small \textit{ev}}, an exception is raised, it will be caught and passed 	  to \mbox{\cf \small \textit{f}}. 	  Nesting of handlers works as would be expected: the innermost 	  handler is the one invoked. 	  Note that exceptions raised in the pre-synchronization actions in 	  \mbox{\cf \small \textit{ev}} (i.\-e., actions defined by {\cf \small guard} and {\cf \small with\-Nack}) 	  are not handled by \mbox{\cf \small \textit{f}}.     \end{speccomment}
\item {\index{guard@guard!CML@\textcf{CML}}}{\kw{val}} {\cf guard: \((\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event})\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.guard}


\begin{speccomment}
\item {\cf \small guard \mbox{\cf \small \textit{f}}           } 
creates \textit{delayed} event value from the function \mbox{\cf \small \textit{f}}. 	  When the resulting event value is synchronized on, the function 	  \mbox{\cf \small \textit{f}} will be evaluated and the resulting event value will be 	  used in its place in the synchronization. 	  This provides a mechanism for implementing pre-synchronization 	  actions, such as sending a request to a server.     \end{speccomment}
\item {\index{withNack@withNack!CML@\textcf{CML}}}{\kw{val}} {\cf withNack: \((\mbox{\cf{}unit}\;\mbox{\cf{}event}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event})\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.withNack}


\begin{speccomment}
\item {\cf \small with\-Nack \mbox{\cf \small \textit{f}}           } 
creates \textit{delayed} event value from the function \mbox{\cf \small \textit{f}}. 	  As in the case of {\cf \small guard}, the function \mbox{\cf \small \textit{f}} will be evaluated 	  at synchronization time and the resulting event value will be 	  used in its place in the synchronization. 	  Furthermore, when \mbox{\cf \small \textit{f}} is evaluated, it is passed a \textit{negative 	  acknowledgement} event as an argument. 	  If the event value that is returned from the evaluation of \mbox{\cf \small \textit{f}} 	  is \emph{not} chosen in the synchronization, then the negative 	  event will be enabled. 	  This provides a mechanism for informing servers that a client has 	  aborted a transaction.     \end{speccomment}
\item {\index{choose@choose!CML@\textcf{CML}}}{\kw{val}} {\cf choose: \(\alpha\mtoksep{}\mbox{\cf{}event}\;\mbox{\cf{}list}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.choose}


\begin{speccomment}
\item {\cf \small choose \mbox{\cf \small \textit{l}}           } 
constructs an event value that represents the non-deterministic 	  choice of the events in the list \mbox{\cf \small \textit{l}}.     \end{speccomment}
\item {\index{sync@sync!CML@\textcf{CML}}}{\kw{val}} {\cf sync: \(\alpha\mtoksep{}\mbox{\cf{}event}\rightarrow \alpha\)}\label{val-CML.sync}


\begin{speccomment}
\item {\cf \small sync \mbox{\cf \small \textit{ev}}           } 
synchronizes the calling thread on the event \mbox{\cf \small \textit{ev}}.     \end{speccomment}
\item {\index{select@select!CML@\textcf{CML}}}{\kw{val}} {\cf select: \(\alpha\mtoksep{}\mbox{\cf{}event}\;\mbox{\cf{}list}\rightarrow \alpha\)}\label{val-CML.select}


\begin{speccomment}
\item {\cf \small select \mbox{\cf \small \textit{evs}}           } 
synchronizes on the choice of a list of event values. 	  This is semantically equivalant to: 	  
\begin{code}
	    sync (choose \mbox{\cf \small \textit{evs}})
	  
\end{code}
 	  but is more efficient.     \end{speccomment}
\item {\index{never@never!CML@\textcf{CML}}}{\kw{val}} {\cf never: \(\alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.never}


\begin{speccomment}
\item {\cf \small never           } 
is an event value that is never enabled for synchronization. 	  It is semantically equivalant to the expression: 	  
\begin{code}
	    choose []
	  
\end{code}
     \end{speccomment}
\item {\index{alwaysEvt@alwaysEvt!CML@\textcf{CML}}}{\kw{val}} {\cf alwaysEvt: \(\alpha\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-CML.alwaysEvt}


\begin{speccomment}
\item {\cf \small always\-Evt \mbox{\cf \small \textit{a}}           } 
creates an event value that is always enabled, and that returns 	  the value \mbox{\cf \small \textit{a}} upon synchronization.     \end{speccomment}
\item {\index{timeOutEvt@timeOutEvt!CML@\textcf{CML}}}{\kw{val}} {\cf timeOutEvt: \(\mbox{\cf{}Time}.\mbox{\cf{}time}\rightarrow \mbox{\cf{}unit}\;\mbox{\cf{}event}\)}\label{val-CML.timeOutEvt}


\begin{speccomment}
\item {\cf \small time\-Out\-Evt \mbox{\cf \small \textit{t}}           } 
creates an event value that becomes enabled at the time 	  interval \mbox{\cf \small \textit{t}} after synchronization. 	  For example, the expression: 	  
\begin{code}
	    sync (time\-Out\-Evt (Time.fromSeconds 1))
	  
\end{code}
 	  will delay the calling thread for one second. 	  Note that the specified time interval is actually a minimum 	  waiting time, and the delay may be longer.     \end{speccomment}
\item {\index{atTimeEvt@atTimeEvt!CML@\textcf{CML}}}{\kw{val}} {\cf atTimeEvt: \(\mbox{\cf{}Time}.\mbox{\cf{}time}\rightarrow \mbox{\cf{}unit}\;\mbox{\cf{}event}\)}\label{val-CML.atTimeEvt}


\begin{speccomment}
\item {\cf \small at\-Time\-Evt \mbox{\cf \small \textit{t}}           } 
creates an event value that becomes enabled at the specified time 	  \mbox{\cf \small \textit{t}}. 	  For example, the expression: 	  
\begin{code}
	    sync (at\-Time\-Evt (Date.toTime (Date.date {\tt\{}
		year = 2000, month = Date.Jan, day = 0,
		hour = 0, minute = 0, second = 0, 
		offset = NONE
	      {\tt\}})))
	  
\end{code}
 	  blocks the calling thread until the beginning of the year 2000.     \end{speccomment}
\end{descr}

\begin{seealso}
{\cf Option}, {\cf Time}
\end{seealso}