Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /sml/trunk/src/cml/doc/Hardcopy/sync-var.tex
ViewVC logotype

Diff of /sml/trunk/src/cml/doc/Hardcopy/sync-var.tex

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 843, Tue Jun 19 21:53:04 2001 UTC revision 844, Wed Jun 20 20:39:15 2001 UTC
# Line 1  Line 1 
1  \section{The {\tt Sync\-Var} structure}  \maybeclearpage
2    \section{The {\cf Sync\-Var} structure}
3    
4    
5  The \texttt{Sync\-Var} 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 \texttt{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.\-  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.
6  \begin{synopsis}  \begin{synopsis}
7  \item {\textbf{signature}} SYNC\_\linebreak[0]VAR\label{sig-SYNC_VAR}  \item {\kw{signature}} \textcf{SYNC\_\linebreak[0]VAR}\label{sig-SYNC_VAR}
8  \item {\STRUCTURE} SyncVar: SYNC\_\linebreak[0]VAR\label{str-SyncVar}  \item {\STRUCTURE} \textcf{SyncVar: SYNC\_\linebreak[0]VAR}\label{str-SyncVar}
9  \end{synopsis}  \end{synopsis}
10    
11  \begin{interface}  \begin{interface}
12  \item {\index{Put@Put!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{exception}} Put  \Nopagebreak
13    \item {\index{Put@Put!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{exception}} \textcf{Put}
14    
15  \item {\index{ivar@ivar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{type}} \(\alpha\)~ivar  \Nopagebreak
16  \item {\index{iVar@iVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iVar: \(\mathrm{unit}\rightarrow \alpha\:\mathrm{ivar}\)}  \item {\index{ivar@ivar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{ivar}
17    \Nopagebreak
18    \item {\index{iVar@iVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}ivar}\)}
19    
20  \item {\index{iPut@iPut!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iPut: \((\alpha\:\mathrm{ivar}\:\verb,*,\:\alpha)\rightarrow \mathrm{unit}\)}  \Nopagebreak
21    \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}\)}
22    
23  \item {\index{iGet@iGet!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGet: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\)}  \Nopagebreak
24    \item {\index{iGet@iGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf iGet: \(\alpha\mtoksep{}\mbox{\cf{}ivar}\rightarrow \alpha\)}
25    
26  \item {\index{iGetEvt@iGetEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGetEvt: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\:\mathrm{event}\)}  \Nopagebreak
27    \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}\)}
28    
29  \item {\index{iGetPoll@iGetPoll!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGetPoll: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\:\mathrm{option}\)}  \Nopagebreak
30    \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}\)}
31    
32  \item {\index{sameIVar@sameIVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt sameIVar: \((\alpha\:\mathrm{ivar}\:\verb,*,\:\alpha\:\mathrm{ivar})\rightarrow \mathrm{bool}\)}  \Nopagebreak
33    \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}\)}
34    
35  \item {\index{mvar@mvar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{type}} \(\alpha\)~mvar  \Nopagebreak
36  \item {\index{mVar@mVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mVar: \(\mathrm{unit}\rightarrow \alpha\:\mathrm{mvar}\)}  \item {\index{mvar@mvar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{mvar}
37    \Nopagebreak
38    \item {\index{mVar@mVar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVar: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}
39    
40  \item {\index{mVarInit@mVarInit!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mVarInit: \(\alpha\rightarrow \alpha\:\mathrm{mvar}\)}  \Nopagebreak
41    \item {\index{mVarInit@mVarInit!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mVarInit: \(\alpha\rightarrow \alpha\mtoksep{}\mbox{\cf{}mvar}\)}
42    
43  \item {\index{mPut@mPut!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mPut: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \mathrm{unit}\)}  \Nopagebreak
44    \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}\)}
45    
46  \item {\index{mTake@mTake!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mTake: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\)}  \Nopagebreak
47    \item {\index{mTake@mTake!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mTake: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}
48    
49  \item {\index{mTakeEvt@mTakeEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mTakeEvt: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{event}\)}  \Nopagebreak
50    \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}\)}
51    
52  \item {\index{mGet@mGet!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGet: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\)}  \Nopagebreak
53    \item {\index{mGet@mGet!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{val}} {\cf mGet: \(\alpha\mtoksep{}\mbox{\cf{}mvar}\rightarrow \alpha\)}
54    
55  \item {\index{mGetEvt@mGetEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGetEvt: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{event}\)}  \Nopagebreak
56    \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}\)}
57    
58  \item {\index{mTakePoll@mTakePoll!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mTakePoll: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{option}\)}  \Nopagebreak
59    \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}\)}
60    
61  \item {\index{mGetPoll@mGetPoll!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGetPoll: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{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}\)}
62    
63  \item {\index{mSwap@mSwap!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mSwap: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \alpha\)}  \Nopagebreak
64    \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\)}
65    
66  \item {\index{mSwapEvt@mSwapEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mSwapEvt: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \alpha\:\mathrm{event}\)}  \Nopagebreak
67    \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}\)}
68    
69  \item {\index{sameMVar@sameMVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt sameMVar: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha\:\mathrm{mvar})\rightarrow \mathrm{bool}\)}  \Nopagebreak
70    \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}\)}
71    
72  \end{interface}  \end{interface}
73    
74  \begin{descr}  \begin{descr}
75  \item {\index{Put@Put!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{exception}} Put\label{exn-SYNC_VAR.Put}  \item {\index{Put@Put!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{exception}} \textcf{Put}\label{exn-SYNC_VAR.Put}
76    
77    
78  \begin{speccomment}  \begin{speccomment}
79  \item  \item
80    
81          This exception is raised when an attempt is made to put a       value into a value that is already full (see \texttt{i\-Put} and        \texttt{m\-Put}).\-     \end{speccomment}          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}
82  \item {\index{ivar@ivar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{type}} \(\alpha\)~ivar\label{ty-SYNC_VAR.ivar}  \item {\index{ivar@ivar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{ivar}\label{ty-SYNC_VAR.ivar}
83    
84  \begin{speccomment}  \begin{speccomment}
85  \item  \item
86    
87          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}          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}
88  \item {\index{iVar@iVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iVar: \(\mathrm{unit}\rightarrow \alpha\:\mathrm{ivar}\)}\label{val-SYNC_VAR.iVar}  \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}
89    
90    
91  \begin{speccomment}  \begin{speccomment}
92  \item {\tt i\-Var ()           }  \item {\cf \small i\-Var ()           }
93  creates a new empty I-variable.\-     \end{speccomment}  creates a new empty I-variable.     \end{speccomment}
94  \item {\index{iPut@iPut!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iPut: \((\alpha\:\mathrm{ivar}\:\verb,*,\:\alpha)\rightarrow \mathrm{unit}\)}\label{val-SYNC_VAR.iPut}\hfill\textbf{raises}~\texttt{Put}  \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}}
95    
96    
97  \begin{speccomment}  \begin{speccomment}
98  \item {\tt i\-Put (\textit{iv}, \textit{x})           }  \item {\cf \small i\-Put (\mbox{\cf \small \textit{iv}}, \mbox{\cf \small \textit{x}})           }
99  fills the I-variable \textit{iv} with the value \textit{x}.\-     Any threads that are blocked on \textit{iv} will be resumed.\-          If \textit{iv} already has a value in it, then the \texttt{Put}         exception is raised.\-     \end{speccomment}  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}
100  \item {\index{iGet@iGet!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGet: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\)}\label{val-SYNC_VAR.iGet}  \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}
101    
102    
103  \begin{speccomment}  \begin{speccomment}
104  \item {\tt i\-Get \textit{iv}           }  \item {\cf \small i\-Get \mbox{\cf \small \textit{iv}}           }
105  returns the contents of the I-variable \textit{iv}.\-     If the variable is empty, then the calling thread blocks until          the variable becomes full.\-     \end{speccomment}  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}
106  \item {\index{iGetEvt@iGetEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGetEvt: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\:\mathrm{event}\)}\label{val-SYNC_VAR.iGetEvt}  \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}
107    
108    
109  \begin{speccomment}  \begin{speccomment}
110  \item {\tt i\-Get\-Evt \textit{iv}           }  \item {\cf \small i\-Get\-Evt \mbox{\cf \small \textit{iv}}           }
111  returns an event-value that represents the \texttt{i\-Get}        operation on \textit{iv}.\-     \end{speccomment}  returns an event-value that represents the {\cf \small i\-Get}    operation on \mbox{\cf \small \textit{iv}}.     \end{speccomment}
112  \item {\index{iGetPoll@iGetPoll!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt iGetPoll: \(\alpha\:\mathrm{ivar}\rightarrow \alpha\:\mathrm{option}\)}\label{val-SYNC_VAR.iGetPoll}  \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}
113    
114    
115  \begin{speccomment}  \begin{speccomment}
116  \item  \item
117    
118            This is a non-blocking version of \texttt{i\-Get}.\-    If the corresponding blocking form would block, then it returns         \texttt{NONE}; otherwise        it returns \texttt{SOME}        of the variable's contents.\-     \end{speccomment}            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}
119  \item {\index{sameIVar@sameIVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt sameIVar: \((\alpha\:\mathrm{ivar}\:\verb,*,\:\alpha\:\mathrm{ivar})\rightarrow \mathrm{bool}\)}\label{val-SYNC_VAR.sameIVar}  \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}
120    
121    
122  \begin{speccomment}  \begin{speccomment}
123  \item {\tt same\-IVar (\textit{iv1}, \textit{iv2})           }  \item {\cf \small same\-IVar (\mbox{\cf \small \textit{iv1}}, \mbox{\cf \small \textit{iv2}})           }
124  returns {\tt true}, if the \textit{iv1} and \textit{iv2} are the          same I-variable.\-     \end{speccomment}  returns {\cf \small true}, if the \mbox{\cf \small \textit{iv1}} and \mbox{\cf \small \textit{iv2}} are the       same I-variable.     \end{speccomment}
125  \item {\index{mvar@mvar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{type}} \(\alpha\)~mvar\label{ty-SYNC_VAR.mvar}  \item {\index{mvar@mvar!SYNC_VAR@\textcf{SYNC\_\linebreak[0]VAR}}}{\kw{type}} \(\alpha\)~\textcf{mvar}\label{ty-SYNC_VAR.mvar}
126    
127  \begin{speccomment}  \begin{speccomment}
128  \item  \item
129    
130          This is the type constructor for M-structured variables.\-      Unlike \texttt{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}          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}
131  \item {\index{mVar@mVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mVar: \(\mathrm{unit}\rightarrow \alpha\:\mathrm{mvar}\)}\label{val-SYNC_VAR.mVar}  \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}
132    
133    
134  \begin{speccomment}  \begin{speccomment}
135  \item {\tt m\-Var ()           }  \item {\cf \small m\-Var ()           }
136  creates a new empty M-variable.\-     \end{speccomment}  creates a new empty M-variable.     \end{speccomment}
137  \item {\index{mVarInit@mVarInit!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mVarInit: \(\alpha\rightarrow \alpha\:\mathrm{mvar}\)}\label{val-SYNC_VAR.mVarInit}  \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}
138    
139    
140  \begin{speccomment}  \begin{speccomment}
141  \item {\tt m\-Var x           }  \item {\cf \small m\-Var x           }
142  creates a new M-variable initialized to \textit{x}.\-     \end{speccomment}  creates a new M-variable initialized to \mbox{\cf \small \textit{x}}.     \end{speccomment}
143  \item {\index{mPut@mPut!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mPut: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \mathrm{unit}\)}\label{val-SYNC_VAR.mPut}\hfill\textbf{raises}~\texttt{Put}  \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}}
144    
145    
146  \begin{speccomment}  \begin{speccomment}
147  \item {\tt m\-Put (\textit{mv}, \textit{x})           }  \item {\cf \small m\-Put (\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{x}})           }
148  fills the M-variable \textit{mv} with the value \textit{x}.\-     Any threads that are blocked on \textit{mv} will be resumed.\-          If \textit{mv} already has a value in it, then the \texttt{Put}         exception is raised.\-     \end{speccomment}  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}
149  \item {\index{mTake@mTake!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mTake: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\)}\label{val-SYNC_VAR.mTake}  \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}
150    
151    
152  \begin{speccomment}  \begin{speccomment}
153  \item {\tt m\-Take \textit{mv}         }  \item {\cf \small m\-Take \mbox{\cf \small \textit{mv}}         }
154  removes and returns the contents of the M-variable \textit{mv}  making it empty.\-      If the variable is already empty, then the calling thread       is blocked until a value is available.\-     \end{speccomment}  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}
155  \item {\index{mTakeEvt@mTakeEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mTakeEvt: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{event}\)}\label{val-SYNC_VAR.mTakeEvt}  \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}
156    
157    
158  \begin{speccomment}  \begin{speccomment}
159  \item {\tt m\-Take\-Evt \textit{mv}           }  \item {\cf \small m\-Take\-Evt \mbox{\cf \small \textit{mv}}           }
160  returns an event-value that represents the \texttt{m\-Take}       operation on \textit{mv}.\-     \end{speccomment}  returns an event-value that represents the {\cf \small m\-Take}           operation on \mbox{\cf \small \textit{mv}}.     \end{speccomment}
161  \item {\index{mGet@mGet!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGet: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\)}\label{val-SYNC_VAR.mGet}  \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}
162    
163    
164  \begin{speccomment}  \begin{speccomment}
165  \item {\tt m\-Get \textit{mv}           }  \item {\cf \small m\-Get \mbox{\cf \small \textit{mv}}           }
166  returns the contents of the M-variable \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:  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:
167  \begin{code}  \begin{code}
168  let val x = mTake \textit{mv} in mPut(\textit{mv}, x); x end  let val x = mTake \mbox{\cf \small \textit{mv}} in mPut(\mbox{\cf \small \textit{mv}}, x); x end
169    
170  \end{code}  \end{code}
171       \end{speccomment}       \end{speccomment}
172  \item {\index{mGetEvt@mGetEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGetEvt: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{event}\)}\label{val-SYNC_VAR.mGetEvt}  \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}
173    
174    
175  \begin{speccomment}  \begin{speccomment}
176  \item {\tt m\-Get\-Evt \textit{mv}           }  \item {\cf \small m\-Get\-Evt \mbox{\cf \small \textit{mv}}           }
177  returns an event-value that represents the \texttt{m\-Get}        operation on \textit{mv}.\-     \end{speccomment}  returns an event-value that represents the {\cf \small m\-Get}    operation on \mbox{\cf \small \textit{mv}}.     \end{speccomment}
178  \item {\index{mGetPoll@mGetPoll!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mGetPoll: \(\alpha\:\mathrm{mvar}\rightarrow \alpha\:\mathrm{option}\)}\label{val-SYNC_VAR.mGetPoll}  \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}
179    
180    \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}
181    
182    
183  \begin{speccomment}  \begin{speccomment}
184  \item  \item
185    
186            These are non-blocking versions of \texttt{m\-Take} and         \texttt{m\-Get} (respectively).\-       If the corresponding blocking form would block, then they return        \texttt{NONE}; otherwise        they return \texttt{SOME}       of the variable's contents.\-     \end{speccomment}            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}
187  \item {\index{mSwap@mSwap!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mSwap: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \alpha\)}\label{val-SYNC_VAR.mSwap}  \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}
188    
189    
190  \begin{speccomment}  \begin{speccomment}
191  \item {\tt m\-Swap (\textit{mv}, \textit{new\-V})           }  \item {\cf \small m\-Swap (\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{new\-V}})           }
192  puts the value \textit{new\-V} into the M-variable \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:  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:
193  \begin{code}  \begin{code}
194  let val x = mTake \textit{mv} in mPut(\textit{mv}, \textit{new\-V}); x end  let val x = mTake \mbox{\cf \small \textit{mv}} in mPut(\mbox{\cf \small \textit{mv}}, \mbox{\cf \small \textit{new\-V}}); x end
195    
196  \end{code}  \end{code}
197            except that {\tt m\-Swap} is executed atomically.\-     \end{speccomment}            except that {\cf \small m\-Swap} is executed atomically.     \end{speccomment}
198  \item {\index{mSwapEvt@mSwapEvt!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt mSwapEvt: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha)\rightarrow \alpha\:\mathrm{event}\)}\label{val-SYNC_VAR.mSwapEvt}  \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}
199    
200    
201  \begin{speccomment}  \begin{speccomment}
202  \item {\tt m\-Swap\-Evt \textit{mv}           }  \item {\cf \small m\-Swap\-Evt \mbox{\cf \small \textit{mv}}           }
203  returns an event-value that represents the \texttt{m\-Swap}       operation on \textit{mv} and \textit{new\-V}.\-     \end{speccomment}  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}
204  \item {\index{sameMVar@sameMVar!SYNC_VAR@SYNC\_\linebreak[0]VAR}}{\textbf{val}} {\tt sameMVar: \((\alpha\:\mathrm{mvar}\:\verb,*,\:\alpha\:\mathrm{mvar})\rightarrow \mathrm{bool}\)}\label{val-SYNC_VAR.sameMVar}  \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}
205    
206    
207  \begin{speccomment}  \begin{speccomment}
208  \item {\tt same\-MVar (\textit{mv1}, \textit{mv2})           }  \item {\cf \small same\-MVar (\mbox{\cf \small \textit{mv1}}, \mbox{\cf \small \textit{mv2}})           }
209  returns {\tt true}, if \textit{mv1} and \textit{mv2} are the same         M-variable.\-   \end{speccomment}  returns {\cf \small true}, if \mbox{\cf \small \textit{mv1}} and \mbox{\cf \small \textit{mv2}} are the same      M-variable.   \end{speccomment}
210  \end{descr}  \end{descr}
211    
212    
213  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.\-  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.
214    
215  A disciplined use of M-variables can provide an atomic read-modify-write operation.\-  A disciplined use of M-variables can provide an atomic read-modify-write operation.
216  \begin{seealso}  \begin{seealso}
217  \texttt{CML}  {\cf CML} (\pageref{str-CML})
218  \end{seealso}  \end{seealso}

Legend:
Removed from v.843  
changed lines
  Added in v.844

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0