3 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).
4 %NOTES: functional programming, higher-order -> compiler responsible for efficiency; a lot of research has gone into it.
8 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.
9 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.
11 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.
12 % TODO: isa_pide_educational.pdf
14 %>>> Sind die Streams zwischen Mathematikengine und Frontend
15 %>>> synchronisiert? Das müsste ich dann nämlich auch noch machen. Oder
16 %>>> passieren sonst noch Dinge innerhalb von appendFormula, die
17 %>>> möglicherweise synchronisiert werden müssen?
19 %>> Diese Frage geht nun über die Programmiersprache (in [2] oben) weiter
20 %>> hinunter zum Betriebssystem: stdin/stdout Streams [3] sind da
21 %>> unglaublich robust: Isac funktioniert schon jetzt so, dass das Java ganz
22 %>> beliebig auf stdin schreibt, ohne sich irgendwie um stdout zu kümmern.
23 %>> Beobachtet man die Konsole, die stdin und stdout gemeinsam darstellt, so
24 %>> sieht das sehr verwirrend aus.
26 %> Isabelle hat in implementation.pdf die direkten, unsynchronisierten
27 %> Zugriffe auf die Standard Streams ausdrücklich verboten. Dabei geht es
28 %> nicht um eine Abhängigkeit zwischen stdin und stdout. Mehrere, parallele
29 %> Schreiboperationen auf stdout können beispielsweise zu fehlerhaften
31 %>> printf("hello\n");
33 %>> printf("world\n");
37 %> Ich weiß nicht, ob dieses Beispiel realistisch ist. Die Problematik
38 %> konnte ich aber nicht anders ausdrücken.
40 %Damit hast Du die Problematik perfekt ausgedrückt, und das Beispiel ist
41 %sehr realistisch: die verschiedenen Threads mit den jeweiligen Aufrufen
42 %der math-engine kommen nach einer beliebigen Zeitspanne zurück (0.005 sec
43 %– 5.00 sec in verfügbaren Beispielen) --- und dann steht nur 1 stdout für
44 %alle Threads zur Verfügung.
45 %Mit dem einzigen stdout bleibt ein wesentlicher Teil des derzeitigen
46 %Flaschenhalses in Isac’s Interaktions-Kette nach Abschluss Deiner Arbeit
47 %bestehen. Damit jeder Thread seinen eigenen stdin/out bekommt, sind
48 %symmetrische Änderungen auf der Java-Seite notwendig --- eine schöne
49 %Arbeit größeren Ausmaßes für FH-Experten nach Dir !
50 %Damit Deine Arbeit Isac weiterhin lauffähig erhält, ist diese Aufgabe zu
52 %************ einen Thread nur dann auf den stdout nur schreiben lassen,
53 % wenn kein anderer Thread gerade schreibt
54 %*********************
55 %Da kann ich mir im Prinzip eine Reihe von Möglichkeiten vorstellen und wir
56 %sollten sorgfältig beraten, welche der Möglichkeiten für Dich am
57 %einfachsten ist und auch möglichst kompatibel mit dem nächsten