\hbugs{} tutors act as MONET services.
-\section{???}
+\section{Implementation details}
\label{implementation}
+\ednote{Zack: l'aspetto grafico di questa parte e' un po' peso, possiamo
+aggiungere varie immagini volendo, e.g.: schema dei thread di un tutor, sample
+code di un tutor generato automaticamente}
+\ednote{Zack: ho cambiato idea riguardo a questa parte, mettere la lista delle
+interfacce di client/broker/... mi sembrava sterile e palloso. Di conseguenza ho
+messo i punti chiave dell'implementazione, dimmi cosa te ne pare ...}
+In this section we present some of the most relevant implementation details of
+the \hbugs{} architecture.
+
+
+ \paragraph{Proof status}
+ In our implementation of the \hbugs{} architecture we used the proof
+ assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
+ client. Thus we have implemented serialization/deserialization capabilities
+ fot its internal status. In order to be able to describe \wss{} that
+ exchange status in WSDL using the XML Schema type system, we have chosen an
+ XML format as the target format for the serialization.
+
+ A schematic representation of the gTopLevel internal status is depicted in
+ Fig. \ref{status}. Each proof is representated by a 4-tuple: \emph{uri},
+ \emph{metasenv}, \emph{proof}, \emph{term}.
+
+ \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
+ status}
+
+ \begin{description}
+ \item[uri]: an URI chosen by the user at the beginning of the proof
+ process. Once (and if) proved, that URI will globally identify the term
+ inside the \helm{} framework (given that the user decide to save it).
+ \item[metasenv]: a list of opened \emph{goals}, in order to complete the
+ proof the user has to fill them all. Each of them is identified by an
+ integer index, has a context (\emph{meta}) and a type (\emph{goal}). The
+ context is in turn represented as a list of named hypotheses
+ (declarations and definitions).
+ \item[proof]: the current incomplete proof tree. It can contain
+ metavariables (\emph{holes}) that need to be proved in order to complete
+ the proof. Each metavariables appearing in the tree reference one
+ element of the current metasenv.
+ \item[term]: the term that the ongoing proof aims to prove
+ \end{description}
+
+ Each of these information is represented in XML as described in
+ \cite{csc-thesis}. Additionally \hbugs{} status carry an integer value
+ referencing one of the opened goal; using this value is possible to
+ implement different client side strategies: the user could ask the tutors to
+ work on the same goal as the user or to work on ``background'' goals.
+
+ \paragraph{Hints}
+ An hint in the \hbugs{} architecture should carry enough information to
+ permit to the client to make progress in the current proof. In our
+ implementation each hint reference one of the tactic available to the user
+ in gTopLevel.
+
+ For tactics that don't require any particular argument (like tactics that
+ apply type constructors or try to automatically conclude equality goals)
+ only the tactic name is represented in the hint. For tactic that need terms
+ as arguments (for example the \emph{Apply} tactic) the hint includes a
+ textual representation of them, using the same representation used by the
+ interactive proof assistent when querying user for terms.
+
+ Hints are serialized to an XML format for the same reasons reported for the
+ proof status.
+
+ Actually is also possible for a tutor to return more hints at once, grouping
+ them in a particular XML element. This feature turns out to be particulary
+ useful for the \emph{searchPatternApply} tutor (Sect. \ref{tutors}) that
+ query a term database and return to the client a list of all terms that
+ could be used to complete the proof. This particular hint is encoded as a
+ list of Apply hints, each of them having one of the results as term
+ argument.
+
+ We would like to stress once more that neither the hint nor the status
+ representation are fixed by the \hbugs{} architecture. Is only necessary
+ that a common format exists and is understood by both clients and tutors.
+
+ Additionally, please note that there is no ``trust'' assumed on tutors'
+ hints. Being encoded as references to available tactics and argument imply
+ that an \hbugs{} client, on receipt of an hint, simply try to reply the work
+ done by a tutor on the local copy of the proof. The application of the hint
+ can even fail to type check and the client copy of the proof can be left
+ undamaged after spotting the error (assuming that client's type checking
+ implementation is correct, though).
+
+ Other choices of hints encoding (like sending the \emph{result} of the hint
+ application), even if reducing total computation time, don't benefit of this
+ nice property.
+
+ \paragraph{Registries}
+ Being central in the \hbugs{} architecture, the broker is also responsible
+ of accounting operations both for clients and tutors. These operations are
+ implemented using three different data structures called \emph{registries}:
+ clients registry, tutors registry and musings registry.
+
+ In order to use the suggestion engine a client should register itself to the
+ broker and subscribe to one or more tutors. The registration phase is
+ triggered by the client using the \emph{Register\_client} method of the
+ broker to send him an unique identifier and the base URI at which client's
+ \ws{} is available. After the registration, the client can use broker's
+ \emph{List\_tutors} method to get a list of available tutors. Eventually the
+ client can subscribe to one or more of these using broker's \emph{Subscribe}
+ method. Clients can also unregister from brokers using
+ \emph{Unregister\_client} method.
+
+ The broker keeps track of both registered clients and clients' subscriptions
+ in the clients registry.
+
+ In order to be advertised to clients during the subscription phase, tutors
+ should register to the broker using broker's \emph{Register\_tutor} method.
+ This method is really similar to the already seen Register\_client: tutors
+ are required to send an unique identify and a base URI for their \ws{}.
+ Additionally tutors are required to send an human readable description of
+ their capabilities, this information could be used by client's user to
+ decide which tutors he need to subscribe to. Like clients, tutors can
+ unregister from brokers using \emph{Unregister\_broker} method.
+
+ Track of available tutors is kept in the tutors registry.
+
+ Each time a new status is available from the client, it is sent to the
+ broker using its \emph{Status} method. Using both clients registry (to
+ lookup client's subscription) and tutors registry (to check if some tutors
+ has unsubscribed), the broker is able to decide to which tutor forward the
+ new status just received.
+
+ The forwarding operation is performed using tutors' \emph{Start\_musing}
+ method, that is a request to start a new computation (\emph{musing}) on a
+ given status. The return value for Start\_musing method is a musing
+ identifier that is saved in the musings registry along with the identifier
+ of the client that triggered the starting of the musing.
+
+ As soon as a musing is completed, the owning tutor informs the broker using
+ its \emph{Musing\_completed} method, the broker can now remove the musing
+ entry from the musings registry and, depending on its outcome, inform the
+ client. In case of success one of the Musing\_completed arguments is an hint
+ to be sent to the client, otherwise there's no need to inform him and the
+ Musing\_completed method is just to update the musings registry.
+
+ Consulting the musings registry, the tutor is able to know, at each time,
+ which musings are in execution on which tutor. This peculiarity is exploited
+ by the broker on invocation of Status method. Receiving a new status from
+ the client imply indeed that the previous status no longer exists and all
+ musings working on it should be stopped. Additionally to the already
+ described behaviour (i.e. starting new musings on the received status), the
+ tutor takes also care of stopping ongoing computation invoking
+ \emph{Stop\_musing} tutors' method.
+
+ \paragraph{\wss{}}
+ As already discussed, all \hbugs{} actors act as \wss{} offering one or more
+ services to neighbour actors. To grant as most accessibility as possible to
+ our \wss{} we have chosen to bind them using the HTTP/POST bindings
+ described in \cite{????}.
+
+ Given that our proof assistant was entirely developed in the Objective Caml
+ language, we have chosen to develop also \hbugs{} in that language in order
+ to maximize code reuse. To develop \wss{} in Objective Caml we have
+ developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
+ write HTTP 1.1 web servers and abstract over GET/POST parsing. This library
+ supports different kind of web servers architecture, including multi-process
+ and multi-threaded ones.
+
+ \paragraph{Tutors}
+ Each tutor expose a \ws{} interface and should be able to work, not only for
+ many different clients referring to a common broker, but also for many
+ different brokers. The potential number of clients is therefore very high
+ and is simply too non scalable to think at a single-process architecture.
+
+ Our choice was for a multi threaded architecture exploiting capabilities of
+ the O'HTTP library. Each tutor is composed by two thread always running plus
+ an additional thread for each running musing. One thread is devoted to
+ listening for incoming \ws{} request, upon correct receiving requests it
+ pass the control to the second always-running thread which handle the pool
+ of running musings. When a new musing is requested, a new thread is spawned
+ to work them out; when a request to interrupt an old musing is received, the
+ thread actually running them is killed freeing its resources.
+
+ This architecture turns out to be scalable and permit at the running threads
+ to share the type checker cache \ednote{Zack: brrrr ... abbiamo il coraggio
+ di dirlo?, mai provato :-)}. This feature turns out to be really useful
+ expecially for reflexive tactics, like Ring and Fourier, that ``reflect''
+ terms of some domain (e.g. polynomials over real numbers) in other abstract
+ domain. Type checking of most of the terms and operation in the abstract
+ domain can be indeed cached and shared by all the threads.
+
+ The implementation of a tutor with the described architecture is not that
+ difficult having a language with good threading capabilities (as OCaml has)
+ and a pool of implemented tactics (as gTopLevel has). Still working with
+ threads is known to be really error prone due to concurrent programming
+ intrinsic complexity.
+
+ To get rid of this technical problem we have written (and thoroughly tested)
+ a ``generic'' implementation of a tutor, and templated (using O'Caml
+ functors) them over some parameters like the tactic to be invoked, the hint
+ to send in case of success and a textual description of the tutor. This
+ generic implementation use O'HTTP to implement the \ws{} part of the tutor
+ and some generic routines we have implemented to handle deserialization of
+ received status and serialization of generated hints.
+
+ Having a list of available tactics and hints we are able to generate
+ automatically source code that implement all the requested tutors.
+ Obviously, this approach works only for the implementation of ``simple'' (or
+ ``stupid'', if you like) tutors that simply interface an already existing
+ proof assistant tactic and can't be used to implement more raffinate
+ decision procedures. Nonetheless, given that the number of available tactics
+ was quite high, it offered a lot of practical advantages.
\section{The \hbugs Tutors}
\label{tutors}
Once the code that implements a tactic or decision procedure is available,
transforming it into a tutor is not a difficult task, but it is surely
-repetitive and error prone.
+repetitive and error prone.\ednote{Zack: perche' hai messo qui questa parte?
+Vuoi riportare qui la generazione automatica dei tutor? per ora lo messo nella
+sezione implementazione}
\section{???}
\label{conclusions}
projects / helm.git / commitdiff