\ignore{
\begin{code}
\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(
Client(..),
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
class Client j where
isResult::j->Bool
\end{code}
\ignore{
\begin{code}
data Config=Config {
server::String,
port::PortID,
privateKey::PrivateKey,
publicKey::PublicKey
}
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}
signAndSend_::(Binary j)=>Config->j->ClientMessage j->IO (ServerMessage j)
signAndSend_ conf _ a=signAndSend conf a
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}
\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}