From 505672eb023eaaaeb6a7c5ac3652f542e96c6a8e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 May 2003 17:48:22 +0000 Subject: [PATCH] Several editor notes resolved. --- .../calculemus-2003/hbugs-calculemus-2003.tex | 31 +++++++------------ 1 file changed, 11 insertions(+), 20 deletions(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 723d21dd1..49322ba2e 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -75,7 +75,7 @@ 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. @@ -120,8 +120,7 @@ \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}. @@ -148,10 +147,8 @@ 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 @@ -201,9 +198,7 @@ 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. @@ -217,8 +212,7 @@ 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 @@ -384,7 +378,7 @@ the \hbugs{} architecture. 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 @@ -401,17 +395,14 @@ the \hbugs{} architecture. 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 -- 2.39.2