\ignore{ \begin{code}
{-#OPTIONS -cpp #-}
{-|
Module      :  Parry.Client
Copyright   :  (c) Pierre-Étienne Meunier 2014
Maintainer  :  pierre-etienne.meunier@lif.univ-mrs.fr
Stability   :  experimental
Portability :  All

Tool to build clients for Parry.
-}
\end{code} } We now prove the client functions. More precisely, we prove that the clients that can be built using the functions in this module are valid and fluent, provided that their worker'' function explores the space correctly. We include the whole source code of this module for the sake of completeness. \hfill \begin{code}
module Parry.Client(
-- * Jobs on the client side
Client(..),
-- * Writing clients
client,Config(..),defaultConfig
) where
import Network
import System.IO
import System.Exit
#ifdef UNIX
import System.Posix.Signals
#endif
import Control.Concurrent
import Control.Exception as E
import Data.List
import Codec.Crypto.RSA.Pure
import qualified Data.ByteString.Lazy.Char8 as B8
import qualified Data.ByteString.Char8 as S
import Data.Binary
import Parry.Util
import Parry.Protocol

-- | For a job to be usable by Parry's clients, it must be a member of this class.
class Client j where
-- | This function is used by the client to distinguish results from regular jobs.
isResult::j->Bool
\end{code} \ignore{ \begin{code}
-- | Client configuration
data Config=Config {
-- | The server's host name (either a DNS name or an IP address).
server::String,
-- | The port number (for instance @'Network.PortNumber' 5129@).
port::PortID,
-- | The private key to sign messages.
privateKey::PrivateKey,
-- | The public key, that the server must know of before the clients connect.
publicKey::PublicKey
}

-- | A default configuration, matching the server's
-- 'Parry.Server.defaultConfig'.  Note that, like in the server, you
-- must provide your own private key for signing the protocol
-- messages. See 'Parry.Server.defaultConfig' for an example method to
-- generate these keys.
defaultConfig::PrivateKey->PublicKey->Config
defaultConfig pr pu=Config {
server="127.0.0.1",
port=PortNumber 5129,
privateKey=pr,
publicKey=pu
}
\end{code} } \begin{lemma} \label{lem:signAndSend} The {\tt signAndSend\_} and {\tt signAndSend} functions send only one kind of messages on the network, with two lines: the first line is an encoding via {\tt encode16l} of $m$, the encoding via {\tt encode} of a constructor of the {\tt ClientMessage} type. The second line is the RSA signature of $m$ using the private key in the {\tt conf} argument. \begin{proof} The results follows from the fact that this function uses only two lines to send messages on the network, and these two lines have the claimed form. \hfill \begin{code}
-- | A wrapper around signAndSend, to force the type of @j@, which is
-- needed for the protocol's @Alive@ messages.
signAndSend_::(Binary j)=>Config->j->ClientMessage j->IO (ServerMessage j)
signAndSend_ conf _ a=signAndSend conf a

-- | Sign a message and send it.
signAndSend::(Binary j)=>Config->ClientMessage j->IO (ServerMessage j)
signAndSend conf m=do {
let { msg=encode m };
case sign (privateKey conf) msg of {
Right b->E.catch (do {
l<-bracket (connectTo (server conf) (port conf)) (hClose)
(\h->do {
B8.hPutStrLn h $encode16l msg; B8.hPutStrLn h$ encode16l b;
hFlush h;
S.hGetLine h;
});
case decodeOrFail $decode16l$ B8.fromStrict l of {
Right (_,_,a)->return a;
Left _->do {
signAndSend conf m
}
}})
(\e->do {
let { _=e::IOError };
print e;
});
er->do {
print er;hFlush stdout;threadDelay 100000;signAndSend conf m
}
}}
\end{code} \end{proof} \end{lemma} To prove the remaining functions, we need to introduce the following invariant on their arguments: \begin{invariant} \label{h} When the {\tt cur} variable is not {\tt Nothing}, the {\tt jobs} and {\tt results} variables contain, respectively, the list of all jobs of the contents of {\tt cur} that have not been completely explored, and the list of results found during the exploration of all other subjobs of the job in {\tt cur}. \end{invariant} \begin{lemma} \label{lem:dowork} If there is a function {\tt doWork} such that, at the same time: \begin{enumerate} \item For all values of {\tt b}, {\tt save} and {\tt j}, {\tt doWork b save j} only calls {\tt save} with arguments {\tt l} and {\tt r}, where {\tt r} is the list of all results that have been found when the subjobs of {\tt j} that have not been completely explored are all in list {\tt l}. \item For all values of {\tt b}, {\tt save} and {\tt j}, {\tt doWork b save j} returns the list of all subjobs of {\tt j} that have not been explored, and all results that have been found in {\tt j}, in the remaining subjobs of {\tt j}. \end{enumerate} Then {\tt client conf doWork} is a valid and fluent client. \begin{proof} We first prove fluency: in the two functions below ({\tt work} and {\tt client}), the only messages sent to the network are either sent using {\tt signAndSend}, or else consist of a single line containing exactly {\tt Hello}, which is the definition of fluency (by Lemma \ref{lem:signAndSend}). We now prove that {\tt client conf doWork} is valid. Indeed, condition \ref{valid:newjobs} of validity ({\tt NewJobs} messages contain all subjobs of the current job) is clearly respected by the {\tt work} function: indeed, by the definition of a result, the {\tt todo} variable in {\tt work} is the list of all subjobs that have not been explored. Condition \ref{valid:jobdone} is also respected, because it is not applicable to the {\tt work} function. Moreover, the {\tt work} function returns either {\tt Nothing}, or {\tt Just (j,r)} where {\tt j} is a job, and {\tt r} is the list of all results found during the exploration of {\tt j}. We prove this recursively on its code: \hfill \begin{code}
work::(Client j,Binary j)=>Config->MVar [j]->MVar[j]->MVar (Maybe j)->
(Bool->([j]->[j]->IO ())->j->IO [j])->Bool->Integer->j->IO (Maybe (j,[j]))
work conf jobs results cur doWork shared num j=do
let save jobs_ results_ jobs results=do
modifyMVar_ jobs_ $\_->return jobs modifyMVar_ results_$ \_->return results
someWork<-doWork shared (save jobs results) j
let (result,todo)=partition isResult someWork
case todo of
\end{code} \hfill Either {\tt doWork} has returned no new jobs, in which case the induction hypothesis clearly holds, because the exploration of the current job is over. \hfill \begin{code}
[]->return (Just (j,result))
\end{code} \hfill Or {\tt doWork} returns some new jobs. In this case, {\tt work} is called on {\tt u} only after reply {\tt Ack} has been received from the server, acknowledging that the current job registered for this client has been updated. Therefore, {\tt work} is called recursively on the current job of this client, and hence, the claim also holds, by recursion. \hfill \begin{code}
u:v->do
x<-signAndSend conf (NewJobs {clientId=num,jobResults=result,
currentJob=j,nextJob=u,newJobs=v })
modifyMVar_ cur (\_->do {
modifyMVar_ results (\_->return []);
modifyMVar_ jobs (\_->return [u]);
return (Just u)
})
case x of
Ack->work conf jobs results cur doWork (shared && (null v)) num u;
_->return Nothing
\end{code} \hfill We will now prove validity for the code of the {\tt client} function. We have assumed that the {\tt save} function above is only called on a list {\tt l} of subjobs, and a list {\tt r} of results, such that {\tt l} contains all subjobs of the initial job {\tt j} that have not been completely explored when results {\tt r} are found. Therefore, in the {\tt work} function above, Invariant \ref{h} on the {\tt jobs\_} and {\tt results\_} variables is clearly maintained: \hfill \ignore{ \begin{code}
-- | @'client' config work@ calls its argument function @work@ on a
-- boolean @s@ (if the server asked to share jobs) and the actual job
-- @j@ that must be done. @work@ must return a list of resulting jobs,
-- that may include results (see 'Parry.Protocol.Client').
--
-- Workers asked to share their input job should share it as early as
-- possible: this usually means that the job already got killed in a
-- previous attempt, probably because of its length.
\end{code} } \begin{code}
client::(Binary j,Client j)=>
Config->(Bool->([j]->[j]->IO())->j->IO [j])->IO ()
client conf doWork=
let startConnection=do
hPutStrLn stderr "Connecting..."
hFlush stderr
l<-E.catch (bracket (connectTo (server conf) (port conf)) hClose
(\h->do {
B8.hPutStrLn h (B8.pack "Hello");
hFlush h;
l<-S.hGetLine h;
case decodeOrFail (decode16l (B8.fromStrict l)) of {
Right x->return (Right x);
Left _->return (Left ())
}}))
(\e->let _=e::IOError in do { hPutStrLn stderr $show e; return (Left ()) }) case l of Right (_,_,num)->do jobs<-newMVar [] results<-newMVar [] cur<-newMVar Nothing \end{code} \hfill At this point, {\tt cur} contains {\tt Nothing}: Invariant \ref{h} is clearly maintained. Now remark that, when the {\tt saveAll} function below is called, and the {\tt cur} variable contains {\tt Nothing}, no message is sent. Therefore, if Invariant \ref{h} holds when {\tt saveAll} is called, the corresponding {\tt NewJobs} message respects the validity condition. \hfill \begin{code} let saveAll=withMVar jobs$ \j->
withMVar cur $\curj-> case (j,curj) of { (h:s,Just cu)-> withMVar results$ \res->do {
_<-signAndSend conf (
NewJobs { clientId=num,
jobResults=res,
currentJob=cu,
nextJob=h,
newJobs=s
});
return ()};
_->return ()
}
#ifdef UNIX
installHandler sigTERM
(Catch (modifyMVar_ threads (\a->do {if a==myth then return () else
#endif
let getAJob=do
job_<-signAndSend conf (GetJob num (publicKey conf));
case job_ of
Job share j->do
modifyMVar_ cur (\_->do {
modifyMVar_ jobs (\_->return [j]);
modifyMVar_ results (\_->return []);
return (Just j)
});
workerMVar<-newEmptyMVar;
\end{code} \hfill At this point, Invariant \ref{h} still holds: the only subjob of the current job is itself, and no results have been found. \hfill \begin{code}
forkFinally
(do {
x<-work conf jobs results cur doWork share num j;
case x of {
Just (j',r)->do {
_<-signAndSend conf
(JobDone {clientId=num,
currentJob=j',
jobResults=r });
return () };
Nothing->return ()
}})
(\_->putMVar workerMVar ())
\end{code} \hfill Here, the validity condition holds for the {\tt JobDone} message: indeed, the current job has been completely explored, and found exactly the results in {\tt r}. \hfill \begin{code}
let heartbeat=do
Ack->do { threadDelay 300000000; heartbeat }
heartbeatMVar<-newEmptyMVar
(heartbeatfinally(putMVar heartbeatMVar ()))
takeMVar workerMVar
takeMVar heartbeatMVar