1.1 --- a/master/thesis/appendix_a.tex Thu Jun 26 02:58:44 2014 +0200
1.2 +++ b/master/thesis/appendix_a.tex Sun Jul 20 16:31:11 2014 +0200
1.3 @@ -27,20 +27,20 @@
1.4 \>fun fib n = fib' (n - 1) |> snd \textrm{,}}
1.5 \noindent
1.6 shows linear runtime behavior. Annotations (section \ref{sec:annot}) were demonstrated using the Fibonacci function (page \pageref{alg:parannot}):
1.7 -\imlcode{~~\=fu\=n fib 0 = 1\\
1.8 +\imlcode{~~\=fu\=n fib 0 = 0\\
1.9 \>\>| fib 1 = 1\\
1.10 \>\>| fib x = fib (x - 1) + par (fib (x - 2))}
1.11 \noindent
1.12 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.
1.13 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:
1.14 \imlcode{\label{alg:fib-futures}
1.15 -~~\=fu\=n \=fi\=b \=0 = 1\\
1.16 +~~\=fu\=n \=fi\=b \=0 = 0\\
1.17 \>\>| fib 1 = 1\\
1.18 \>\>| fib x = let\\
1.19 \>\>\>\>\>fun fib' () = fib (x - 2)\\
1.20 \>\>\>\>\>val fibf = Future.fork fib'\\
1.21 \>\>\>\>in fib (x - 1) + (Future.join fibf) end}
1.22 -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.
1.23 +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.
1.24
1.25
1.26 \section{{\tt merge\_lists} implementation}
2.1 --- a/master/thesis/conclusion.tex Thu Jun 26 02:58:44 2014 +0200
2.2 +++ b/master/thesis/conclusion.tex Sun Jul 20 16:31:11 2014 +0200
2.3 @@ -8,7 +8,7 @@
2.4 While \isac{}'s internal user session management has now been parallelized, multiple user GUIs communicate with the same standard input stream on the \textit{Standard ML} side and this communication is unsynchronized. The mathematic engine writes to one single standard output stream. The write operation in use is provided and synchronized by \isabelle. However, since all GUIs read from the same stream, they need to filter out all messages not meant for them and thus waste resources, especially with growing numbers of simultaneous user sessions. The next important step is therefore a more flexible, efficient and robust communication model which would then allow the parallel session management to be stressed and also fine-tuned to perform well in practice.
2.5 Other improvements to \isac{} include utilizing of \isabelle{}'s function package and code generator to simplify and speedup \isac{}'s programming language, adaptation of \isabelle{}'s capabilities with respect to floating point numbers and complex numbers, possibly adopt term nets for better performance of \isac{}'s rewrite engine. The latter plans for improvement of the mathematics-engine can be pursued independently from work on the front-end due to a stable interface in between. While \isac{}'s own front-end will be extended and improved, future development of the \textit{Isabelle/jEdit} IDE may enable \isac{} to adopt it as its front-end in the long run.
2.6
2.7 -The whole case study involved deeply invasive refactoring processes. The presence auf automatic tools for this kind of tasks in \textit{Standard ML} would have been desireable. While there has been related work on \textit{Haskell} \cite{brown2012paraforming,thompson2005refactoring,dig2011refactoring,li2006comparative} and \textit{Erlang} \cite{brown2013cost,li2006comparative}, there are, to my knowledge, no such projects specificly for \textit{Standard ML} available. These could also help remove unused code and support convenient restructuring of modules.
2.8 +The whole case study involved deeply invasive refactoring processes. The presence of automatic tools for this kind of tasks in \textit{Standard ML} would have been desirable. While there has been related work on \textit{Haskell} \cite{brown2012paraforming,thompson2005refactoring,dig2011refactoring,li2006comparative} and \textit{Erlang} \cite{brown2013cost,li2006comparative}, there are, to my knowledge, no such projects specifically for \textit{Standard ML} available. These could also help remove unused code and support convenient restructuring of modules.
2.9 % TODO: isa_pide_educational.pdf
2.10
2.11 %>>> Sind die Streams zwischen Mathematikengine und Frontend
3.1 --- a/master/thesis/fundamentals.tex Thu Jun 26 02:58:44 2014 +0200
3.2 +++ b/master/thesis/fundamentals.tex Sun Jul 20 16:31:11 2014 +0200
3.3 @@ -13,7 +13,7 @@
3.4
3.5 In 1978 John Backus, who had been heavily involved in the design of \textit{Fortran} and \textit{ALGOL}, held a Turing award lecture which emphasized certain benefits of functional style languages over imperative programming. The document which resulted from the lecture \cite{backus1978can} strongly influenced and fueled research in the area of functional programming. Also in the mid 1970s, Robin Milner and others from the \textit{University of Edinburgh} designed the \textit{ML} {\em metalanguage} as a command language for the theorem prover {\em LCF} \cite{milner1978theory} (see section \ref{sec:ctp}). They continued the development of \textit{ML} and turned it into a stand-alone programming language. Even though it has impure features such as mutable references and an I/O system which is not side effect free, \textit{ML} is known as a functional programming language because it encourages a functional programming style. \textit{ML}'s type system employs the {\em Hindley–Milner type inference algorithm} (see section \ref{sec:hindleymilner}) which reduces the number of required type annotations because it can infer the types of expressions in most cases. Later, a standard for the language was established \cite{milner1997definition}, which resulted in the programming language \textit{Standard ML}.
3.6
3.7 -As a dozen non-strict languages (i.e. employing lazy evaluation) emerged in the 1980s, it was decided at a conference in 1987 that the parallel efforts should be merged into one common language as a basis for an exchange of ideas. This decision resulted in the formation of a commitee which created {\em Haskell} \cite{jones2003haskell}. Research around this purely functional, general-purpose programming language has produced many innovations in the area of functional programming during the last two decades.
3.8 +As a dozen non-strict languages (i.e. employing lazy evaluation) emerged in the 1980s, it was decided at a conference in 1987 that the parallel efforts should be merged into one common language as a basis for an exchange of ideas. This decision resulted in the formation of a committee which created {\em Haskell} \cite{jones2003haskell}. Research around this purely functional, general-purpose programming language has produced many innovations in the area of functional programming during the last two decades.
3.9
3.10 \subsection{Common Features}
3.11 There are certain distinguishing features which can be found in most contemporary functional programming languages. This section outlines the most prevalent ones (e.g., see \cite{hudak1989conception, haskell2013functional}).
3.12 @@ -22,7 +22,7 @@
3.13 The heavy use of immutable data has already been mentioned in section \ref{sec:funprog}. A consequence of pure functions is {\em referential transparency}, which is the property of computations which always yield equal results whenever they are invoked with the same input parameters. Later in this section we will see how pure languages enable e.g. input, output and exception handling whilst preserving purity.
3.14
3.15 \subsubsection{Recursion}
3.16 -Recursion is not a technique which is specific to functional programming. However, since loops require the use of mutable values (counter variables), recursion is used way more excessively than in imperative languages. Often, it is the only way to describe iterations. As recursion can easily cause an overflow of the call stack, most implementations of functional languages employ {\em tail call optimization}. This mechanism discards a function call's environment and thereby aviods creating a new stack frame for the recursive call and saves memory. This only works for true tail recursion, i.e. if the result of the recursive call is the result of the function itself.
3.17 +Recursion is not a technique which is specific to functional programming. However, since loops require the use of mutable values (counter variables), recursion is used way more excessively than in imperative languages. Often, it is the only way to describe iterations. As recursion can easily cause an overflow of the call stack, most implementations of functional languages employ {\em tail call optimization}. This mechanism discards a function call's environment and thereby avoids creating a new stack frame for the recursive call and saves memory. This only works for true tail recursion, i.e. if the result of the recursive call is the result of the function itself.
3.18
3.19 \subsubsection{Higher-Order Functions}
3.20 Higher-order functions (HOFs) are functions which expect other functions as their input parameters or have functions as their return values. Examples for frequently used HOFs are the {\em map} and {\em fold} operations, which apply other functions to lists of values as in the \textit{Standard ML} expression
3.21 @@ -32,7 +32,7 @@
3.22
3.23 \subsubsection{Purity and Effects}
3.24 \label{sec:pureeffects}
3.25 -Many functional programming languages such as \textit{Standard ML} encourage a purely funcional coding style. However, certain functionalities like memory I/O require developers to write impure code. Purely functional programming languages like \textit{Haskell} and \textit{Clean} do not permit any side effects and therefore use other mechanisms to accomplish the desired effects. The \textit{Haskell} developers decided to implement a language construct called {\em monad} \cite{jones2003haskell}. Monads can be described as representations of possibly impure computations. In order to preserve purity, functions which perform e.g. I/O operations have to accept monads as arguments or return them. Similarly, \textit{Clean} uses {\em uniqueness types} \cite{achten1995ins} which ensure that every function's type makes transparent to the environment, which mutable aspects of the environment it manipulates. This is accomplished by allowing these functions exactly one access to the denoted mutable data which they receive as arguments and whose manipulated versions are contained in their return values.
3.26 +Many functional programming languages such as \textit{Standard ML} encourage a purely functional coding style. However, certain functionality like memory I/O require developers to write impure code. Purely functional programming languages like \textit{Haskell} and \textit{Clean} do not permit any side effects and therefore use other mechanisms to accomplish the desired effects. The \textit{Haskell} developers decided to implement a language construct called {\em monad} \cite{jones2003haskell}. Monads can be described as representations of possibly impure computations. In order to preserve purity, functions which perform e.g. I/O operations have to accept monads as arguments or return them. Similarly, \textit{Clean} uses {\em uniqueness types} \cite{achten1995ins} which ensure that every function's type makes transparent to the environment, which mutable aspects of the environment it manipulates. This is accomplished by allowing these functions exactly one access to the denoted mutable data which they receive as arguments and whose manipulated versions are contained in their return values.
3.27
3.28 \subsubsection{Partial Function Evaluation}
3.29 Partial function evaluation facilitates applying less arguments to a function than it requires which results in another function that only requires the remaining arguments. E.g. the function \texttt{fun add x y = x + y} accepts two arguments. Its partial evaluation \texttt{val add2 = add 2} results in a function which only expects one argument and adds 2 to it.
3.30 @@ -47,12 +47,12 @@
3.31
3.32
3.33 \subsubsection{Lazy Evaluation}
3.34 -Due to referencial transparency, the order in which expressions are evaluated does not affect the results. Therefore, some languages like \textit{Haskell} defer the computation of expressions until they are actually needed. This avoids unnecessary calculations and makes infinite data structures possible. On the other hand, lazy evaluation can potentially cause space leaks \cite{launchbury1993natural} and it makes formal reasoning about code hard \cite{lippmeier2009type}. The opposite is called {\em eager} or {\em strict} evaluation which is the standard for most imperative languages and e.g. \textit{Standard ML}.
3.35 +Due to referential transparency, the order in which expressions are evaluated does not affect the results. Therefore, some languages like \textit{Haskell} defer the computation of expressions until they are actually needed. This avoids unnecessary calculations and makes infinite data structures possible. On the other hand, lazy evaluation can potentially cause space leaks \cite{launchbury1993natural} and it makes formal reasoning about code hard \cite{lippmeier2009type}. The opposite is called {\em eager} or {\em strict} evaluation which is the standard for most imperative languages and e.g. \textit{Standard ML}.
3.36
3.37
3.38 \section{Computer Theorem Proving}
3.39 \label{sec:ctp}
3.40 -Computer Theorem Proving is related to functional programming in serveral fundamental ways. My practical work for this thesis concerned TP ({\bf T}heorem {\bf P}roving) on a technical level below the logical level of TP, on the level of parallel execution on multi-core hardware. However, it is the logical level of TP which provides the fundamental relations to functional programming.
3.41 +Computer Theorem Proving is related to functional programming in several fundamental ways. My practical work for this thesis concerned TP ({\bf T}heorem {\bf P}roving) on a technical level below the logical level of TP, on the level of parallel execution on multi-core hardware. However, it is the logical level of TP which provides the fundamental relations to functional programming.
3.42
3.43 \subsection{History}
3.44 \label{ssec:ctp-hist}
3.45 @@ -62,11 +62,11 @@
3.46 Mechanical or ``formal'' reasoning was an original interest of Artificial Intelligence (AI). The first important programming languages in AI were \textit{Prolog} (logic programming) and \textit{Lisp}. The latter was briefly introduced as a functional language in section \ref{sec:funhist}.
3.47
3.48 \paragraph{\textit{Automath}.}
3.49 -A first notable success was the mechanisation of Edmund Landau's {\em Foundations of Analysis} \cite{van1979checking} in {\em Automath} in 1969. {\em Automath} is outdated, but some of its achievements are still used in TP, e.g. de-Brujin indices, the lambda calculus and Curry-Howard correspondence. This early succcess in TP was not acknowledged by mainstream mathematics. Rather, TP was mixed up with predictions of early AI, e.g. Herbert A. Simon's claim that ``{\em [m]achines will be capable, within twenty years, of doing any work a man can do.}'' \cite{simon1965shape}; predictions that soon turned out to be unrealistic. Nevertheless, mechanisation of various logics (sequent calculus, temporal logics, communicating sequential processes (see section \ref{sec:csp}), etc.) was continued and led to many different, unrelated software tools.
3.50 +A first notable success was the mechanization of Edmund Landau's {\em Foundations of Analysis} \cite{van1979checking} in {\em Automath} in 1969. {\em Automath} is outdated, but some of its achievements are still used in TP, e.g. de-Brujin indices, the lambda calculus and Curry-Howard correspondence. This early success in TP was not acknowledged by mainstream mathematics. Rather, TP was mixed up with predictions of early AI, e.g. Herbert A. Simon's claim that ``{\em [m]achines will be capable, within twenty years, of doing any work a man can do.}'' \cite{simon1965shape}; predictions that soon turned out to be unrealistic. Nevertheless, mechanization of various logics (sequent calculus, temporal logics, communicating sequential processes (see section \ref{sec:csp}), etc.) was continued and led to many different, unrelated software tools.
3.51
3.52 \paragraph{\textit{LCF}.}
3.53 \label{sssec:lcf}
3.54 -\textit{LCF} (Logic for Computable Functions) \cite{milner1978theory} denotes an interactive, automated theorem prover developed at the universities of Edinburgh and Stanford in the early 1970s. The \textit{LCF} project is relevant for this thesis, because it introduced the \textit{ML} programming language explored in section \ref{sec:isasml} and was used for the practical work within the thesis. The purpose of \textit{LCF} was to allow users to write theorem proving tactics and to encapsulate theorems as abstract da\-ta\-types, such that only the admitted inference rules can establish a theorem. This is still called {\em LCF princple}. \textit{LCF} became the ancestor of the {\em HOL family} of provers introduced below.
3.55 +\textit{LCF} (Logic for Computable Functions) \cite{milner1978theory} denotes an interactive, automated theorem prover developed at the universities of Edinburgh and Stanford in the early 1970s. The \textit{LCF} project is relevant for this thesis, because it introduced the \textit{ML} programming language explored in section \ref{sec:isasml} and was used for the practical work within the thesis. The purpose of \textit{LCF} was to allow users to write theorem proving tactics and to encapsulate theorems as abstract da\-ta\-types, such that only the admitted inference rules can establish a theorem. This is still called {\em LCF principle}. \textit{LCF} became the ancestor of the {\em HOL family} of provers introduced below.
3.56
3.57 \paragraph{\textit{The Next Seven Hundred Theorem Provers}.}
3.58 \label{par:next-700}
3.59 @@ -88,7 +88,7 @@
3.60 \subsection{Relevance}
3.61
3.62 \paragraph{The executable fragment of HOL and code generation.}
3.63 -As already mentioned, higher-order logic is closely related to functional programming. This relation includes an executable fragment, i.e. equational theorems within HOL, which can model programs and which can be evaluated within the logic. This way of embedding programs in the logical environment provides the best prerequisites for proving properties of programs and for software verification. \isabelle{} recentely implemented a {\em function package}. Execution, or more appropriately, evaluation, within a prover is very inefficient in comparison with state-of-the-art production software. Therefore engineering software cannot be built within a prover. However, it turned out that algorithms described within the executable fragment of HOL are a concise source for automatic generation of efficient code in a surprisingly straight forward manner.
3.64 +As already mentioned, higher-order logic is closely related to functional programming. This relation includes an executable fragment, i.e. equational theorems within HOL, which can model programs and which can be evaluated within the logic. This way of embedding programs in the logical environment provides the best prerequisites for proving properties of programs and for software verification. \isabelle{} recently implemented a {\em function package}. Execution, or more appropriately, evaluation, within a prover is very inefficient in comparison with state-of-the-art production software. Therefore engineering software cannot be built within a prover. However, it turned out that algorithms described within the executable fragment of HOL are a concise source for automatic generation of efficient code in a surprisingly straight forward manner.
3.65
3.66 \paragraph{Functional programming.}
3.67 Software verification tools are presently already more advanced for functional programming languages. And the theoretical background presented in this section indicates that verification tools will develop better in the paradigm of functional programming than in other paradigms. Also, efficiency considerations are expected to change in favor of the functional paradigm. Programs written on an abstract level in a TP can be transformed into efficient code by automated code generation. This transformation can potentially handle parallelization much more conveniently than programs developed within other paradigms \cite{haftmann2010code}.
3.68 @@ -96,7 +96,7 @@
3.69
3.70 \section{Parallelism}
3.71 \label{sec:parallelism}
3.72 -Concurrency in software has been around for a long time and without it, multitasking would be impossible. It means that processes and threads may be started, executed and completed in overlapping time periods. This does not necessarily imply any parallel, i.e. simultaneous, execution. Parallel software is structured in a way which allows for literally simultaneous execution, e.g. on multi-core processors. Now that this kind of processors is used heavily in PCs, laptops and smartphones, efficient software must be able to exploit parallelism. Approaches to parallelism can roughly be grouped into three different levels: {\em instruction-level} (section \ref{sec:multicoreproc}), {\em task parallelism} (section \ref{sec:task_par}) and {\em data} (section \ref{sec:data_parallelism}). The following sections will establish a theoretical background of parallelism.
3.73 +Concurrency in software has been around for a long time and without it, multitasking would be impossible. It means that processes and threads may be started, executed and completed in overlapping time periods. This does not necessarily imply any parallel, i.e. simultaneous, execution. Parallel software is structured in a way which allows for literally simultaneous execution, e.g. on multi-core processors. Now that this kind of processors is used heavily in PCs, laptops and smart phones, efficient software must be able to exploit parallelism. Approaches to parallelism can roughly be grouped into three different levels: {\em instruction-level} (section \ref{sec:multicoreproc}), {\em task parallelism} (section \ref{sec:task_par}) and {\em data} (section \ref{sec:data_parallelism}). The following sections will establish a theoretical background of parallelism.
3.74
3.75 \subsection{Gain, Cost and Limits}
3.76 Formulated in 1967, Amdahl's Law \cite{amdahl1967validity} describes the correlation between the inherently sequential fraction of a program and the resulting maximally possible speedup $S_A$ under parallel execution (see fig. \ref{fig:amdahls}), given by
3.77 @@ -183,13 +183,13 @@
3.78 \begin{description}
3.79 \item[Bit-level parallelism] takes advantage of increased processor word sizes in order to reduce the number of instructions that need to be executed to complete operations on variables which are longer than one word \cite{culler1999parallel}.
3.80
3.81 -\item[Instruction-level parallelism] tries to discover data independent instructions which often can be reordered and computed during the same processing cycle. Also, instruction piplines with multiple stages allow different instructions to be in different stages and thereby overlap their processing \cite{hennessy2012computer}.
3.82 +\item[Instruction-level parallelism] tries to discover data independent instructions which often can be reordered and computed during the same processing cycle. Also, instruction pipelines with multiple stages allow different instructions to be in different stages and thereby overlap their processing \cite{hennessy2012computer}.
3.83
3.84 \item[Simultaneous multithreading] enables multiple threads to issue instructions on a single processing core which may be processed during the same cycle \cite{tullsen1995simultaneous}.
3.85 \end{description}
3.86
3.87 \subsection{Operating Systems}
3.88 -Operating systems are heavily involved in the resource management of their underlying architecture, both for their own operations and for user applications. Besides support for simultaneous multithreading (see previous section), general-purpose OSes have to deal with diverse hardware approaches, e.g. multiprocessors vs. multi-core processors, shared vs. separate cache models. Scheduling algorithms and memory management are facing new challenges because they must balance loads between cores while avoiding cache misses and reducing the number of context switches. In this thesis we will assume symmetric multiprocessing (SMP), i.e. systems whose processing cores are identical and access the same main memory. Scheduling algorithms in OSes for more heterogenous systems also need to take into account differing performance characteristics and possibly even instruction sets of several processors.
3.89 +Operating systems are heavily involved in the resource management of their underlying architecture, both for their own operations and for user applications. Besides support for simultaneous multithreading (see previous section), general-purpose OSes have to deal with diverse hardware approaches, e.g. multiprocessors vs. multi-core processors, shared vs. separate cache models. Scheduling algorithms and memory management are facing new challenges because they must balance loads between cores while avoiding cache misses and reducing the number of context switches. In this thesis we will assume symmetric multiprocessing (SMP), i.e. systems whose processing cores are identical and access the same main memory. Scheduling algorithms in OSes for more heterogeneous systems also need to take into account differing performance characteristics and possibly even instruction sets of several processors.
3.90
3.91 \subsection{Functional Programming}
3.92 \label{sec:par_funprog}
3.93 @@ -214,7 +214,7 @@
3.94 \label{sec:refacfunprogs}
3.95 Refactoring is a process which changes the design and structure of existing software without changing its external behavior. It can result in simpler programs, remove duplicate code or prepare an extension of the program's functionality. Because refactoring is a potentially tedious and error-prone process \cite{thompson2005refactoring}, there is a variety of tools which automatically check preconditions for and apply refactoring steps for object-oriented programming languages. The number of such tools for functional programming languages, however, is limited. One of the few existing projects targets \textit{Haskell} code and is called {\em HaRe} (\textit{\textbf{Ha}skell} \textbf{Re}factorer). It follows five main strategies:
3.96 \begin{enumerate}
3.97 - \item {\bf Generalisation.} Extract some of a function's behavior into an argument, possibly a HOF, and thereby make the function more general and reusable.
3.98 + \item {\bf Generalization.} Extract some of a function's behavior into an argument, possibly a HOF, and thereby make the function more general and reusable.
3.99 \item {\bf Commonality.} Similar or identical parts of a program are identified, extracted into a single function which is invoked at the respective locations and with appropriate parameters.
3.100 \item {\bf Data Abstraction.} Replacing algebraic da\-ta\-types by abstract da\-ta\-types often allows programmers to modify concrete implementations without touching client code.
3.101 \item {\bf Overloading.} The use of {\em type classes} and {\em instances} allows for overloading of names. This may improve readability and facilitate code reuse.
4.1 --- a/master/thesis/funproglangs_mcsystems.tex Thu Jun 26 02:58:44 2014 +0200
4.2 +++ b/master/thesis/funproglangs_mcsystems.tex Sun Jul 20 16:31:11 2014 +0200
4.3 @@ -2,7 +2,7 @@
4.4 \label{cha:funproglangs_mcsystems}
4.5 This section presents several concepts for parallelism and concurrency which have been suggested for and implemented in functional programming languages. The central idea here is the philosophy of the declarative paradigm: The developer should not have to worry about {\em how} the parallel execution needs to be organized but at most make informed decisions on {\em what} has to be parallelized. Ideally, process management details such as process creation, resource assignment and synchronization should be taken care of by compiler and run-time system. In practice, various properties of languages such as impureness and monadic I/O, may allow for language constructs from imperative programming or even require forms of explicit synchronization.
4.6
4.7 -Many of the mechanisms presented in the following sections have been implemented in and modified for certain programming languages. It seemed appropriate to place details on these realization details and changes in the respective sections. Table \ref{tab:lang_par_overview} gives a brief overview. Note that it only contains those michanisms and sections that mention concrete implementations.
4.8 +Many of the mechanisms presented in the following sections have been implemented in and modified for certain programming languages. It seemed appropriate to place details on these realization details and changes in the respective sections. Table \ref{tab:lang_par_overview} gives a brief overview. Note that it only contains those mechanisms and sections that mention concrete implementations.
4.9 \begin{table}[ht]
4.10 \centering
4.11 \caption{Overview of parallelism mechanisms and referenced programming languages.}
4.12 @@ -61,7 +61,7 @@
4.13 \label{sec:annot}
4.14 Another straight forward solution is the use of annotations. This is probably the simplest way of expressing parallelism because it does not affect the semantics of a program but only its runtime behavior. By ignoring the annotations the program can then still be compiled sequentially. This method has been implemented in the programming language \textit{Clean} \cite{nocker1991concurrent} which also allows indications of the target processing unit for the evaluation. Since eager languages evaluate a function's arguments before invoking the function itself, this mechanism, in its simple form, only works for lazy languages. A potential implementation of the parallel {\tt fib} function\footnote{see comments in appendix \ref{sec:fib-imp}} in a lazy version of \textit{Standard ML} could look somewhat like the definition
4.15 \imlcode{\label{alg:parannot}
4.16 -~~\=fu\=n fib 0 = 1\\
4.17 +~~\=fu\=n fib 0 = 0\\
4.18 \>\>| fib 1 = 1\\
4.19 \>\>| fib x = fib (x - 1) + par (fib (x - 2)); \textrm{.}}
4.20 \noindent
4.21 @@ -71,7 +71,7 @@
4.22 \label{sec:futurespro}
4.23 The concepts of {\em promises} and {\em futures} were first suggested in the mid 1970s \cite{baker1977incremental}. The idea is similar to annotations (see previous section). One of the first languages that adopted futures was called {\em Multilisp} \cite{halstead1985multilisp}. As the {\em Isabelle} theorem prover provides its own implementation of futures \cite{matthews2010efficient} which have been introduced to \isac{} during the parallelization process (section \ref{ssec:session-manag}), they are of special interest for this thesis. Futures are objects representing the result of an expression which may not be known initially because its computation is managed by the run-time system and may occur in parallel. {\em Implicit} futures are usually an integral part of a language and treated like ordinary references. If results are not available the first time they are requested, program execution stops until the future value has been obtained. In contrast, {\em explicit} futures require programmers to manually enforce their computations before they can access their results. {\em Isabelle}'s solution follows the latter approach and will be discussed in more detail in section \ref{sec:isafut}. The definition
4.24 \imlcode{\label{alg:futures}
4.25 -~~\=fu\=n \=fi\=b \=0 = 1\\
4.26 +~~\=fu\=n \=fi\=b \=0 = 0\\
4.27 \>\>| fib 1 = 1\\
4.28 \>\>| fib x = let\\
4.29 \>\>\>\>\>fun fib' () = fib (x - 2)\\
4.30 @@ -90,7 +90,7 @@
4.31
4.32 \subsection{Algorithmic Skeletons}
4.33 \label{sec:algoskel}
4.34 -The idea of algorthmic skeletons is simple and not limited to parallelism. Most parallel algorithms show common patterns. These patterns can be abstracted into higher-order functions. A well known example is {\em divide-and-conquer}:
4.35 +The idea of algorithmic skeletons is simple and not limited to parallelism. Most parallel algorithms show common patterns. These patterns can be abstracted into higher-order functions. A well known example is {\em divide-and-conquer}:
4.36 \imlcode{~~\=fu\=n \=da\=c \=is\=\_trivial solve divide conquer x =\\
4.37 \>\>\>if is\_trivial x then\\
4.38 \>\>\>\>solve x\\
4.39 @@ -99,7 +99,7 @@
4.40 \>\>\>\>\>|> map (dac is\_trivial solve divide conquer)\\
4.41 \>\>\>\>\>|> conquer; \textrm{,}}
4.42 \noindent
4.43 -where \texttt{x |> f} is syntactic sugar for \texttt{f x} and \texttt{is\_trivial} is a function with one argument and a \texttt{bool} return value. In order to parallelize the algorithm we only need to use a parallel version of {\tt map}. Other common patterns include {\em branch-and-bound} and {\em dynamic programming}. While this method is also available for imperative languages such as \textit{Java}, the fact that functional languages treat higher-order functions as first-class citizens makes them particularly suitable for the use of skeletons. Algorithmic skeletons hide the orchestration between sequential portions of code from the programmer. Sometimes the compiler can provide low-level support for the skeletons. Furthermore, multiple primitive skeletons can be composed to produce more powerful patterns. Unlike other high-level parallelism mechanisms, they are apt to cost modelling \cite{hammond2000research}.
4.44 +where \texttt{x |> f} is syntactic sugar for \texttt{f x} and \texttt{is\_trivial} is a function with one argument and a \texttt{bool} return value. In order to parallelize the algorithm we only need to use a parallel version of {\tt map}. Other common patterns include {\em branch-and-bound} and {\em dynamic programming}. While this method is also available for imperative languages such as \textit{Java}, the fact that functional languages treat higher-order functions as first-class citizens makes them particularly suitable for the use of skeletons. Algorithmic skeletons hide the orchestration between sequential portions of code from the programmer. Sometimes the compiler can provide low-level support for the skeletons. Furthermore, multiple primitive skeletons can be composed to produce more powerful patterns. Unlike other high-level parallelism mechanisms, they are apt to cost modeling \cite{hammond2000research}.
4.45
4.46
4.47 \section{Data Parallelism}
4.48 @@ -117,7 +117,7 @@
4.49
4.50 \subsection{Software Transactional Memory}
4.51 \label{sec:stm}
4.52 -While hardware support for transactions had been introduced before and they were a fundamental aspect of fault tolerance in the context of database systems, software-only transactional memory was first suggested by Shavit and Touitou in 1997 \cite{shavit1997software}. Unlike {\em lock-based synchronization} STM generally is a non-blocking strategy. Transactions are sequences of read and write operations on a shared memory. They are tagged atomic blocks, processed optimistically, regardless of other threads potentially performing other alterations to the memory simultaneously. Each access to the memory is logged and once a transaction is finished, a final validation step verifies that no other thread modified any of the elements which were read during the process, i.e. the transaction's view of the memory was consistent. If there was no conflicting write access, the transaction is commited to the memory. Otherwise the whole process is repeated until no more conflicts arise. In order to be correct, transactions must be linearizable, i.e. it must be possible to execute them in a certain sequence without temporal overlaps, such that the resulting state of the shared memory is the same as if the transactions had been carried out concurrently \cite{herlihy1990linearizability}. Because of their non-blocking nature, STMs do not cause deadlocks or priority inversion. They are inherently fault tolerant to a certain extent, because transactions can be undone in the event of a timeout or an exception. Also, they are free from the tradeoffs between lock granularity and concurrency.
4.53 +While hardware support for transactions had been introduced before and they were a fundamental aspect of fault tolerance in the context of database systems, software-only transactional memory was first suggested by Shavit and Touitou in 1997 \cite{shavit1997software}. Unlike {\em lock-based synchronization} STM generally is a non-blocking strategy. Transactions are sequences of read and write operations on a shared memory. They are tagged atomic blocks, processed optimistically, regardless of other threads potentially performing other alterations to the memory simultaneously. Each access to the memory is logged and once a transaction is finished, a final validation step verifies that no other thread modified any of the elements which were read during the process, i.e. the transaction's view of the memory was consistent. If there was no conflicting write access, the transaction is committed to the memory. Otherwise the whole process is repeated until no more conflicts arise. In order to be correct, transactions must be linearizable, i.e. it must be possible to execute them in a certain sequence without temporal overlaps, such that the resulting state of the shared memory is the same as if the transactions had been carried out concurrently \cite{herlihy1990linearizability}. Because of their non-blocking nature, STMs do not cause deadlocks or priority inversion. They are inherently fault tolerant to a certain extent, because transactions can be undone in the event of a timeout or an exception. Also, they are free from the tradeoffs between lock granularity and concurrency.
4.54
4.55 Recent work on {\em commitment ordering} has helped reduce the number of transaction conflicts and thereby improve performance of STM implementations \cite{ramadan2009committing,zhang2010software}. Also, there are various STM solutions that do in fact use locking mechanisms during different phases of transaction. They can potentially reduce the number of rollbacks and consequently also make process coordination faster \cite{ennals2006software}. The significant difference between these approaches and conventional, mutex based thread synchronization mechanisms is the fact that with STM, any locking is invisible to the programmer and taken care of by the run-time system. The downside of STM is the performance overhead caused by transaction management which typically impairs the performance of programs with a low number of threads, such that they are slower than when implemented in a sequential manner. STMs, however, scale particularly well with respect to higher thread and processor numbers \cite{saha2006mcrt}.
4.56
4.57 @@ -131,7 +131,7 @@
4.58
4.59 \subsection{The Actor Model}
4.60 \label{sec:actormodel}
4.61 -In 1973, Hewitt, Bishop and Steiger suggested a modular actor formalism \cite{hewitt1973universal} which laid out the basis of what is now known as the {\em Actor model}. Several publications of the following decade formed a comprehensive Actor model theory. The two central concepts of the Actor model are {\em actors} and {\em messages} \cite{agha1985actors}. Actors are entities that can send and receive messages. Their behavior is defined by the {\bf actions} they perform on receipt of a message (e.g. create another actor) and a finite number of other actors they know about, called {\bf acquaintances}. The acquantance relation is not necessarily bidirectional, i.e. an acquantance $B$ of actor $A$ must not necessarily know actor $A$. Each actor has an immutable, unique name and a local state. Communication between actors is asynchronous. Incoming messages are processed one at a time and as a response to each message an atomic sequence of actions is performed. Since actors and messages are autonomous, encapsulated entities they are easy to reason about and can be composed into more complex systems \cite{agha1997foundation}. The order of actions affects an actor's external behavior. But because messaging occurs asynchronously, the processing order of messages is undefined. This leads to nondeterminism in computations based on the actor system. There are certain abstractions available which allow for constraints on message ordering and can therefore eliminate part of the nondeterminism \cite{karmani2009actor}. They can be summarized in four important properties:
4.62 +In 1973, Hewitt, Bishop and Steiger suggested a modular actor formalism \cite{hewitt1973universal} which laid out the basis of what is now known as the {\em Actor model}. Several publications of the following decade formed a comprehensive Actor model theory. The two central concepts of the Actor model are {\em actors} and {\em messages} \cite{agha1985actors}. Actors are entities that can send and receive messages. Their behavior is defined by the {\bf actions} they perform on receipt of a message (e.g. create another actor) and a finite number of other actors they know about, called {\bf acquaintances}. The acquaintance relation is not necessarily bidirectional, i.e. an acquaintance $B$ of actor $A$ must not necessarily know actor $A$. Each actor has an immutable, unique name and a local state. Communication between actors is asynchronous. Incoming messages are processed one at a time and as a response to each message an atomic sequence of actions is performed. Since actors and messages are autonomous, encapsulated entities they are easy to reason about and can be composed into more complex systems \cite{agha1997foundation}. The order of actions affects an actor's external behavior. But because messaging occurs asynchronously, the processing order of messages is undefined. This leads to non-determinism in computations based on the actor system. There are certain abstractions available which allow for constraints on message ordering and can therefore eliminate part of the non-determinism \cite{karmani2009actor}. They can be summarized in four important properties:
4.63 \begin{enumerate}
4.64 \item {\bf Encapsulation.} Unlike shared memory thread models, actors are highly encapsulated. Therefore, they provide no locking or synchronization mechanisms for shared resources. Their internal states are not directly accessible by other actors. The only way for them to exchange data or influence each other is by means of messages. This limitation, however, is violated by some implementations in languages such as \textit{Scala} \cite{thurauakka}. In programming languages which permit mutable data, messages should, in theory, not transfer references to locations in a shared address space. Otherwise the receiving party could modify memory locations that are contained in another actor's state representation. However, \textit{Java}'s actor library {\em Akka} allows actors to do just that and it is the programmer's responsibility to maintain encapsulation.
4.65 \item {\bf Fairness.} Another important property is fairness with respect to actor sched\-ul\-ing: a message will be delivered to its target actor eventually, i.e. unless an actor dies or displays faulty behavior, it will be scheduled in a fair manner.
4.66 @@ -145,7 +145,7 @@
4.67
4.68 \subsubsection{\textit{Scala}}
4.69 \label{sec:actors_scala}
4.70 -\textit{Scala} is a programming language for the \textit{Java Virtual Machine} that combines concepts of object-oriented and functional programming \cite{odersky2004overview}. Its distribution comes with a toolkit for actors and message passing functionality called {\em Akka}. \textit{Scala}'s standard actors library up to version 2.9.2 \cite{scala2014migration} has now been depricated and replaced by \textit{Akka}. Its implementation is based on \textit{Erlang} like, fault tolerant actors and its execution model follows an {\em event-based} approach, thus introducing {\em inversion of control}. Compared to \textit{Scala}'s orginal actors, \textit{Akka} actors are more performant, fault tolerant and offer automatic load balancing \cite{tasharofi2013scala}. They draw on the language's functional programming features such as partial functions and, like \textit{Erlang}, pattern matching which are convenient for message passing. Actors potentially provide safer concurrency than traditional shared memory mechanisms because by design, no race conditions can occur. Also, actors are more lightweight than threads.
4.71 +\textit{Scala} is a programming language for the \textit{Java Virtual Machine} that combines concepts of object-oriented and functional programming \cite{odersky2004overview}. Its distribution comes with a toolkit for actors and message passing functionality called {\em Akka}. \textit{Scala}'s standard actors library up to version 2.9.2 \cite{scala2014migration} has now been deprecated and replaced by \textit{Akka}. Its implementation is based on \textit{Erlang} like, fault tolerant actors and its execution model follows an {\em event-based} approach, thus introducing {\em inversion of control}. Compared to \textit{Scala}'s original actors, \textit{Akka} actors are more performant, fault tolerant and offer automatic load balancing \cite{tasharofi2013scala}. They draw on the language's functional programming features such as partial functions and, like \textit{Erlang}, pattern matching which are convenient for message passing. Actors potentially provide safer concurrency than traditional shared memory mechanisms because by design, no race conditions can occur. Also, actors are more lightweight than threads.
4.72 % why no race conditions!?!?!?
4.73
4.74 \subsubsection{Futures}
5.1 --- a/master/thesis/introduction.tex Thu Jun 26 02:58:44 2014 +0200
5.2 +++ b/master/thesis/introduction.tex Sun Jul 20 16:31:11 2014 +0200
5.3 @@ -11,9 +11,9 @@
5.4 \caption{Intel CPU trends (source: \cite{sutter2005free}).}
5.5 \label{fig:chip-speeds}
5.6 \end{figure}
5.7 -Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and higly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster.
5.8 +Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and highly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster.
5.9
5.10 -Functional programming is a declarative paradigm based on the lambda calculs. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}).
5.11 +Functional programming is a declarative paradigm based on the lambda calculus. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}).
5.12
5.13 The interactive theorem prover \isabelle{} \cite{nipkow2002isabelle} is a comprehensive, international software project. Its internal logic has been written entirely in {\em Standard ML} which later was embedded in a {\em Scala} environment to simplify interaction with the underlying operating system and software built on top of \isabelle{}. As the use of multi-core systems became more common, \isabelle{}'s computationally complex logic was required to exploit the newly available processing power. Makarius Wenzel, one of the leading developers of \isabelle{}, parallelized essential parts of the system within a few man months (scattered over about two years). This is a surprisingly little amount of effort considering the project's size and complexity. A significant amount of the work was required due to the use of impure code, facilitated by \textit{Standard ML} and \textit{Scala}, i.e. work concerning purification in terms of the functional paradigm. {\em Isabelle/Scala} provides tools for interaction between front-end and proof engine and contains object-oriented components to deal with inherently stateful aspects of the development environment {\em Isabelle/jEdit}.
5.14
5.15 @@ -22,4 +22,4 @@
5.16
5.17 \section{Thesis Structure}
5.18 \label{sec:thesis_structure}
5.19 -The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible futurework are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis.
5.20 +The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible future work are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis.
6.1 --- a/master/thesis/isabelle_isac.tex Thu Jun 26 02:58:44 2014 +0200
6.2 +++ b/master/thesis/isabelle_isac.tex Sun Jul 20 16:31:11 2014 +0200
6.3 @@ -64,7 +64,7 @@
6.4 \textit{ML} stands for {\em meta language}. The language was briefly introduced in section \ref{sec:funhist}. It is a strongly typed, functional programming language, which is not pure as it allows side effects and updatable references. Many people contributed ideas to the language. In order maintain a common ground, a standard was established \cite{milner1997definition}. All the code samples in this document are written in \textit{Standard ML} syntax. Since \textit{Standard ML} is only a language definition which is not dictated by a reference implementation, there are multiple compilers available, most notably {\em Standard ML of New Jersey} ({\em SML/NJ}) \cite{smlnj2013standard}, {\em MLton} \cite{weeks2006whole} and {\em Moscow ML} \cite{romanenko2014moscow}. They differ in their priorities such as optimization, standard library size or platform support. \textit{ML} was originally designed as a command language for the interactive theorem prover \textit{LCF} (section \ref{sssec:lcf}) \cite{milner1978theory}. Because of its history in this area, it was specifically suitable for the development of \isabelle{}. Inference rules can easily be implemented as functions that accept a theorem and return a new one. Complete theorems can be constructed by applying a sequence of rules to other known theorems.
6.5
6.6 \paragraph{The Hind\-ley-Mil\-ner Type System.}\label{sec:hindleymilner}
6.7 -\textit{Standard ML} makes use of {\em Hind\-ley-Mil\-ner type inference} \cite{milner1978theory} based on a type system for the lambda calculus which utilizes parametric polymorphism, i.e. types can be declared using type variables (e.g. \textit{Synchronized} signature on page \pageref{alg:guarded_access_sig}) and the decision on the instantiated types is left to the inference algorithm. This allows for the generic definition of functions while still ensuring static type safety. The type inference method is complete and is able to always deduce the most general type of an expression without requiring type annotations. If it cannot find a suitable type for an expression, its declaration must contain errors. Because type checking in \textit{ML} is secure, deduction of theroems is always sound. Wrong applications of rules lead to exceptions.
6.8 +\textit{Standard ML} makes use of {\em Hind\-ley-Mil\-ner type inference} \cite{milner1978theory} based on a type system for the lambda calculus which utilizes parametric polymorphism, i.e. types can be declared using type variables (e.g. \textit{Synchronized} signature on page \pageref{alg:guarded_access_sig}) and the decision on the instantiated types is left to the inference algorithm. This allows for the generic definition of functions while still ensuring static type safety. The type inference method is complete and is able to always deduce the most general type of an expression without requiring type annotations. If it cannot find a suitable type for an expression, its declaration must contain errors. Because type checking in \textit{ML} is secure, deduction of theorems is always sound. Wrong applications of rules lead to exceptions.
6.9
6.10 \bigskip
6.11
6.12 @@ -79,7 +79,7 @@
6.13 \label{sec:isabelleml}
6.14 \textit{Isabelle/ML} is a way of programming in \textit{Standard ML} which is encouraged and enhanced within the \isabelle{} infrastructure. It adds many library modules to plain \textit{Poly/ML}.
6.15
6.16 -\paragraph{Antiqutations.}\label{sec:antiquot}
6.17 +\paragraph{Antiquotations.}\label{sec:antiquot}
6.18 A very powerful mechanism for easy access to \isabelle{} system values and logical entities are so called {\em antiquotations} \cite{wenzel2013impl}. Depending on their particular purpose they are resolved at compile, link or run time. They can refer to various datatypes such as {\em theorems} (derived propositions), {\em theories} (containers for global declarations), {\em contexts} (deductive environment states) and many other concepts within the \isabelle{} framework. E.g. {\tt @\{context\}} would refer to the context at compile time at the location where it is used, i.e. a \textit{Standard ML} value of type {\tt context}.
6.19
6.20 \paragraph{Concurrency.}
6.21 @@ -114,13 +114,13 @@
6.22 \>val map: ('a -> 'b) -> 'a future -> 'b future\\
6.23 \>val value: 'a -> 'a future}
6.24 \noindent
6.25 -Notice that {\tt 'a} is a placeholder for an arbitrary type which a future can represent. Calls to {\tt Future.join} synchronize the evaluation and wait for the future's result if it is not already available. In case an exception is raised during the evaluation, its propagation will wait until the future is joined. {\tt Future.cancel} stops a future's evaluation if it has not finished, otherwise the function has no effect. The evaluation of futures is managed by means of tasks and worker threads. The number of workers should be related to the number of available processing cores. The exact number, however, is adjusted dynamically because the future scheduler always keeps a limited number of inactive threads in memory, such that they can immediately take over if another thread is temporarily stalled. In practice, the additional functions {\tt Future.map} and {\tt Future.value} have turned out to be useful in reducing the number of tasks and as a consequence the scheduling overhead. {\tt Future.map} can append another operation to an existing future, which will be executed on the originally scheduled function's result. If the original future's evaluation has not started yet, the appended operation will be computed within the same task. {\tt Future.value} produces a dummy future holding the function's argument as a result. Additionally, futures can be assigned priorities in order to influence execution order which by default is based on creation time. Also, futures can be organized in groups and even hierarchies of groups. This allows futures that depend on each other to be cancelled whenever one of them raises an exception.
6.26 +Notice that {\tt 'a} is a placeholder for an arbitrary type which a future can represent. Calls to {\tt Future.join} synchronize the evaluation and wait for the future's result if it is not already available. In case an exception is raised during the evaluation, its propagation will wait until the future is joined. {\tt Future.cancel} stops a future's evaluation if it has not finished, otherwise the function has no effect. The evaluation of futures is managed by means of tasks and worker threads. The number of workers should be related to the number of available processing cores. The exact number, however, is adjusted dynamically because the future scheduler always keeps a limited number of inactive threads in memory, such that they can immediately take over if another thread is temporarily stalled. In practice, the additional functions {\tt Future.map} and {\tt Future.value} have turned out to be useful in reducing the number of tasks and as a consequence the scheduling overhead. {\tt Future.map} can append another operation to an existing future, which will be executed on the originally scheduled function's result. If the original future's evaluation has not started yet, the appended operation will be computed within the same task. {\tt Future.value} produces a dummy future holding the function's argument as a result. Additionally, futures can be assigned priorities in order to influence execution order which by default is based on creation time. Also, futures can be organized in groups and even hierarchies of groups. This allows futures that depend on each other to be canceled whenever one of them raises an exception.
6.27
6.28 A simple {\em future} example has already been shown on page \pageref{alg:futures}. Internally, the {\em Futures} module is based on the guarded access mechanisms introduced above. Based on futures, \textit{Isabelle/ML} provides more specific parallel combinators such as the parallel list combinators {\tt map} and {\tt find}. The latter makes use of future groups and throws an exception as soon as a match is found, such that other search branches are not evaluated. This example shows how exceptions can be used as a basic means for functional interaction of futures without reintroducing the complexities usually associated with inter-process communication. See \cite{matthews2010efficient} for further details and a discussion of the performance of futures.
6.29
6.30 \subsection{\textit{Isabelle/Isar}}
6.31 \label{sec:isaisar}
6.32 -While in older versions of \isabelle{}, theorem proving tasks had to be solved using raw \textit{ML} tactic scripts, theories and proofs can now be developed interactively in an interpreted, structured, formal proof language called {\em Isar} (Intelligible semi-automated reasoning) \cite{wenzel2013isar,wenzel1999isar}. \textit{Isar} was designed to address an issue common to state-of-the-art theorem provers: Despite successfully formalising a good amount of existing mathematical knowledge, logics and computer science theory, it was still hard to reach potential target groups unfamiliar with the involved computer programming requirements. The primary users of theorem provers should be mathematicians and engineers who utilize them to formulate new proofs and for verification purposes. \textit{Isar} enables these users (``authors'' in fig. \ref{fig:isar-use}) to write proofs and theories in a way that can be understood by machines while being much closer to human language than \textit{ML} code or some logical calculus. As much as possible, it hides operational details thanks to its notion of {\em obvious inferences}. With a little extra care it can therefore also be used for presentation to an audience. The short, well-known proof that the square root of 2 is an irrational number is presented in appendix \ref{app:sqrt2-isar}.
6.33 +While in older versions of \isabelle{}, theorem proving tasks had to be solved using raw \textit{ML} tactic scripts, theories and proofs can now be developed interactively in an interpreted, structured, formal proof language called {\em Isar} (Intelligible semi-automated reasoning) \cite{wenzel2013isar,wenzel1999isar}. \textit{Isar} was designed to address an issue common to state-of-the-art theorem provers: Despite successfully formalizing a good amount of existing mathematical knowledge, logics and computer science theory, it was still hard to reach potential target groups unfamiliar with the involved computer programming requirements. The primary users of theorem provers should be mathematicians and engineers who utilize them to formulate new proofs and for verification purposes. \textit{Isar} enables these users (``authors'' in fig. \ref{fig:isar-use}) to write proofs and theories in a way that can be understood by machines while being much closer to human language than \textit{ML} code or some logical calculus. As much as possible, it hides operational details thanks to its notion of {\em obvious inferences}. With a little extra care it can therefore also be used for presentation to an audience. The short, well-known proof that the square root of 2 is an irrational number is presented in appendix \ref{app:sqrt2-isar}.
6.34
6.35 \begin{figure}
6.36 \centering
6.37 @@ -148,7 +148,7 @@
6.38 \>private case class Variable(val name: String) extends Elem\\
6.39 \>private case object Parent extends Elem}
6.40 \noindent
6.41 -The internal protocol utilizes \textit{YXML}, a transfer format based on XML \cite{wenzel2011isabelle}. Instead of keeping a public protocol specification, the details are being kept private. This allows the developers to make substantial changes to protocol and document model to improve robustness and performance without further ado. Instead, both \textit{Isabelle/ML} and \textit{Isabelle/Scala} offer public, static APIs for their communictaion which are maintained and kept simple and stable.
6.42 +The internal protocol utilizes \textit{YXML}, a transfer format based on XML \cite{wenzel2011isabelle}. Instead of keeping a public protocol specification, the details are being kept private. This allows the developers to make substantial changes to protocol and document model to improve robustness and performance without further ado. Instead, both \textit{Isabelle/ML} and \textit{Isabelle/Scala} offer public, static APIs for their communication which are maintained and kept simple and stable.
6.43
6.44 \begin{figure}
6.45 \centering
6.46 @@ -169,7 +169,7 @@
6.47
6.48 \subsection{\textit{Isabelle/jEdit}}
6.49 \label{ssec:isa-jedit}
6.50 -Recent \isabelle{} distributions include a complete prover IDE prototype implementation based on the text editor framework {\em jEdit} \cite{wenzel2012isabelle}. \textit{Isabelle/jEdit} features a completely new interaction model that performs continuous, parallel proof checking. It uses GUI functionalities such as highlighting, coloring, tooltips, popup windows and hyperlinks to annotate user code written in \textit{Isar} and \textit{ML} incrementally with semantic information from the prover (see fig. \ref{fig:jedit_feedback}). Prover and editor front-end are executed independently and never block each other thanks to the asynchronous protocol. Additionally, \textit{Isabelle/jEdit} includes several plugins and fonts to facilitate entering and rendering of mathematical symbols.
6.51 +Recent \isabelle{} distributions include a complete prover IDE prototype implementation based on the text editor framework {\em jEdit} \cite{wenzel2012isabelle}. \textit{Isabelle/jEdit} features a completely new interaction model that performs continuous, parallel proof checking. It uses GUI functionality such as highlighting, coloring, tooltips, popup windows and hyperlinks to annotate user code written in \textit{Isar} and \textit{ML} incrementally with semantic information from the prover (see fig. \ref{fig:jedit_feedback}). Prover and editor front-end are executed independently and never block each other thanks to the asynchronous protocol. Additionally, \textit{Isabelle/jEdit} includes several plugins and fonts to facilitate entering and rendering of mathematical symbols.
6.52
6.53 \begin{figure}
6.54 \centering
6.55 @@ -238,7 +238,7 @@
6.56 \item\label{enum:isa-repos}{\bf The repository}, publicly readable \cite{tum2014repo} is the third pillar for documentation. Commits must follow a {\em minimal changeset} policy which allows for quick queries and documents particular interdependencies across several files. This kind of documentation of complicated connections is very efficient and always up to date even with frequent changes.
6.57 \end{enumerate}
6.58 \noindent
6.59 -This documentation model has evolved during more than two decades and still allows for ongoing rapid development with invasive changes, last but not least parallelization. However, relevant documenation for this thesis is marginal. Parallelization, as already mentioned, has been done by Makarius Wenzel and was preceeded by a feasibility study conducted by a master student \cite{haller2006object}. Wenzel's respective papers \cite{matthews2010efficient,wenzel1999isar,wenzel2012asynchronous, wenzel2011isabelle,wenzel2012isabelle} concern fundamental considerations. The most relevant reference manual \cite{wenzel2013impl} contains less than ten pages on parallelization. All the rest had to be found in the code (several hundred thousand LOCs\footnote{{\em lines of code}}). The gap between papers and code was hard to bridge.
6.60 +This documentation model has evolved during more than two decades and still allows for ongoing rapid development with invasive changes, last but not least parallelization. However, relevant documentation for this thesis is marginal. Parallelization, as already mentioned, has been done by Makarius Wenzel and was preceded by a feasibility study conducted by a master student \cite{haller2006object}. Wenzel's respective papers \cite{matthews2010efficient,wenzel1999isar,wenzel2012asynchronous, wenzel2011isabelle,wenzel2012isabelle} concern fundamental considerations. The most relevant reference manual \cite{wenzel2013impl} contains less than ten pages on parallelization. All the rest had to be found in the code (several hundred thousand LOCs\footnote{{\em lines of code}}). The gap between papers and code was hard to bridge.
6.61
6.62 \subsection{Reasons for Parallelism in \isabelle{}}
6.63 \label{ssec:isab-parallel}
6.64 @@ -248,7 +248,7 @@
6.65 \isabelle{}'s collection of automated provers was mentioned in section \ref{sec:isaatp}. It still has a mechanism to connect with remote prover instances and these already featured parallel access to external resources. Since personal computers and laptops have become powerful enough to run \isabelle{}, this hardware has also become powerful enough to run automated provers. But running them in parallel on a local machine required a redesign.
6.66
6.67 \subsubsection{Provide a Tool Usable in Engineering Practice}
6.68 -The paragraph about {\em Continuous Pentration of Computer Science} by formal methods in section \ref{par:invade-cs} (page \pageref{par:invade-cs}) mentioned the increasing demand for theorem provers in the practice of software engineering and related mathematics. In particular, software engineers are used to comprehensive support by integrated development environments (IDEs): interlinked code, various views on relations between code elements, etc. Since TPs have been used by experts only until the presence, specific user interfaces were sufficient. For \isabelle{} this was {\em Proof General} (see section \ref{ssec:isa-jedit}), which is based on \textit{Emacs}. Those who still use this editor which was dominant during the last decades, know how different \textit{Emacs} is: not reasonable for engineering practice of today. So the issue was to meet the usability requirements of contemporary engineering practice. \isabelle{}'s attempt to meet such requirements is the {\em PIDE} project (section \ref{ssec:isa-scala}). \textit{Isabelle/jEdit} (section \ref{ssec:isa-jedit}) is the reference implementation, which is accompanied by development of an \textit{Eclipse} plugin \cite{andriusvelykis2013isaclipse} and a browser-based front-end under construction.
6.69 +The paragraph about {\em Continuous Penetration of Computer Science} by formal methods in section \ref{par:invade-cs} (page \pageref{par:invade-cs}) mentioned the increasing demand for theorem provers in the practice of software engineering and related mathematics. In particular, software engineers are used to comprehensive support by integrated development environments (IDEs): interlinked code, various views on relations between code elements, etc. Since TPs have been used by experts only until the presence, specific user interfaces were sufficient. For \isabelle{} this was {\em Proof General} (see section \ref{ssec:isa-jedit}), which is based on \textit{Emacs}. Those who still use this editor which was dominant during the last decades, know how different \textit{Emacs} is: not reasonable for engineering practice of today. So the issue was to meet the usability requirements of contemporary engineering practice. \isabelle{}'s attempt to meet such requirements is the {\em PIDE} project (section \ref{ssec:isa-scala}). \textit{Isabelle/jEdit} (section \ref{ssec:isa-jedit}) is the reference implementation, which is accompanied by development of an \textit{Eclipse} plugin \cite{andriusvelykis2013isaclipse} and a browser-based front-end under construction.
6.70
6.71 \subsubsection{Accelerate theory evaluation}
6.72 My supervisor's first experience with \isabelle{} was about fifteen years ago on a high-end SPARK workstation. The initial evaluation of \textit{Isabelle/HOL} took more than twenty minutes; not to speak of the considerable amount of time an experienced system administrator needed for installation. Since this time \textit{Isabelle/HOL} has become about three times larger, but the initial evaluation of theories takes about two minutes for recent \isabelle{} releases. \textit{Isabelle/jEdit} represents theory evaluation as shown in fig. \ref{fig:jedit_thy} on page \pageref{fig:jedit_thy}. Parallel branches in the dependency graph are evaluated in parallel. Without this kind of speedup, large theory developments involving several dozens of theories would not be manageable. The most recent \isabelle{} releases do not package binaries of evaluated theories any more. Instead, they pack further components into the bundle. The bundle of the current release is more than 400MB for download. Also, all other bandwidth aspects of \isabelle{} are at the limits of present mainstream hardware. \isabelle{} does not run below 4GB main memory and requires a dual-core processor with more than 2GHz per core.
6.73 @@ -286,7 +286,7 @@
6.74 \noindent
6.75 These three features together establish a powerful interface to the mathe\-matics-engine. With these given, interaction can be analogous to learning how to play chess in interaction with a chess program. The player executes a move (the student inputs a formula) and the program checks the correctness of the move (\isac{} checks the input). The program performs a move (\isac{} proposes a next step) and the player accepts or changes it. If the player is in danger of losing the game (the student gets stuck within the steps towards a problem solution), they can go back a few moves and try alternative moves. Or the player can even switch roles with the system and watch how the system copes with the unfortunate configuration. All these choices are available to a student analogously when learning mathematics in interaction with \isac.
6.76
6.77 -The comparison of interaction in \isac{} with interaction in playing chess makes clear, that learning with a mechanical system does not necessarily lead to drill and practice in operational mechanisation. The degree of freedom in interaction allows for fostering of the evaluation of alternatives and thus learning by trial and error, comparing strategies, etc.
6.78 +The comparison of interaction in \isac{} with interaction in playing chess makes clear, that learning with a mechanical system does not necessarily lead to drill and practice in operational mechanization. The degree of freedom in interaction allows for fostering of the evaluation of alternatives and thus learning by trial and error, comparing strategies, etc.
6.79
6.80 \subsection{Architecture Separating Mathematics and Dialogs}
6.81 \label{ssec:isac-archi}
6.82 @@ -364,7 +364,7 @@
6.83 \item\label{enum:pbl}{\bf Application-oriented knowledge} is given by formal specifications of problems in applied mathematics. The specification of all problems, which can be solved automatically by \isac{} (with the help of algorithms, see below), is available online \cite{isac2014pbl}.
6.84 This collection is structured as a tree. Given a tree, automated problem refinement is possible, e.g. starting from the specification at the node of {\em univariate equations} \cite{isac2014pblequuniv} a certain equation can be matched with all child nodes until the appropriate type of equation has been identified. In case a match has been found, such a node contains a pointer to a program solving the specific type of equation.
6.85 This kind of problem refinement makes transparent, what is done by computer algebra systems as black boxes.
6.86 -\item\label{enum:met}{\bf Algorithmic knowledge} is given by programs to undergo \textit{Lucas-Interpretation}. The collection of programs is structured as a tree. However, principal requirements on the structure are still unclear. There are ideas of how to group algorithms in \cite{buchberger1984mathematik} but the ideas are too vague for mechanisation. \isac's programs can be found online \cite{isac2014met}.
6.87 +\item\label{enum:met}{\bf Algorithmic knowledge} is given by programs to undergo \textit{Lucas-Interpretation}. The collection of programs is structured as a tree. However, principal requirements on the structure are still unclear. There are ideas of how to group algorithms in \cite{buchberger1984mathematik} but the ideas are too vague for mechanization. \isac's programs can be found online \cite{isac2014met}.
6.88 \end{enumerate}
6.89 The structure of the knowledge collections of pt. \ref{enum:pbl} and \ref{enum:met} are different from pt. \ref{enum:thy}. E.g. linear equations in pt. \ref{enum:pbl} are the same for rational numbers and complex numbers, but the definition of rationals is far away from complex numbers in pt. \ref{enum:thy}.
6.90 So the implementation of the latter two collections is orthogonal to the first, the collection structured and managed by \isabelle{}. The only way of implementation was by {\tt Unsynchronized.ref}, i.e. by global references. Write access to these references assumed a certain sequence in evaluation of the theories. This assumption broke with the introduction of parallel execution in \isabelle{}. Section \ref{ssec:parall-thy} explains how this issue was resolved.
6.91 @@ -400,7 +400,7 @@
6.92
6.93 \paragraph{Adopt \textit{Isabelle/jEdit} for \isac{}.}
6.94 \isac's initial design also stressed usability of the front-end for students. At this time \isabelle{}'s front-end was {\em Proof General} \cite{aspinall2000proof}. Thus there was no choice but to develop a custom GUI for \isac{}.
6.95 -In the meantime \textit{Isabelle/jEdit} has become an appealing prover IDE. However, the requirements are presently quite opposing. \isabelle{} connects one engineer with a multitude of cores while \isac{} connects a multitude of students with one server. \isac's centralised structure has good reasons: groups of students have one lecturer, groups of students are examined together, etc.
6.96 +In the meantime \textit{Isabelle/jEdit} has become an appealing prover IDE. However, the requirements are presently quite opposing. \isabelle{} connects one engineer with a multitude of cores while \isac{} connects a multitude of students with one server. \isac's centralized structure has good reasons: groups of students have one lecturer, groups of students are examined together, etc.
6.97 During the next years, \isac{}'s front-end will be developed and improved independently from \isabelle{}. Narrowing towards \isabelle{} can start as soon as \textit{Isabelle/jEdit} moves towards collaborative work, implements session management, version management, etc.
6.98
6.99 \subsubsection{Summary on \isac's Approach to \isabelle{}}
6.100 @@ -421,14 +421,14 @@
6.101
6.102 \bigskip
6.103
6.104 -The last sections have outlined the conceptual and architectural differences between \isabelle{} and \isac{}. \isac{} needs to manage application-oriented and algorithmic knowledge which originally could not be integrated with the deductive structure of \isabelle{}'s theories. Therefore these data were stored in raw ML references. {\em Isabelle2009} then introduced parallelism. Now the computation order of the theories was not deterministic anymore and \isac{} could not ensure that its \textit{ML} references were accessed and updated in the same order as previously. This caused certain parts of the system to show faulty behavior in some cases. {\em Isabelle2009-1} then added the wrapper structure {\tt Unsychronized.ref} to denote that these references are not synchronized with the parallel environment managed by \isabelle{}.
6.105 +The last sections have outlined the conceptual and architectural differences between \isabelle{} and \isac{}. \isac{} needs to manage application-oriented and algorithmic knowledge which originally could not be integrated with the deductive structure of \isabelle{}'s theories. Therefore these data were stored in raw ML references. {\em Isabelle2009} then introduced parallelism. Now the computation order of the theories was not deterministic anymore and \isac{} could not ensure that its \textit{ML} references were accessed and updated in the same order as previously. This caused certain parts of the system to show faulty behavior in some cases. {\em Isabelle2009-1} then added the wrapper structure {\tt Unsynchronized.ref} to denote that these references are not synchronized with the parallel environment managed by \isabelle{}.
6.106 While the temporary deactivation of faulty modules and certain work\-arounds fixed most problems, the parallelization of \isac{}'s user session management required that most relevant data be properly managed by \isabelle{}. Therefore the preparatory step for the parallelization was the integration of the unsynchronized references in question with \isabelle{} by means of the functor {\tt Theory\_Data} \cite{wenzel2013impl}.
6.107 It is important to mention that the \isabelle{} implementation manual \cite{wenzel2013impl} warns to be careful about using too many datastructures on the basis of {\tt Theory\_Data} because they are newly initialized for every single theory that derives from the respective module that declared the datastructures. Thus, space is reserved which can cause a significantly increased memory footprint. Most of the overhead, however, occurs when theories are loaded dynamically. When working with a compiled \isac{} system the overhead should be reasonable.
6.108
6.109 The workflow was implemented for several central elements and broken down into five isolated steps to conform with \isabelle{}'s minimal changeset development and documentation model (section \ref{sec:isadevdoc}):
6.110 \begin{enumerate}
6.111 - \item\label{enum:isolate} {\bf Isolate access.} In this step, read accesses were centralized by wrapping references in an access function and replacing all occurences with a call to the function:
6.112 -\imlcode{~~\=val foo = Unsychronized.ref [1,2,3]; (*declaration*)\\
6.113 + \item\label{enum:isolate} {\bf Isolate access.} In this step, read accesses were centralized by wrapping references in an access function and replacing all occurrences with a call to the function:
6.114 +\imlcode{~~\=val foo = Unsynchronized.ref [1,2,3]; (*declaration*)\\
6.115 \>fun get\_foo () = !foo; (*new*)\\
6.116 \>fun add x y = x + y;\\
6.117 \>fun foo\_sum () = fold add (!foo) 0; (*obsolete*)\\
6.118 @@ -455,7 +455,7 @@
6.119 is more flexible in that {\tt get\_foo'} operates on a reference theory set by the programmer (details on {\tt get\_ref\_thy} are explained in the subsequent section) and passes it to {\tt get\_foo'} from above. The last aspect of this step is the addition of {\bf setup} blocks \cite{wenzel2013isar} where previously the raw references had been updated. These blocks must contain one \textit{ML} expression which represents a mapping between two {\tt theory}s. As a consequence, \isabelle{} updates the current theory context with the function's result in these locations, e.g.
6.120 \imlcode{~~setup \{* put\_foo' [4,5,6] *\} \textit{.}}
6.121
6.122 - \item\label{enum:checkdiff} {\bf Check differences.} Now that both, the old unsychronized reference and the new stored as theory data, are created and updated, we can compare their contents and make sure that the last steps were successful. Due to the nature of the datastructures and the fact that the new method caused a different ordering to some of the elements, the most convenient solution was to compute a string representation from both results, write them into documents and compare the documents using a file comparison utility. If any errors occurred, step \ref{enum:isolate} and \ref{enum:addthydata} required revision.
6.123 + \item\label{enum:checkdiff} {\bf Check differences.} Now that both, the old unsynchronized reference and the new stored as theory data, are created and updated, we can compare their contents and make sure that the last steps were successful. Due to the nature of the datastructures and the fact that the new method caused a different ordering to some of the elements, the most convenient solution was to compute a string representation from both results, write them into documents and compare the documents using a file comparison utility. If any errors occurred, step \ref{enum:isolate} and \ref{enum:addthydata} required revision.
6.124
6.125 \item\label{enum:shiftthydata} {\bf Shift to theory data.} Optimally, this step merely meant exchanging the old definition of {\tt get\_foo} (pt. \ref{enum:isolate}) for the new one (pt. \ref{enum:addthydata}).
6.126
6.127 @@ -465,7 +465,7 @@
6.128
6.129 Besides acquiring the necessary knowledge on how to store and access arbitrary datastructures in a theory's context, the biggest challenges included understanding and merging the different kinds of custom datastructures and keeping the solutions simple; optimally simpler than the previous code. Also, I had to adjust the theory hierarchy and add new theories in order to keep a clean structure and ensure that the availability and computation of datastructures was sound and behaved as it had previously. Some of the data dependencies had not been reflected in the dependency graph but had rather been fulfilled by a fortunate execution order.
6.130
6.131 -As a result of this contribution, most of the stateful compontents in \isac{}, which had been necessary to circumvent mismatches between \isac{}'s and \isabelle{}'s architectures, were eradicated from the system. Those which are still not synchronized are currently being replaced. However, they are not accessed by theories pontentially executed in parallel and therefore do not interfere with \isac{}'s parallel user session management.
6.132 +As a result of this contribution, most of the stateful components in \isac{}, which had been necessary to circumvent mismatches between \isac{}'s and \isabelle{}'s architectures, were eradicated from the system. Those which are still not synchronized are currently being replaced. However, they are not accessed by theories potentially executed in parallel and therefore do not interfere with \isac{}'s parallel user session management.
6.133
6.134 % calcelems.sml:839
6.135 % merge tree into another tree (not bidirectional!)
6.136 @@ -580,7 +580,7 @@
6.137 \end{figure}
6.138
6.139 \subsubsection{Discussion}
6.140 -From these results it is evident, that two parallel calculations can almost fully exploit both physical processing cores. The slight increase of processing time can be explained by a parallelization overhead caused by \isabelle{}'s future management. Another factor are the synchronized accesses to the {\tt states} datastructure. Since simultanteous multithreading cannot completely simulate additional cores, the increase in runtime between two and three parallel calculations is then sligtly bigger. The same happens between six and seven parallel {\tt autoCaclulate} invocations. As the number of logical cores of the used machine is four, multiples of four show a significant increase in runtime because once all cores are occupied, additional calculations need to wait. Hence, the execution time accurately doubles with the number of calculations according to the number of cores. The measured runtime of the new {\tt autoCalculate} version was only $38.7\%$ of the previous, sequential implementation with eight parallel calculations, $39.8\%$ with ten and $39.7\%$ with twelve. This is a very satisfying outcome and we trust that it will help to significantly improve the end user experience and enable \isac{} servers to deal with a high number of clients simultaneously.
6.141 +From these results it is evident, that two parallel calculations can almost fully exploit both physical processing cores. The slight increase of processing time can be explained by a parallelization overhead caused by \isabelle{}'s future management. Another factor are the synchronized accesses to the {\tt states} datastructure. Since simultaneous multithreading cannot completely simulate additional cores, the increase in runtime between two and three parallel calculations is then slightly bigger. The same happens between six and seven parallel {\tt autoCalculate} invocations. As the number of logical cores of the used machine is four, multiples of four show a significant increase in runtime because once all cores are occupied, additional calculations need to wait. Hence, the execution time accurately doubles with the number of calculations according to the number of cores. The measured runtime of the new {\tt autoCalculate} version was only $38.7\%$ of the previous, sequential implementation with eight parallel calculations, $39.8\%$ with ten and $39.7\%$ with twelve. This is a very satisfying outcome and we trust that it will help to significantly improve the end user experience and enable \isac{} servers to deal with a high number of clients simultaneously.
6.142
6.143 \subsection{Project Status}
6.144 \label{sec:proj-stat}
7.1 --- a/master/thesis/literature.bib Thu Jun 26 02:58:44 2014 +0200
7.2 +++ b/master/thesis/literature.bib Sun Jul 20 16:31:11 2014 +0200
7.3 @@ -1,7 +1,7 @@
7.4
7.5 @article{moore1965cramming,
7.6 title={{Cramming More Components onto Integrated Circuits}},
7.7 - author={Moore, Gordon E},
7.8 + author={Moore, Gordon E.},
7.9 year={1965},
7.10 journal={Electronics},
7.11 pages = {114--117},
7.12 @@ -51,10 +51,12 @@
7.13 }
7.14
7.15 @book{burge1975recursive,
7.16 - title={Recursive programming techniques},
7.17 - author={Burge, William H},
7.18 + title={Recursive Programming Techniques},
7.19 + author={Burge, William H.},
7.20 year={1975},
7.21 - publisher={Addison-Wesley Reading}
7.22 + isbn = {0201144506},
7.23 + publisher={Addison-Wesley},
7.24 +
7.25 }
7.26
7.27 @book{paulson1994isabelle,
7.28 @@ -347,7 +349,7 @@
7.29
7.30 @article{moore2008multicore,
7.31 title={Multicore is bad news for supercomputers},
7.32 - author={Moore, Samuel K},
7.33 + author={Moore, Samuel K.},
7.34 journal={Spectrum, IEEE},
7.35 volume={45},
7.36 number={11},
7.37 @@ -455,7 +457,7 @@
7.38 }
7.39
7.40 @inproceedings{nocker1991concurrent,
7.41 - author = {N\"{o}cker, E. G. J. M. H. and Smesters, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.},
7.42 + author = {N\"{o}cker, Eric and Smesters, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.},
7.43 title = {Concurrent Clean},
7.44 booktitle = {Proceedings on Parallel Architectures and Languages Europe: Volume II: Parallel Languages},
7.45 series = {PARLE '91},
7.46 @@ -576,7 +578,7 @@
7.47 }
7.48
7.49 @inproceedings{matthews2010efficient,
7.50 - author = {Matthews, David C.J. and Wenzel, Makarius},
7.51 + author = {Matthews, David C. J. and Wenzel, Makarius},
7.52 title = {Efficient Parallel Programming in Poly/ML and Isabelle/ML},
7.53 booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming},
7.54 series = {DAMP '10},
7.55 @@ -672,7 +674,7 @@
7.56
7.57 @patent{zhang2010software,
7.58 title={Software Transaction Commit Order and Conflict Management},
7.59 - author={Zhang, L. and Grover, V.K. and Magruder, M.M. and Detlefs, D. and Duffy, J.J. and Graefe, G.},
7.60 + author={Zhang, Lingli and Grover, Vinod K. and Magruder, Michael M. and Detlefs, David and Duffy, John J. and Graefe, Goetz},
7.61 url={http://www.google.co.in/patents/US7711678},
7.62 year={2010},
7.63 month={5},
7.64 @@ -767,7 +769,7 @@
7.65 }
7.66
7.67 @article{agha1997foundation,
7.68 - author = {Gul Agha and
7.69 + author = {Gul A. Agha and
7.70 Ian A. Mason and
7.71 Scott F. Smith and
7.72 Carolyn L. Talcott},
7.73 @@ -790,7 +792,7 @@
7.74 }
7.75
7.76 @inproceedings{karmani2009actor,
7.77 - author = {Karmani, Rajesh K. and Shali, Amin and Agha, Gul},
7.78 + author = {Karmani, Rajesh K. and Shali, Amin and Agha, Gul A.},
7.79 title = {Actor Frameworks for the JVM Platform: A Comparative Analysis},
7.80 booktitle = {Proceedings of the 7th International Conference on Principles and Practice of Programming in Java},
7.81 series = {PPPJ '09},
7.82 @@ -823,7 +825,7 @@
7.83
7.84 @article{panwar1994methodology,
7.85 author = {Rajendra Panwar and
7.86 - Gul Agha},
7.87 + Gul A. Agha},
7.88 title = {A Methodology for Programming Scalable Architectures},
7.89 journal = {Journal of Parallel and Distributed Computing},
7.90 volume = {22},
7.91 @@ -1142,12 +1144,12 @@
7.92 @online{matthews2014documentation,
7.93 url={http://polyml.org/Doc.html},
7.94 title={Documentation},
7.95 - author={Matthews, David C.J.},
7.96 + author={Matthews, David C. J.},
7.97 year={2014-05-15}
7.98 }
7.99
7.100 @techreport{matthews1995papers,
7.101 - author = {Matthews, David CJ},
7.102 + author = {Matthews, David C. J.},
7.103 title = {{Papers on Poly/ML}},
7.104 year = {1989},
7.105 month = {feb},
7.106 @@ -1156,7 +1158,7 @@
7.107
7.108 @techreport{matthews1991distributed,
7.109 title={A Distributed Concurrent Implementation of Standard ML},
7.110 - author={Matthews, David CJ},
7.111 + author={Matthews, David C. J.},
7.112 year={1991},
7.113 institution={LFCS, Department of Computer Science, University of Edinburgh}
7.114 }
7.115 @@ -1529,7 +1531,7 @@
7.116
7.117 @book{simon1965shape,
7.118 address = {New York},
7.119 - author = {Simon, H. A.},
7.120 + author = {Simon, Herbert A.},
7.121 publisher = {Harper \& Row},
7.122 title = {{The Shape of Automation for Men and Management}},
7.123 year = {1965}
7.124 @@ -1537,9 +1539,10 @@
7.125
7.126 @book{gordon1993introduction,
7.127 title={Introduction to HOL: A theorem proving environment for higher-order logic},
7.128 - author={Gordon, Michael JC and Melham, Tom F},
7.129 + author={Michael J. C. Gordon and Melham, Tom F.},
7.130 year={1993},
7.131 - publisher={Cambridge University Press}
7.132 + publisher={Cambridge University Press},
7.133 + isbn={0521441897}
7.134 }
7.135
7.136 @online{harrison2014hol,
7.137 @@ -1567,14 +1570,14 @@
7.138 title={Historical Overview of the Kepler Conjecture},
7.139 url={http://dx.doi.org/10.1007/978-1-4614-1129-1_3},
7.140 publisher={Springer New York},
7.141 - author={Hales, ThomasC.},
7.142 + author={Hales, Thomas C.},
7.143 pages={65-82},
7.144 language={English}
7.145 }
7.146
7.147 @techreport{sharangpani1994statistical,
7.148 title={Statistical Analysis of Floating Point Flaw in the Pentium Processor},
7.149 - author={Sharangpani, HP and Barton, ML},
7.150 + author={Sharangpani, H. P. and Barton, M. L.},
7.151 institution={Intel Corporation},
7.152 year={1994}
7.153 }
8.1 --- a/master/thesis/preface.tex Thu Jun 26 02:58:44 2014 +0200
8.2 +++ b/master/thesis/preface.tex Sun Jul 20 16:31:11 2014 +0200
8.3 @@ -9,7 +9,7 @@
8.4
8.5 Walther Neuper's enthusiasm for his project and his eager cooperation and supervision were extremely motivating and made the whole process of creating this thesis very efficient. His gentle and wise personality and his trust in me were very encouraging.
8.6
8.7 -I owe my great appreciation to Volker Christian for his friendly personal and competent, professional supervision and his interest in my topic. I am overly thankful for his trust, support and encouragement to persue my interests.
8.8 +I owe my great appreciation to Volker Christian for his friendly personal and competent, professional supervision and his interest in my topic. I am overly thankful for his trust, support and encouragement to pursue my interests.
8.9
8.10 \bigskip
8.11 \bigskip