Skip to content

Commit 42279d5

Browse files
author
Aslan Askarov
committed
Improvements thanks to Musard
1 parent 5660dfe commit 42279d5

File tree

2 files changed

+130
-68
lines changed

2 files changed

+130
-68
lines changed

body.tex

Lines changed: 129 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,9 @@ \subsection{A minimal \troupelang\ program}
5555

5656
\subsection{Overview of the basic language}
5757
At the very core of \troupelang\ is a dynamically typed functional programming language without mutable references.
58-
For example, a Fibonacci function in \troupelang\ is written exactly as in SML sans type annotations.
58+
For example, a Fibonacci function in \troupelang\ is written exactly as in SML sans type annotations.
5959
\begin{lstlisting}
60+
(* basic_fib.trp *)
6061
let fun fib x =
6162
if x > 2 then fib (x - 1) + fib (x - 2)
6263
else 1
@@ -139,6 +140,7 @@ \subsubsection{Function declarations}
139140
Functions are declared using \textcode{let fun} syntax. Mutually recursive functions
140141
are delimited using the \textcode{and} keyword.
141142
\begin{lstlisting}
143+
(* basic_evenodd.trp *)
142144
let fun even x = if x = 0 then true else odd (x - 1)
143145
and odd x = if x = 0 then false else even (x - 1)
144146
in even 7
@@ -161,6 +163,7 @@ \subsection{Libraries}
161163
Troupe has a minimal support for built-in libraries. Current libraries include a library \code{lists} for common list manipulations, library \code{declassifyutil} for declassification of aggregate data structures, and library
162164
\code{stdio} with convenient wrappers for standard input and output. To use a library, one needs to import it with an \code{import} statement at the top of the program.
163165
\begin{lstlisting}
166+
(* basic_lib.trp *)
164167
import lists
165168
printWithLabels (map ( fn i => i + 1) [1,2,3])
166169
\end{lstlisting}
@@ -174,6 +177,7 @@ \subsubsection{Spawning processes}
174177
It return the process identifier of the new process, and starts the new process that from now on runs concurrently with the
175178
parent process.
176179
\begin{lstlisting}
180+
(* basic_spawn.trp *)
177181
import lists
178182
let fun printwait x = let val _ = printWithLabels x in sleep 10 end
179183
fun foo () = map printwait [1,2,3]
@@ -205,6 +209,7 @@ \subsubsection{Sending and receiving messages}
205209

206210

207211
\begin{lstlisting}
212+
(* basic_receive.trp *)
208213
let fun foo () =
209214
receive [hn x => printWithLabels ("foo received", x)]
210215
val p = spawn foo
@@ -248,6 +253,7 @@ \subsubsection{Example: receive with a timeout}
248253
The use of the unique string avoids creating a confusion when multiple
249254
timeouts may be involved.
250255
\begin{lstlisting}
256+
(* basic_timeout.trp *)
251257
let fun timeout p r t = let val _ = sleep t
252258
in send (p, r)
253259
end
@@ -266,6 +272,8 @@ \subsubsection{Example: updateable service}
266272
messages with the \textcode{"UPDATE"} string.
267273

268274
\begin{lstlisting}
275+
(* basic_updateableserver.trp *)
276+
import timeout
269277
let fun v_one n =
270278
receive [ hn ("REQUEST", senderid) =>
271279
let val _ = send (senderid, n)
@@ -293,14 +301,16 @@ \subsubsection{Example: updateable service}
293301
val _ = send (service, ("UPDATE", v_two))
294302
val _ = send (service, ("COMPUTE", self(), fn x => x * x, 42))
295303
val _ = receive [ hn x => print x]
296-
in ()
304+
in exitAfterTimeout authority 1000 0
305+
"force terminating the server example after 1s"
297306
end
298307
\end{lstlisting}
299308
The evaluation of this program results in the output
300309
\begin{verbatim}
301310
0@{}%{}
302311
1764@{}%{}
303312
main thread finished with value: ()@{}%{}
313+
force terminating the server example after 1s
304314
\end{verbatim}
305315

306316
\subsection{Debugging concurrent programs}
@@ -359,6 +369,7 @@ \subsection{Monitoring for information flow}
359369
\paragraph{Explicit flows}
360370
The following example shows how to create labeled values and how explicit dependencies are propagated.
361371
\begin{lstlisting}
372+
(* ifc_explicit.trp *)
362373
let val x = 10 raisedTo {alice}
363374
val y = 20 raisedTo {bob}
364375
in x + y
@@ -382,6 +393,7 @@ \subsection{Monitoring for information flow}
382393
Labels in \troupelang\ are first-class:
383394

384395
\begin{lstlisting}
396+
(* ifc_labels.trp *)
385397
import lists
386398
map (fn (x,lev) => x raisedTo lev) [ (1, {alice})
387399
, (2, {bob})
@@ -396,6 +408,7 @@ \subsection{Monitoring for information flow}
396408

397409

398410
\begin{lstlisting}
411+
(* ifc_implicit1.trp *)
399412
let val x = 10 raisedTo {alice}
400413
in if x > 5 then 1 else 0
401414
end
@@ -407,6 +420,10 @@ \subsection{Monitoring for information flow}
407420
branch that has been chosen here. Because, of the dynamic nature of type checking,
408421
we also carry the information about the chosen branch into the type label.
409422

423+
424+
425+
426+
410427
\paragraph{Implicit flows and I/O}
411428
The implicit information flows are further propagated between processes.
412429
In the mailbox, each message is additionally tagged with a label that
@@ -416,6 +433,7 @@ \subsection{Monitoring for information flow}
416433
where the pc-tag set to the provided label argument.
417434

418435
\begin{lstlisting}
436+
(* ifc_implicit2.trp *)
419437
let val x = 10 raisedTo {secret}
420438
val p = self()
421439
val _ = spawn ( fn () => if x > 0
@@ -438,6 +456,7 @@ \subsection{Monitoring for information flow}
438456
$\mathit{pc}~\sqsubseteq~\mathit{block}$. To view the labels there is a
439457
helper internal function \code{debugpc ()}.
440458
\begin{lstlisting}
459+
(* ifc_debugpc.trp *)
441460
let val x = 1 raisedTo{secret}
442461
val _ = debugpc()
443462
val x = if x > 2 then receive [] else ()
@@ -494,6 +513,7 @@ \subsubsection{Attenuation}
494513
Authority can be attenuated using the \code{attenuate} primitive.
495514

496515
\begin{lstlisting}
516+
(* ifc_attenuate.trp *)
497517
attenuate (authority, {alice})
498518
\end{lstlisting}
499519
\begin{verbatim}
@@ -505,13 +525,15 @@ \subsubsection{Basic declassification}
505525
the expression to declassify, the authority, and the target label. For example, a basic declassification
506526
looks like this.
507527
\begin{lstlisting}
528+
(* ifc_declassify_atten.trp *)
508529
let val x = 10 raisedTo {alice}
509530
in declassify (x , authority, {} )
510531
end
511532
\end{lstlisting}
512533

513534
When authority for declassification is not sufficient, Troupe returns an error message.
514535
\begin{lstlisting}
536+
(* ifc_declassify_err.trp *)
515537
let val authAlice = attenuate (authority, {alice})
516538
val x = 1 raisedTo {bob}
517539
in declassify (x, authAlice, {})
@@ -537,6 +559,7 @@ \subsubsection{Declassification of the blocking level}
537559
levels.
538560

539561
\begin{lstlisting}
562+
(* ifc_pini.trp *)
540563
let val x = 10 raisedTo {alice}
541564
val y = 0
542565
val z =
@@ -660,7 +683,6 @@ \subsubsection{Registering and looking up processes}
660683
the node identity and the name at which a process is bound, we can find the process at that node, using the
661684
\code{whereis} primitive:
662685

663-
664686
\begin{lstlisting}
665687
let val echo =
666688
whereis ( "QmNRwNZACPciLS14cZFApwrCcAdbRAXYgztea9m5XwRe4z"
@@ -670,6 +692,10 @@ \subsubsection{Registering and looking up processes}
670692
end
671693
\end{lstlisting}
672694

695+
The complete echo example -- including the code above and
696+
the scripts for generating the identifiers is available at
697+
\code{\$TROUPE/examples/network/echo}.
698+
673699
\subsubsection{Aliases}
674700
Aliases is a mechanism that allows us to avoid having hardcoded node identifiers in the source code.
675701
The alias mechanism operates in the way of the traditional Unix hosts files.
@@ -771,6 +797,24 @@ \subsubsection{\code{declassify}}
771797
\end{description}
772798

773799

800+
\subsubsection{\code{exit}}
801+
\begin{description}
802+
\item [Description] Exits the Troupe runtime.
803+
\item [Arguments] A tuple \code{(authority, exitCode)}.
804+
\item [Returns] Nothing
805+
\item [Example usage] \textcode{exit(authority, 0)}
806+
\end{description}
807+
808+
809+
\subsubsection{\code{getTime}}
810+
\begin{description}
811+
\item [Description] Obtains current Unix timestmap
812+
\item [Arguments] Unit.
813+
\item [Returns] Number.
814+
\item [Example usage] \textcode{getTime()}
815+
\end{description}
816+
817+
774818
\subsubsection{\code{getTime}}
775819
\begin{description}
776820
\item [Description] Obtains current Unix timestmap
@@ -780,6 +824,20 @@ \subsubsection{\code{getTime}}
780824
\end{description}
781825

782826

827+
\subsubsection{\code{inputLine}}
828+
\begin{description}
829+
\item[Description] Reads a line from the console.
830+
\item[Arguments] Unit.
831+
\item[Returns] String value.
832+
\item[Blocking behavior] Synchronous. Observe that the blocking label
833+
is raised to top after this operation, because the user providing the
834+
input is assumed to operate at level top. To prevent this from happening,
835+
the blocking label can be declassified using the \code{let\ pini} constructs.
836+
See also library functions \code{inputLineWithPini} and \code{inputLineWithPini}
837+
from \code{stdio} library.
838+
\end{description}
839+
840+
783841
\subsubsection{\code{lowermbox}}
784842
\begin{description}
785843
\item [Description] Lowers the clearance of the current process' mailbox.
@@ -797,6 +855,17 @@ \subsubsection{\code{mkuuid}}
797855
\item [Example usage] \textcode{print (mkuuid\ ())}
798856
\end{description}
799857

858+
859+
\subsubsection{\code{node}}
860+
\begin{description}
861+
\item [Description] Returns node identifier of a process.
862+
\item [Arguments] Process identifier.
863+
\item [Returns] String containing a node identifier.
864+
\end{description}
865+
866+
867+
868+
800869
\subsubsection{\code{pinipop}}
801870
\begin{description}
802871
\item [Description] Pop an authority value from the \emph{pini} stack, and declassify the current blocking level.
@@ -832,6 +901,30 @@ \subsubsection{\code{printWithLabels}}
832901
\item [Example usage] \code{printWithLabels\ "Hello, world"}
833902
\end{description}
834903

904+
905+
\subsubsection{\code{raiseTrust}}
906+
\begin{description}
907+
\item [Description] Dynamically raise the trust level of a node.
908+
\item [Arguments] A triple of a node identifier, root-level authority, and the intended trust level.
909+
\item [Returns] Unit.
910+
\item [Failure behavior]. Fails if the argument type is invalid. Fails if the authority argument is not top.
911+
Fails if the blocking level is not $\bot$.
912+
\item [Example usage] $\code{raiseTrust("@alicescomputer", authority, \{alice\})}$
913+
\end{description}
914+
Note that the top-level authority is required because this is a privileged operation with system-wide consequences.
915+
916+
917+
918+
919+
\subsubsection{\code{raisembox}}
920+
\begin{description}
921+
\item [Description] Raises the clearance of the current process' mailbox.
922+
\item [Arguments] A security level
923+
\item [Returns] A capability for lowering the mailbox level back to the previous value.
924+
\item [Failure behavior] Fails if the type of the argument is invalid (dynamic type checking).
925+
\end{description}
926+
927+
835928
\subsubsection{\code{random}}
836929
\begin{description}
837930
\item [Description] Generates a random number between 0 (inclusive) and 1.
@@ -842,6 +935,39 @@ \subsubsection{\code{random}}
842935

843936

844937

938+
939+
940+
\subsubsection{\code{receive}}
941+
\begin{description}
942+
\item [Description] Picks a message from the mailbox.
943+
\item [Arguments] A list of \emph{handler functions} (cf. Section~\ref{sec:handlers}).
944+
\item [Returns] The value returned by the body of the matching handler.
945+
\end{description}
946+
947+
\subsubsection{\code{register}}
948+
\begin{description}
949+
\item [Description] Registers the process under a name.
950+
\item [Arguments] A tuple of the form $(\mathit{str}, \mathit{pid}, \mathit{authority})$, where $\mathit{str}$ is the name under
951+
which the process is to be registered, $\mathit{pid}$ is the process identifier, and
952+
$\mathit{authority}$ is the top authority value.
953+
\item [Returns] Unit.
954+
\item [Blocking behavior] Synchronous.
955+
\item [Failure behavior] Crashes if the provided authority is not top, or if the blocking level is not $\bot$.
956+
\item [Example usage]\textcode{register ("auctionServer", self(), authority)}
957+
\end{description}
958+
959+
Note that this is a privileged operation with system-wide consequences.
960+
961+
962+
\subsubsection{\code{rcv}}
963+
\begin{description}
964+
\item [Description] Picks a message from the mailbox with pre-filtering the levels of the messages.
965+
\item [Arguments] A triple of the form $(\mathit{hs}, \ell_{\mathit{lo}}, \ell_{\mathit{hi}}) $ where $\mathit{hs}$ is the list of handlers, $\ell_{\mathit{lo}}$ is the lower bound on the \emph{sender-level} of the messages, and
966+
$\ell_{\mathit{hi}}$ is the upper bound on the \emph{sender-level} of the messages in the mailbox.
967+
\item [Returns] The value returned by the body of the matching handler.
968+
\end{description}
969+
970+
845971
\subsubsection{\code{sandbox}}
846972
\begin{description}
847973
\item [Description] Execute a function in a sandbox for a fixed duration of time.
@@ -919,70 +1045,6 @@ \subsubsection{\code{raisedTo}}
9191045
\item [Example usage] $\code{42\ raisedTo\ \{alice\}}$
9201046
\end{description}
9211047

922-
\subsubsection{\code{raiseTrust}}
923-
\begin{description}
924-
\item [Description] Dynamically raise the trust level of a node.
925-
\item [Arguments] A triple of a node identifier, root-level authority, and the intended trust level.
926-
\item [Returns] Unit.
927-
\item [Failure behavior]. Fails if the argument type is invalid. Fails if the authority argument is not top.
928-
Fails if the blocking level is not $\bot$.
929-
\item [Example usage] $\code{raiseTrust("@alicescomputer", authority, \{alice\})}$
930-
\end{description}
931-
Note that the top-level authority is required because this is a privileged operation with system-wide consequences.
932-
933-
934-
935-
936-
\subsubsection{\code{raisembox}}
937-
\begin{description}
938-
\item [Description] Raises the clearance of the current process' mailbox.
939-
\item [Arguments] A security level
940-
\item [Returns] A capability for lowering the mailbox level back to the previous value.
941-
\item [Failure behavior] Fails if the type of the argument is invalid (dynamic type checking).
942-
\end{description}
943-
944-
945-
946-
947-
\subsubsection{\code{readInput}}
948-
\begin{description}
949-
\item[Description] Reads a line from the console.
950-
\item[Arguments] Unit.
951-
\item[Returns] String value.
952-
\item[Blocking behavior] Synchronous.
953-
\end{description}
954-
955-
956-
957-
\subsubsection{\code{receive}}
958-
\begin{description}
959-
\item [Description] Picks a message from the mailbox.
960-
\item [Arguments] A list of \emph{handler functions} (cf. Section~\ref{sec:handlers}).
961-
\item [Returns] The value returned by the body of the matching handler.
962-
\end{description}
963-
964-
\subsubsection{\code{register}}
965-
\begin{description}
966-
\item [Description] Registers the process under a name.
967-
\item [Arguments] A tuple of the form $(\mathit{str}, \mathit{pid}, \mathit{authority})$, where $\mathit{str}$ is the name under
968-
which the process is to be registered, $\mathit{pid}$ is the process identifier, and
969-
$\mathit{authority}$ is the top authority value.
970-
\item [Returns] Unit.
971-
\item [Blocking behavior] Synchronous.
972-
\item [Failure behavior] Crashes if the provided authority is not top, or if the blocking level is not $\bot$.
973-
\item [Example usage]\textcode{register ("auctionServer", self(), authority)}
974-
\end{description}
975-
976-
Note that this is a privileged operation with system-wide consequences.
977-
978-
979-
\subsubsection{\code{rcv}}
980-
\begin{description}
981-
\item [Description] Picks a message from the mailbox with pre-filtering the levels of the messages.
982-
\item [Arguments] A triple of the form $(\mathit{hs}, \ell_{\mathit{lo}}, \ell_{\mathit{hi}}) $ where $\mathit{hs}$ is the list of handlers, $\ell_{\mathit{lo}}$ is the lower bound on the \emph{sender-level} of the messages, and
983-
$\ell_{\mathit{hi}}$ is the upper bound on the \emph{sender-level} of the messages in the mailbox.
984-
\item [Returns] The value returned by the body of the matching handler.
985-
\end{description}
9861048

9871049
\subsubsection{\code{whereis}}
9881050

main.tex

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@
3939
%\author{}
4040
% \author{\sf Aslan Askarov \\ \small aslan@cs.au.dk}
4141

42-
\date{March 4, 2020} % Activate to display a given date or no date
42+
\date{March 16, 2020} % Activate to display a given date or no date
4343

4444
\begin{document}
4545
\maketitle

0 commit comments

Comments
 (0)