\chapter{Conclusion}

\label{cha:conclusion}

In this thesis we showed how an educational mathematics system called \isac{} was integrated with the theory data evaluation scheme managed by \isabelle, an interactive theorem proving system. This modification allowed for the straight forward introduction of a parallel execution mechanism called {\em futures}, which are data structures holding possibly unfinished computations and whose evaluation is efficiently managed by \isabelle{}'s run-time system. Before we went into the details of this process, a comprehensive theoretical basis was established. This included a discussion of the requirement for modern software to utilize the processing power available on shared memory multi-core architectures which have become a standard during the last decade. Also, various approaches towards the implementation and benefits of parallelism and concurrency in functional programming were explored, along with important aspects to consider in order to parallelize software efficiently. The architectures and technologies related to \isabelle{} and \isac{} were explained and we saw how both projects combined \textit{JVM}-based front-ends with logical engines developed in \textit{Standard ML} and followed different approaches for the communication between these layers. The systems' designs show how one can benefit from the advantages and strengths of different programming paradigms and platforms within a single architecture. The results of the case study are promising and show that depending on the problem at hand, the achievable speedup can be close to a factor of the number of available processing cores, potentially enhanced even more by the use of simultaneous multithreading (hyper-threading).

%NOTES: functional programming, higher-order -> compiler responsible for efficiency; a lot of research has gone into it.

\section{Future Work}

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.

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.

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.

% TODO: isa_pide_educational.pdf

%>>> Sind die Streams zwischen Mathematikengine und Frontend

%>>> synchronisiert? Das müsste ich dann nämlich auch noch machen. Oder

%>>> passieren sonst noch Dinge innerhalb von appendFormula, die

%>>> möglicherweise synchronisiert werden müssen?

%>>

%>> Diese Frage geht nun über die Programmiersprache (in [2] oben) weiter

%>> hinunter zum Betriebssystem: stdin/stdout Streams [3] sind da

%>> unglaublich robust: Isac funktioniert schon jetzt so, dass das Java ganz

%>> beliebig auf stdin schreibt, ohne sich irgendwie um stdout zu kümmern.

%>> Beobachtet man die Konsole, die stdin und stdout gemeinsam darstellt, so

%>> sieht das sehr verwirrend aus.

%>>

%> Isabelle hat in implementation.pdf die direkten, unsynchronisierten

%> Zugriffe auf die Standard Streams ausdrücklich verboten. Dabei geht es

%> nicht um eine Abhängigkeit zwischen stdin und stdout. Mehrere, parallele

%> Schreiboperationen auf stdout können beispielsweise zu fehlerhaften

%> Ausgaben führen.

%>> printf("hello\n");

%> und

%>> printf("world\n");

%> ergeben zB.

%>> hewolrlo

%>> ld

%> Ich weiß nicht, ob dieses Beispiel realistisch ist. Die Problematik

%> konnte ich aber nicht anders ausdrücken.

%>

%Damit hast Du die Problematik perfekt ausgedrückt, und das Beispiel ist

%sehr realistisch: die verschiedenen Threads mit den jeweiligen Aufrufen

%der math-engine kommen nach einer beliebigen Zeitspanne zurück (0.005 sec

%– 5.00 sec in verfügbaren Beispielen) --- und dann steht nur 1 stdout für

%alle Threads zur Verfügung.

%Mit dem einzigen stdout bleibt ein wesentlicher Teil des derzeitigen

%Flaschenhalses in Isac’s Interaktions-Kette nach Abschluss Deiner Arbeit

%bestehen. Damit jeder Thread seinen eigenen stdin/out bekommt, sind

%symmetrische Änderungen auf der Java-Seite notwendig --- eine schöne

%Arbeit größeren Ausmaßes für FH-Experten nach Dir !

%Damit Deine Arbeit Isac weiterhin lauffähig erhält, ist diese Aufgabe zu

%lösen:

%************ einen Thread nur dann auf den stdout nur schreiben lassen,

%                       wenn kein anderer Thread gerade schreibt    

%*********************

%Da kann ich mir im Prinzip eine Reihe von Möglichkeiten vorstellen und wir

%sollten sorgfältig beraten, welche der Möglichkeiten für Dich am

%einfachsten ist und auch möglichst kompatibel mit dem nächsten

%Entwicklungsschritt.