From: Stefano Zacchiroli Date: Mon, 26 May 2003 07:53:49 +0000 (+0000) Subject: written section 3 X-Git-Tag: submitted~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5e0d6f71a0edd3e222841b04b616c5873ecd8a15 written section 3 --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 87e20b3c6..1f5974807 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -221,8 +221,211 @@ \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} @@ -326,7 +529,9 @@ we have investigated three classes of 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} diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt index a82334740..55cb826ce 100644 --- a/helm/papers/calculemus-2003/outline.txt +++ b/helm/papers/calculemus-2003/outline.txt @@ -14,23 +14,13 @@ - attori (client, broker, tutor) - ruoli e funzionalita' di ognuno di essi (breve) - mapping con gli attori di monet -3) Dettagli - 3.1) codifica dello stato e dei suggerimenti - - oss: l'architettura e' generica non dipenda da una particolare codifica di - dimostrazioni - - interfaccia verso il broker - 3.2) client - - proof assistant - 3.3) broker - - registri - - interfaccia verso i client (registrazione, sottoscrizione, state change, - deregistrazione) - - interfaccia verso i tutor (registrazione, suggerimento, deregistrazione) - 3.4) tutor - - cosa puo' implementare un tutor - - nessuna assunzione sulla correttezza del suggerimento - - interfaccia verso il broker (start/stop musing) - - thread (?) +3) Zack + Dettagli Implementativi + - codifica dello stato + - codifica dei suggerimenti + - registry del broker + - implementazione dei ws + - implementazione dei tutor (gen. automatica, thread) 4) CSC Sample session - screen shot