62 \subsubsection{\textit{Standard ML}} |
62 \subsubsection{\textit{Standard ML}} |
63 \label{sec:isasml} |
63 \label{sec:isasml} |
64 \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. |
64 \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. |
65 |
65 |
66 \paragraph{The Hind\-ley-Mil\-ner Type System.}\label{sec:hindleymilner} |
66 \paragraph{The Hind\-ley-Mil\-ner Type System.}\label{sec:hindleymilner} |
67 \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. |
67 \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. |
68 |
68 |
69 \bigskip |
69 \bigskip |
70 |
70 |
71 Another important feature of \textit{Standard ML} is its design for robust, large scale, modular software. Signatures are part of the type system and describe the interfaces between different modules. |
71 Another important feature of \textit{Standard ML} is its design for robust, large scale, modular software. Signatures are part of the type system and describe the interfaces between different modules. |
72 |
72 |
77 |
77 |
78 \subsubsection{\textit{Isabelle/ML}} |
78 \subsubsection{\textit{Isabelle/ML}} |
79 \label{sec:isabelleml} |
79 \label{sec:isabelleml} |
80 \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}. |
80 \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}. |
81 |
81 |
82 \paragraph{Antiqutations.}\label{sec:antiquot} |
82 \paragraph{Antiquotations.}\label{sec:antiquot} |
83 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}. |
83 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}. |
84 |
84 |
85 \paragraph{Concurrency.} |
85 \paragraph{Concurrency.} |
86 \textit{Poly/ML} comes with very general mechanisms for concurrency. Its approach is based on shared resources and synchronized access. While this concurrency model is well established, it is easy for the programmer to overlook some detail in the coordination of threads and deadlocks can occur. In order to ensure correctness by design, \textit{Isabelle/ML} provides higher-order combinators and thereby hides synchronization details. |
86 \textit{Poly/ML} comes with very general mechanisms for concurrency. Its approach is based on shared resources and synchronized access. While this concurrency model is well established, it is easy for the programmer to overlook some detail in the coordination of threads and deadlocks can occur. In order to ensure correctness by design, \textit{Isabelle/ML} provides higher-order combinators and thereby hides synchronization details. |
87 |
87 |
112 \>val is\_finished: 'a future -> bool\\ |
112 \>val is\_finished: 'a future -> bool\\ |
113 \>val join: 'a future -> 'a\\ |
113 \>val join: 'a future -> 'a\\ |
114 \>val map: ('a -> 'b) -> 'a future -> 'b future\\ |
114 \>val map: ('a -> 'b) -> 'a future -> 'b future\\ |
115 \>val value: 'a -> 'a future} |
115 \>val value: 'a -> 'a future} |
116 \noindent |
116 \noindent |
117 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. |
117 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. |
118 |
118 |
119 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. |
119 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. |
120 |
120 |
121 \subsection{\textit{Isabelle/Isar}} |
121 \subsection{\textit{Isabelle/Isar}} |
122 \label{sec:isaisar} |
122 \label{sec:isaisar} |
123 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}. |
123 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}. |
124 |
124 |
125 \begin{figure} |
125 \begin{figure} |
126 \centering |
126 \centering |
127 \def\svgwidth{18.5em} |
127 \def\svgwidth{18.5em} |
128 \resizebox{.5\textwidth}{!}{\input{images/isar_use.pdf_tex}} |
128 \resizebox{.5\textwidth}{!}{\input{images/isar_use.pdf_tex}} |
146 \>private case class Root(val name: String) extends Elem\\ |
146 \>private case class Root(val name: String) extends Elem\\ |
147 \>private case class Basic(val name: String) extends Elem\\ |
147 \>private case class Basic(val name: String) extends Elem\\ |
148 \>private case class Variable(val name: String) extends Elem\\ |
148 \>private case class Variable(val name: String) extends Elem\\ |
149 \>private case object Parent extends Elem} |
149 \>private case object Parent extends Elem} |
150 \noindent |
150 \noindent |
151 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. |
151 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. |
152 |
152 |
153 \begin{figure} |
153 \begin{figure} |
154 \centering |
154 \centering |
155 \def\svgwidth{17.5em} |
155 \def\svgwidth{17.5em} |
156 \resizebox{.6\textwidth}{!}{\bf\input{images/pide_comm.pdf_tex}} |
156 \resizebox{.6\textwidth}{!}{\bf\input{images/pide_comm.pdf_tex}} |
167 % Walther mail 24.04. "Fwd: [isabelle-dev] scala-2.11.0" (scala actors) |
167 % Walther mail 24.04. "Fwd: [isabelle-dev] scala-2.11.0" (scala actors) |
168 % isabelle-doc.pdf (YXML) |
168 % isabelle-doc.pdf (YXML) |
169 |
169 |
170 \subsection{\textit{Isabelle/jEdit}} |
170 \subsection{\textit{Isabelle/jEdit}} |
171 \label{ssec:isa-jedit} |
171 \label{ssec:isa-jedit} |
172 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. |
172 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. |
173 |
173 |
174 \begin{figure} |
174 \begin{figure} |
175 \centering |
175 \centering |
176 \includegraphics[width=94mm]{jedit_feedback} %width=.95\textwidth |
176 \includegraphics[width=94mm]{jedit_feedback} %width=.95\textwidth |
177 \caption{GUI feedback in \textit{Isabelle/jEdit}.} |
177 \caption{GUI feedback in \textit{Isabelle/jEdit}.} |
236 \item{\bf The code} itself, without any further comments except in few specific cases. This is common to functional programming and very different from what one is used to from e.g. \textit{Javadoc}. The code can be inspected in the repository, see pt. \ref{enum:isa-repos} below. |
236 \item{\bf The code} itself, without any further comments except in few specific cases. This is common to functional programming and very different from what one is used to from e.g. \textit{Javadoc}. The code can be inspected in the repository, see pt. \ref{enum:isa-repos} below. |
237 \item\label{enum:isa-man}{\bf Reference manuals and tutorials}, which can be found online \cite{tum2013isadoc} and are easily accessible from \textit{Isabelle/jEdit} (section \ref{ssec:isa-jedit}). Both, manuals and tutorials are automatically held in sync with the code by specifically developed mechanisms such as antiquotations (section \ref{sec:bigisaml}, page \pageref{sec:antiquot}), e.g. {\tt @\{type \dots\}}, {\tt @\{const \dots\}}, etc. These entries in the documentation raise exceptions in case some type or constant has changed in the code. |
237 \item\label{enum:isa-man}{\bf Reference manuals and tutorials}, which can be found online \cite{tum2013isadoc} and are easily accessible from \textit{Isabelle/jEdit} (section \ref{ssec:isa-jedit}). Both, manuals and tutorials are automatically held in sync with the code by specifically developed mechanisms such as antiquotations (section \ref{sec:bigisaml}, page \pageref{sec:antiquot}), e.g. {\tt @\{type \dots\}}, {\tt @\{const \dots\}}, etc. These entries in the documentation raise exceptions in case some type or constant has changed in the code. |
238 \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. |
238 \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. |
239 \end{enumerate} |
239 \end{enumerate} |
240 \noindent |
240 \noindent |
241 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. |
241 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. |
242 |
242 |
243 \subsection{Reasons for Parallelism in \isabelle{}} |
243 \subsection{Reasons for Parallelism in \isabelle{}} |
244 \label{ssec:isab-parallel} |
244 \label{ssec:isab-parallel} |
245 \isabelle{} is the first theorem prover which is able to exploit multi-core hardware. The reasons for introducing parallelism in \isabelle{} are directed towards the future and complement considerations discussed for functional programming. There are three motivations for parallelization mentioned for \isabelle{}. They have all been addressed at once: parallel invocation of multiple automated provers, a responsive prover IDE and efficient theory evaluation envisage better usability in engineering practice. All three development issues are successfully being tackled, an end cannot be foreseen yet. |
245 \isabelle{} is the first theorem prover which is able to exploit multi-core hardware. The reasons for introducing parallelism in \isabelle{} are directed towards the future and complement considerations discussed for functional programming. There are three motivations for parallelization mentioned for \isabelle{}. They have all been addressed at once: parallel invocation of multiple automated provers, a responsive prover IDE and efficient theory evaluation envisage better usability in engineering practice. All three development issues are successfully being tackled, an end cannot be foreseen yet. |
246 |
246 |
247 \subsubsection{Run Automated Provers in Parallel} |
247 \subsubsection{Run Automated Provers in Parallel} |
248 \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. |
248 \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. |
249 |
249 |
250 \subsubsection{Provide a Tool Usable in Engineering Practice} |
250 \subsubsection{Provide a Tool Usable in Engineering Practice} |
251 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. |
251 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. |
252 |
252 |
253 \subsubsection{Accelerate theory evaluation} |
253 \subsubsection{Accelerate theory evaluation} |
254 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. |
254 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. |
255 |
255 |
256 |
256 |
284 \item[Propose a next step if students get stuck.] This feature seems indispensable for independent learning. However, this exceeds the traditional discipline of TP. E.g., {\it lemma} $\int{1+x+x^2\;{\it dx}} = x + \frac{x^2}{2} + \frac{x^3}{3} + c$ can be proved, but given $\int{1+x+x^2\;{\it dx}}$ there is no direct way to calculate the result $x + \frac{x^2}{2} + \frac{x^3}{3} + c$ in TP. Since indispensable, \isac{} provides this feature by a novel combination of deduction and computation, called {\em Lucas-Interpretation} \cite{neuper2012automated}. \textit{Lucas-Interpretation} works on programs which describe how to solve a problem of applied mathematics in a quite traditional way. In addition to maintaining an environment as usual for interpretation, \textit{Lucas-Interpretation} maintains a logical context, such that automated prov\-ers are provided with all current knowledge required to check user input. \cite{daroczy2013error} gives a brief introduction to \textit{Lucas-Interpretation}. |
284 \item[Propose a next step if students get stuck.] This feature seems indispensable for independent learning. However, this exceeds the traditional discipline of TP. E.g., {\it lemma} $\int{1+x+x^2\;{\it dx}} = x + \frac{x^2}{2} + \frac{x^3}{3} + c$ can be proved, but given $\int{1+x+x^2\;{\it dx}}$ there is no direct way to calculate the result $x + \frac{x^2}{2} + \frac{x^3}{3} + c$ in TP. Since indispensable, \isac{} provides this feature by a novel combination of deduction and computation, called {\em Lucas-Interpretation} \cite{neuper2012automated}. \textit{Lucas-Interpretation} works on programs which describe how to solve a problem of applied mathematics in a quite traditional way. In addition to maintaining an environment as usual for interpretation, \textit{Lucas-Interpretation} maintains a logical context, such that automated prov\-ers are provided with all current knowledge required to check user input. \cite{daroczy2013error} gives a brief introduction to \textit{Lucas-Interpretation}. |
285 \end{description} |
285 \end{description} |
286 \noindent |
286 \noindent |
287 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. |
287 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. |
288 |
288 |
289 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. |
289 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. |
290 |
290 |
291 \subsection{Architecture Separating Mathematics and Dialogs} |
291 \subsection{Architecture Separating Mathematics and Dialogs} |
292 \label{ssec:isac-archi} |
292 \label{ssec:isac-archi} |
293 The strengths of \isac's mathematics-engine, as described above, provide powerful features for human-machine interaction and thus call for concepts and technology from AI. In order to cope with increasing complexity, a separation of concerns between AI and mathematics is required. |
293 The strengths of \isac's mathematics-engine, as described above, provide powerful features for human-machine interaction and thus call for concepts and technology from AI. In order to cope with increasing complexity, a separation of concerns between AI and mathematics is required. |
294 |
294 |
362 \begin{enumerate} |
362 \begin{enumerate} |
363 \item\label{enum:thy}{\bf Deductive knowledge} is defined and managed in TP. Beginning with the basic axioms (axioms of higher-order logic in \textit{Isabelle/HOL} used by \isac), definitions are given and theorems about these definitions are proved, theory by theory. \isabelle{} provides an elegant mechanism for defining new syntax, which results in a language close to traditional mathematical notation. The subset of \isabelle{} knowledge presently in use by \isac{} can be found online \cite{isac2014knowledge}. |
363 \item\label{enum:thy}{\bf Deductive knowledge} is defined and managed in TP. Beginning with the basic axioms (axioms of higher-order logic in \textit{Isabelle/HOL} used by \isac), definitions are given and theorems about these definitions are proved, theory by theory. \isabelle{} provides an elegant mechanism for defining new syntax, which results in a language close to traditional mathematical notation. The subset of \isabelle{} knowledge presently in use by \isac{} can be found online \cite{isac2014knowledge}. |
364 \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}. |
364 \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}. |
365 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. |
365 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. |
366 This kind of problem refinement makes transparent, what is done by computer algebra systems as black boxes. |
366 This kind of problem refinement makes transparent, what is done by computer algebra systems as black boxes. |
367 \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}. |
367 \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}. |
368 \end{enumerate} |
368 \end{enumerate} |
369 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}. |
369 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}. |
370 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. |
370 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. |
371 |
371 |
372 \subsection{Relation to Ongoing \isabelle{} Development} |
372 \subsection{Relation to Ongoing \isabelle{} Development} |
398 \isabelle{}'s rewrite engine meets opposite requirements: provide a maximum of automation with large rule sets (``simpsets''). Only recently, frequent user requests motivated projects in the \isabelle{} development to provide readable traces for rewriting. |
398 \isabelle{}'s rewrite engine meets opposite requirements: provide a maximum of automation with large rule sets (``simpsets''). Only recently, frequent user requests motivated projects in the \isabelle{} development to provide readable traces for rewriting. |
399 However, the requirements of \isabelle{} and \isac{} are too different and \isac{} will keep its own rewrite engine. But the mechanism of {\em term nets} \cite{charniak2014artificial} could be adopted to improve \isac's efficiency. |
399 However, the requirements of \isabelle{} and \isac{} are too different and \isac{} will keep its own rewrite engine. But the mechanism of {\em term nets} \cite{charniak2014artificial} could be adopted to improve \isac's efficiency. |
400 |
400 |
401 \paragraph{Adopt \textit{Isabelle/jEdit} for \isac{}.} |
401 \paragraph{Adopt \textit{Isabelle/jEdit} for \isac{}.} |
402 \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{}. |
402 \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{}. |
403 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. |
403 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. |
404 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. |
404 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. |
405 |
405 |
406 \subsubsection{Summary on \isac's Approach to \isabelle{}} |
406 \subsubsection{Summary on \isac's Approach to \isabelle{}} |
407 Above, those points are listed, where \isac's math-engine is supposed to approach \isabelle{} in future development, as this thesis already has begun. Development of \isac's math-engine is separated from the development of \isac's front-end. Section \ref{ssec:isac-archi} describes \isac's {\em architecture {\em separating} mathematics and dialogs}. |
407 Above, those points are listed, where \isac's math-engine is supposed to approach \isabelle{} in future development, as this thesis already has begun. Development of \isac's math-engine is separated from the development of \isac's front-end. Section \ref{ssec:isac-archi} describes \isac's {\em architecture {\em separating} mathematics and dialogs}. |
408 Development of the front-end addresses the expertise represented by our {\em University of Applied Sciences} in Hagenberg: human-centered computing, interactive media, mobile computing, secure information systems, software engineering, etc. \isac's development efforts in these disciplines can be planned independently from the above list for several years, until \textit{Isabelle/jEdit} is ready to be adopted for \isac{} in a particularly interesting development effort. |
408 Development of the front-end addresses the expertise represented by our {\em University of Applied Sciences} in Hagenberg: human-centered computing, interactive media, mobile computing, secure information systems, software engineering, etc. \isac's development efforts in these disciplines can be planned independently from the above list for several years, until \textit{Isabelle/jEdit} is ready to be adopted for \isac{} in a particularly interesting development effort. |
419 |
419 |
420 \paragraph{Data flow.} In order to understand the following paragraphs, we need to know how \isabelle{} computes theories and what the theory data flow looks like. Section \ref{sec:isaisar} already mentioned, that the inheritance structure of \isabelle{}'s theories forms an acyclic, directed graph. Computation begins at the root theories which are determined backwards from the current working theory. The resulting data is then available in all descendant theories. Whenever a theory has more than one ancestor, the derived data is merged. |
420 \paragraph{Data flow.} In order to understand the following paragraphs, we need to know how \isabelle{} computes theories and what the theory data flow looks like. Section \ref{sec:isaisar} already mentioned, that the inheritance structure of \isabelle{}'s theories forms an acyclic, directed graph. Computation begins at the root theories which are determined backwards from the current working theory. The resulting data is then available in all descendant theories. Whenever a theory has more than one ancestor, the derived data is merged. |
421 |
421 |
422 \bigskip |
422 \bigskip |
423 |
423 |
424 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{}. |
424 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{}. |
425 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}. |
425 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}. |
426 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. |
426 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. |
427 |
427 |
428 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}): |
428 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}): |
429 \begin{enumerate} |
429 \begin{enumerate} |
430 \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: |
430 \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: |
431 \imlcode{~~\=val foo = Unsychronized.ref [1,2,3]; (*declaration*)\\ |
431 \imlcode{~~\=val foo = Unsynchronized.ref [1,2,3]; (*declaration*)\\ |
432 \>fun get\_foo () = !foo; (*new*)\\ |
432 \>fun get\_foo () = !foo; (*new*)\\ |
433 \>fun add x y = x + y;\\ |
433 \>fun add x y = x + y;\\ |
434 \>fun foo\_sum () = fold add (!foo) 0; (*obsolete*)\\ |
434 \>fun foo\_sum () = fold add (!foo) 0; (*obsolete*)\\ |
435 \>fun foo\_sum () = fold add (get\_foo ()) 0; (*new*)} |
435 \>fun foo\_sum () = fold add (get\_foo ()) 0; (*new*)} |
436 |
436 |
453 \imlcode{~~fun get\_foo () = get\_ref\_thy () |> get\_foo';} |
453 \imlcode{~~fun get\_foo () = get\_ref\_thy () |> get\_foo';} |
454 \noindent |
454 \noindent |
455 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. |
455 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. |
456 \imlcode{~~setup \{* put\_foo' [4,5,6] *\} \textit{.}} |
456 \imlcode{~~setup \{* put\_foo' [4,5,6] *\} \textit{.}} |
457 |
457 |
458 \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. |
458 \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. |
459 |
459 |
460 \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}). |
460 \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}). |
461 |
461 |
462 \item\label{enum:removecode} {\bf Cleanup.} Finally, we can remove all code concerned with the unsynchronized reference. |
462 \item\label{enum:removecode} {\bf Cleanup.} Finally, we can remove all code concerned with the unsynchronized reference. |
463 |
463 |
464 \end{enumerate} |
464 \end{enumerate} |
465 |
465 |
466 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. |
466 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. |
467 |
467 |
468 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. |
468 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. |
469 |
469 |
470 % calcelems.sml:839 |
470 % calcelems.sml:839 |
471 % merge tree into another tree (not bidirectional!) |
471 % merge tree into another tree (not bidirectional!) |
472 %(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge |
472 %(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge |
473 % function for trees / ptyps *) |
473 % function for trees / ptyps *) |
578 \caption{{\tt autoCalculate} performance comparison.} |
578 \caption{{\tt autoCalculate} performance comparison.} |
579 \label{fig:autocalc} |
579 \label{fig:autocalc} |
580 \end{figure} |
580 \end{figure} |
581 |
581 |
582 \subsubsection{Discussion} |
582 \subsubsection{Discussion} |
583 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. |
583 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. |
584 |
584 |
585 \subsection{Project Status} |
585 \subsection{Project Status} |
586 \label{sec:proj-stat} |
586 \label{sec:proj-stat} |
587 The user session management is now able to utilize several processing cores for independent computations. However, communication between the \textit{ML} and \textit{Java} layers occurs on the basis of plain standard I/O streams, i.e. multiple front-ends using the same math-engine instance need to write to the same input stream on the \textit{ML} side and thus communication is unsynchronized. This means that although the math-engine is now able to deal with calculations for multiple users concurrently in an efficient manner, the communication model does not yet allow for thread-safe communication. Changing this may be subject for a future project. Another area requiring further investigation is the memory footprint of accumulated state data for calculations and how to deal with a very high number of concurrent user sessions in this respect. |
587 The user session management is now able to utilize several processing cores for independent computations. However, communication between the \textit{ML} and \textit{Java} layers occurs on the basis of plain standard I/O streams, i.e. multiple front-ends using the same math-engine instance need to write to the same input stream on the \textit{ML} side and thus communication is unsynchronized. This means that although the math-engine is now able to deal with calculations for multiple users concurrently in an efficient manner, the communication model does not yet allow for thread-safe communication. Changing this may be subject for a future project. Another area requiring further investigation is the memory footprint of accumulated state data for calculations and how to deal with a very high number of concurrent user sessions in this respect. |
588 |
588 |