\ignore{ \begin{code}
{-#OPTIONS -cpp #-}
{-|
Module      :  Parry.Client
Copyright   :  (c) Pierre-√Čtienne Meunier 2014
License     :  GPL-3
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 {
                             threadDelay 1000000;
                             signAndSend conf m
                             }
                           }})
             (\e->do {
                 let { _=e::IOError };
                 print e;
                 threadDelay 1000000;signAndSend conf m
                 });
    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 ()
                    }
            myth<-myThreadId
            threads<-newMVar myth
#ifdef UNIX
            installHandler sigTERM
              (Catch (modifyMVar_ threads (\a->do {if a==myth then return () else
                                                     killThread a;return myth}))) Nothing
#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}
                      workerThread<-
                        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
                            answer<-signAndSend_ conf j (Alive num)
                            case answer of
                              Ack->do { threadDelay 300000000; heartbeat }
                              _->do { saveAll; killThread workerThread }
                      heartbeatMVar<-newEmptyMVar
                      hbThread<-forkIO
                                (heartbeat`finally`(putMVar heartbeatMVar ()))
                      modifyMVar_ threads (\_->return workerThread)
                      takeMVar workerMVar
                      killThread hbThread
                      takeMVar heartbeatMVar
                      stop<-withMVar threads (\t->return (t==myth))
                      if stop then do { saveAll; exitSuccess } else getAJob
                    Finished->return ();
                    _->do
                      threadDelay 10000000
                      getAJob
            getAJob
          Left _->do
            threadDelay 5000000
            startConnection
  in
   startConnection
\end{code} \end{proof} \end{lemma}