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)
possibile posto dove mettere una mini-sessione interattiva. L'appendice
un altro.}
+ \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
MONET's Broker Locating Service (since the client is supposed to know the
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}
+ ongoing \musings{}.
Additionally brokers keep track of available tutors and clients
subscriptions.
the broker instead of being received from the service when it 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
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
+ 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 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.
+ received status), the broker takes also care of stopping ongoing
+ computation invoking \texttt{Stop\_musing} tutors' method.
\paragraph{\wss{}}
As already discussed, all \hbugs{} actors act as \wss{} offering one or more
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 and the thread in duty to handle the HTTP request
+ returns an HTTP response containing an identifier of the just started
+ musing. Otherwise, if the received request is \texttt{Stop\_musing},
+ it carries a \texttt{musing} identifier used to identify the thread
+ responsible for a \texttt{musing}; that thread gets killed and an HTTP
+ response is returned.
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.