25 \>\>\>end;\\ |
25 \>\>\>end;\\ |
26 \>(*gets 2nd element of touple*)\\ |
26 \>(*gets 2nd element of touple*)\\ |
27 \>fun fib n = fib' (n - 1) |> snd \textrm{,}} |
27 \>fun fib n = fib' (n - 1) |> snd \textrm{,}} |
28 \noindent |
28 \noindent |
29 shows linear runtime behavior. Annotations (section \ref{sec:annot}) were demonstrated using the Fibonacci function (page \pageref{alg:parannot}): |
29 shows linear runtime behavior. Annotations (section \ref{sec:annot}) were demonstrated using the Fibonacci function (page \pageref{alg:parannot}): |
30 \imlcode{~~\=fu\=n fib 0 = 1\\ |
30 \imlcode{~~\=fu\=n fib 0 = 0\\ |
31 \>\>| fib 1 = 1\\ |
31 \>\>| fib 1 = 1\\ |
32 \>\>| fib x = fib (x - 1) + par (fib (x - 2))} |
32 \>\>| fib x = fib (x - 1) + par (fib (x - 2))} |
33 \noindent |
33 \noindent |
34 In practice, the gain from parallelism in this example would not just be marginal, the overhead for managing parallel execution would most likely result in a performance worse than the sequential version. Note that annotations of this kind can only work in a programming language following a lazy evaluation strategy because in an eager language like \textit{Standard ML} the annotated expression would be evaluated before being passed to the hypothetical {\tt par} evaluation. |
34 In practice, the gain from parallelism in this example would not just be marginal, the overhead for managing parallel execution would most likely result in a performance worse than the sequential version. Note that annotations of this kind can only work in a programming language following a lazy evaluation strategy because in an eager language like \textit{Standard ML} the annotated expression would be evaluated before being passed to the hypothetical {\tt par} evaluation. |
35 Futures have been discussed in detail throughout this thesis (sections \ref{sec:futurespro}, \ref{sec:actors_scala}, \ref{sec:csp}, \ref{sec:isafut}). The example on page \pageref{alg:futures} redefined {\tt fib} with a future: |
35 Futures have been discussed in detail throughout this thesis (sections \ref{sec:futurespro}, \ref{sec:actors_scala}, \ref{sec:csp}, \ref{sec:isafut}). The example on page \pageref{alg:futures} redefined {\tt fib} with a future: |
36 \imlcode{\label{alg:fib-futures} |
36 \imlcode{\label{alg:fib-futures} |
37 ~~\=fu\=n \=fi\=b \=0 = 1\\ |
37 ~~\=fu\=n \=fi\=b \=0 = 0\\ |
38 \>\>| fib 1 = 1\\ |
38 \>\>| fib 1 = 1\\ |
39 \>\>| fib x = let\\ |
39 \>\>| fib x = let\\ |
40 \>\>\>\>\>fun fib' () = fib (x - 2)\\ |
40 \>\>\>\>\>fun fib' () = fib (x - 2)\\ |
41 \>\>\>\>\>val fibf = Future.fork fib'\\ |
41 \>\>\>\>\>val fibf = Future.fork fib'\\ |
42 \>\>\>\>in fib (x - 1) + (Future.join fibf) end} |
42 \>\>\>\>in fib (x - 1) + (Future.join fibf) end} |
43 This code does work in {\em Isabelle/ML} (section \ref{sec:isabelleml}). The performance concerns we saw with the previous example also apply here: in practice, parallelising the evaluation of the Fibonacci function in this way makes no sense. |
43 This code does work in {\em Isabelle/ML} (section \ref{sec:isabelleml}). The performance concerns we saw with the previous example also apply here: in practice, parallelizing the evaluation of the Fibonacci function in this way makes no sense. |
44 |
44 |
45 |
45 |
46 \section{{\tt merge\_lists} implementation} |
46 \section{{\tt merge\_lists} implementation} |
47 \label{app:merge-lists} |
47 \label{app:merge-lists} |
48 In the \texttt{Theory\_Data} implementation on page \pageref{alg:thydata-functor} (section \ref{ssec:parall-thy}) we omitted the definitions of the functions {\tt merge\_lists} and {\tt merge\_lists'} for simplicity reasons. They have been added here (program \ref{alg:merge-lists}). Please note that they require that their input lists of type {\tt int list} are already ordered. The difference is that {\tt merge\_lists} accepts the two lists in a touple and {\tt merge\_lists'} as two separate arguments. |
48 In the \texttt{Theory\_Data} implementation on page \pageref{alg:thydata-functor} (section \ref{ssec:parall-thy}) we omitted the definitions of the functions {\tt merge\_lists} and {\tt merge\_lists'} for simplicity reasons. They have been added here (program \ref{alg:merge-lists}). Please note that they require that their input lists of type {\tt int list} are already ordered. The difference is that {\tt merge\_lists} accepts the two lists in a touple and {\tt merge\_lists'} as two separate arguments. |