The big challenge for the next future is to provide stable and reliable
services over this disorganized, unreliable and ever-evolving architecture.
- The standard solution \ednote{zack: buhm! :-P} is providing a further level of
+ The standard solution is providing a further level of
stable services (called \emph{brokers}) that behave as common gateway/address
for client applications to access a wide variety of services and abstract over
them.
\Omegapp{} proof-planner \cite{omega}. The main architectural difference
between \hbugs{} and \OmegaAnts{} are that the latter is based on a
black-board architecture and it is not implemented using \wss{} and
- brokers. Other differences will be detailed in Sect. \ref{conclusions}
- \ednote{CSC: che si fa di sta frase?}.
+ brokers.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
Further implementation details are given in Sect. \ref{implementation}.
A proof status is a representation of an incomplete proof and is supposed to
be informative enough to be used by an interactive proof assistant. No
additional requirements exist on the proof status, but there should be an
- agreement on its format between clients and tutors. An hint is a
- representation\ednote{CSC: non c'\'e un sinonimo pi\'u carino? Zack: l'unico
- decente sembra essere nuovamente "suggestion". CSC: chiamalo sinonimo!}
- of a step that can be performed in order to proceed in an
+ agreement on its format between clients and tutors. An hint is an
+ encoding of a step that can be performed in order to proceed in an
incomplete proof. Usually it represents a reference to a tactic available
on some proof assistant along with an instantiation for its formal
parameters. More structured hints can also be used: an hint can be
as complex as a whole proof-plan.
- \myincludegraphics{interfaces}{t}{10cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
- \wss{} interfaces}
-
Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
providers and requesters, see Fig. \ref{interfaces}.
They act as providers for the broker (to receive hints)
additionally use broker service to know which tutors are available and to
subscribe to one or more of them.
- Usually, when the role of client is taken by an interactive proof assistant,
+ Usually, when the client role is taken by an interactive proof assistant,
new status are sent to the broker as soon as the proof change (e.g. when the
user applies a tactic or when a new proof is started) and hints are shown to
the user be the means of some effect in the user interface (e.g. popping a
dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
- possibile posto dove mettere una mini-sessione interattiva. L'appendice
- un altro.}
+ possibile posto dove mettere una reference a una mini-sessione interattiva.
+ \'E l'appendice un posto dove metterla?}
+
+ \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
+ {\hbugs{} \wss{} interfaces}
\hbugs{} clients act as MONET clients and ask brokers to provide access to a
set of services (the tutors). \hbugs{} has no actors corresponding to
providers and requesters for \emph{both} clients and tutors, see Fig.
\ref{interfaces}.
- With respect to client, a broker act as \ws{} provider, receiving the
+ With respect to the client, a broker acts as a \ws{} provider, receiving the
proof status and forwarding it to one or more tutors.
It also acts as a \ws{} requester sending
hints to the client as soon as they are available from the tutors.
- With respect to tutors, the \ws{} provider role is accomplished by receiving
- hints as soon as they are produced; as a requester, it is accomplished
- by asking for computations (\emph{musings} in \hbugs{} terminology) on
- status received by clients and by stopping already late but still
- ongoing \musings{}
- \ednote{Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo
- commento sulla utilita'/quantita' delle figure ... CSC: vanno benissimo}
+ With respect to the tutors, the \ws{} provider role is accomplished by
+ receiving hints as soon as they are produced; as a requester, it is
+ accomplished by asking for computations (\emph{musings} in \hbugs{}
+ terminology) on status received by clients and by stopping already late but
+ still ongoing \musings{}.
Additionally brokers keep track of available tutors and clients
subscriptions.
which the client is subscribed), Execution Manager. The Service Manager
component is not required since the session handler, that identifies
a session between a service and a broker, is provided to the service by
- the broker instead of being received from the service when it is
+ the broker instead of being received from the service when the session is
initialized. In particular, a session is identified by an unique identifier
for the client (its URL) and an unique identifier for the broker (its
- URL).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i
- multi-sessione. Ma mi sembra la strada che prenderemmo, no?}
+ URL).
The MONET architecture specification does not state explicitly whether
the service and broker answers can be asynchronous. Nevertheless, the
\paragraph{Tutors}
Tutors are software component able to consume proof status producing hints.
- \hbugs{} doesn't specify by which means hints should be produced: tutors can
- use any means necessary (heuristics, external theorem prover or CAS, ...).
- The only requirement is that there exists an agreement on the formats of
- proof status and hints.
+ \hbugs{} does not specify by which means hints should be produced: tutors
+ can use any means necessary (heuristics, external theorem prover or CAS,
+ etc.). The only requirement is that there exists an agreement on the
+ formats of proof status and hints.
Tutors act both as \ws{} providers and requesters for the broker. As
providers, they wait for commands requesting to start a new \musing{} on
\hbugs{} tutors act as MONET services.
+\section{An \hbugs{} Session Example}
+
\section{Implementation's Highlights}
\label{implementation}
In this section we present some of the most relevant implementation details of
unregister from brokers using \texttt{Unregister\_broker} method.
Each time the client status change, the status is sent to the
- broker using its \emph{Status} method. Using both clients registry (to
+ broker using its \texttt{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 tutors the
new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
della possibilit\'a di avere un vero brocker che multiplexi le richieste
- del tutor localizzando i servizi, etc.}
+ dei client localizzando i servizi, etc.}
The forwarding operation is performed using the \texttt{Start\_musing}
method of the tutors, that is a request to start a new computation
inform him and the \texttt{Musing\_completed} method is called
just to update the \musings{} registry.
- Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
- stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
- ovviamente ... CSC: ma a che serve???} 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 implies indeed that the previous status no longer
- exists and all \musings{} working on it should be stopped: additionally to
- the already described behavior (i.e. starting new \musings{} on the
- received status), the tutor\ednote{CSC: Ma sei veramente veramente sicuro?}
- takes also care of stopping ongoing computation invoking
- \texttt{Stop\_musing} tutors' method.
+ Consulting the \musings{} registry, the broker 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 the \texttt{Status} method.
+ Receiving a new status from the client implies indeed that the previous
+ status no longer exists and all \musings{} working on it should be stopped:
+ additionally to the already described behavior (i.e. starting new
+ \musings{} on the received status), the broker takes also care of stopping
+ ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
\paragraph{\wss{}}
As already discussed, all \hbugs{} actors act as \wss{} offering one or more
services to neighbor 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{wsdlbindings}\footnote{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 kinds of Web
- servers architecture, including multi-process and multi-threaded ones.}.
+ our \wss{} we have chosen to bind them using the HTTP/POST\footnote{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 kinds of Web servers architecture, including
+ multi-process and multi-threaded ones.} bindings described in
+ \cite{wsdlbindings}.
\paragraph{Tutors}
Each tutor expose a \ws{} interface and should be able to work, not only for
Our current implementation is based on a multi threaded architecture
exploiting the capabilities of the O'HTTP library. Each tutor is composed
- by two thread always running plus
+ by one 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.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
- ricordo male al problema dell'uccisione dei thread. Ora o si spiega
- il motivo di questa architettura o si glissa/bluffa. Zack: cosa ti sembra
- delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...
- CSC: la motivazione per avere due thread always running e non due}
-
+ pass the control to a second thread, created on the fly, to handle the
+ incoming request following the classical one-thread-per-request approach in
+ web servers design.
+ If the received request is \texttt{Start\_musing}, a new thread is
+ spawned to handle it; the thread in duty to handle the HTTP request
+ returns an HTTP response containing the identifier of the just started
+ \texttt{musing}, and then dyes. If the received request is
+ \texttt{Stop\_musing}, instead, the spawned thread kills the thread
+ responsible for the \texttt{musing} whose identifier is the argument
+ of the \texttt{Stop\_musing} method.
+
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.
As we will explain in Sect. \ref{tutors}, this feature turns out to be
with the \helm{} Search-Engine and looks for lemmas that can be directly
applied.
- We have many plan for further developing both the \hbugs{} architecture and
+ We have many plans for further developing both the \hbugs{} architecture and
our prototype. Interesting results could be obtained
augmenting the informative content of each suggestion. We can for example
modify the broker so that also negative results are sent back to the client.
the client to trust other actors a bit more than in the current approach.
We plan also to add some rating mechanism to the architecture. A first
- improvement in this direction could be to distinguish between hints that, when
+ improvement in this direction could be distinguishing between hints that, when
applied, are able to completely close one or more goals and
tactics that progress in the proof by reducing one or more goals to new goals:
the new goals could be false and the proof can be closed only by backtracking.
privileging therefore non-overkilling solutions \cite{ring}.
We are also considering to follow the \OmegaAnts{} path more closely adding
- ``recursion'' to the system so that proof status resulting from the
+ ``recursion'' to the system so that the proof status resulting from the
application of old hints are cached somewhere and could be used as a starting
point for new hint searches. The approach is interesting, but it represents
a big shift towards automatic theorem proving: thus we must consider if it is
worth the effort given the increasing availability of automation in proof
- assistants' tactics and the ongoing development of \wss{} based on
+ assistants tactics and the ongoing development of \wss{} based on
already existent and well developed theorem provers.
Even if not strictly part of the \hbugs{} architecture, the graphical user
projects / helm.git / blobdiff