{-# LANGUAGE KindSignatures , GADTs , ScopedTypeVariables , PatternSignatures , MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , TypeFamilies #-} {- Pid.hs Copyright 2008 Matthew Sackman This file is part of Session Types for Haskell. Session Types for Haskell is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. Session Types for Haskell is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with Session Types for Haskell. If not, see . -} -- | Defines what a 'Pid' is and provides functionality to create new -- sessions / channels to a given pid. Obviously this is /safe/ in -- some way - in particular, a Pid carries about with it the set of -- Session Types it is willing to use. This means that you can't try -- to start any old Session Type with any given Pid. However, it -- doesn't mean that given an acceptable Session Type, the other -- thread will ever actually get around to agreeing to create the new -- session / channel with you. module Control.Concurrent.Session.Pid ( Pid (..) , InternalPid (..) , makePid , rootPid , iPidToPid , myPid , InterleavedChain (..) , BuildPidTyMap (..) , CreateSession (..) , PidEq (..) ) where import Control.Concurrent.Session.Bool import Control.Concurrent.Session.Number import Control.Concurrent.Session.Map import Control.Concurrent.Session.List import Control.Concurrent.Session.SessionType import Control.Concurrent.Session.SMonad import Control.Concurrent.Session.Runtime import Control.Concurrent import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe type RawPid = [Int] -- | A process ID. This is a tiny bit like ThreadId but rather heavily annotated. data Pid :: * -> * -> * -> * where Pid :: RawPid -> prog -> TyMap sessionsToIdx idxsToPairStructs -> Pid prog sessionsToIdx idxsToPairStructs data InternalPid :: * -> * -> * -> * where IPid :: Pid prog sessionsToIdx idxsToPairStructs -> [RawPid] -> InternalPid prog sessionsToIdx idxsToPairStructs pidToRawPid :: Pid prog sessionsToIdx idxsToPairStructs -> RawPid pidToRawPid (Pid p _ _) = p iPidToPid :: InternalPid prog sessionsToIdx idxsToPairStructs -> Pid prog sessionsToIdx idxsToPairStructs iPidToPid (IPid p _) = p instance Show (Pid prog sessionsToIdx idxsToPairStructs) where show = (:) '<' . (:) '.' . foldr (\c a -> shows c ('.':a)) ">" . reverse . pidToRawPid instance Eq (Pid prog sessionsToIdx idxsToPairStructs) where (==) a b = (==) (pidToRawPid a) (pidToRawPid b) instance Ord (Pid prog sessionsToIdx idxsToPairStructs) where compare a b = compare (pidToRawPid a) (pidToRawPid b) instance Eq (InternalPid prog sessionsToIdx idxsToPairStructs) where (==) a b = (==) (iPidToPid a) (iPidToPid b) instance Ord (InternalPid prog sessionsToIdx idxsToPairStructs) where compare a b = compare (iPidToPid a) (iPidToPid b) -- | Provides a way to compare two Pids. Of course, if the Pids have -- different type params, then they are definitely different, but it's -- still convenient to be able to do something like (==) on them. class PidEq a b where (=~=) :: a -> b -> Bool instance PidEq (Pid progA sessionsToIdxA idxsToPairStructsA) (Pid progB sessionsToIdxB idxsToPairStructsB) where (=~=) a b = (==) (pidToRawPid a) (pidToRawPid b) makePid :: InternalPid prog sessionsToIdxO idxsToPairStructsO -> TyMap sessionsToIdxN idxsToPairStructsN -> (InternalPid prog sessionsToIdxO idxsToPairStructsO, InternalPid prog sessionsToIdxN idxsToPairStructsN) makePid (IPid orig@(Pid _ prog _) (p:ps)) childTM = ((IPid orig ps), child) where child = IPid (Pid p prog childTM) [x:p | x <- [0..]] makePid (IPid _ []) _ = error "Out of pids. Interesting." rootPid :: TyMap sessionsToIdx idxsToPairStructs -> prog -> InternalPid prog sessionsToIdx idxsToPairStructs rootPid tm prog = IPid (Pid [0] prog tm) [[x,0] | x <- [0..]] newtype InterleavedChain internalPid from to res = InterleavedChain { runInterleavedChain :: internalPid -> from -> IO (res, to, internalPid) } myPid :: InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) from from (Pid prog sessionsToIdx idxsToPairStructs) myPid = InterleavedChain $ \p x -> return (iPidToPid p, x, p) instance SMonad (InterleavedChain internalPid) where f ~>> g = InterleavedChain $ \p x -> do { (_, y, p') <- runInterleavedChain f p x ; runInterleavedChain g p' y } f ~>>= g = InterleavedChain $ \p x -> do { (a, y, p') <- runInterleavedChain f p x ; runInterleavedChain (g a) p' y } sreturn a = InterleavedChain $ \p x -> return (a, x, p) instance SMonadIO (InterleavedChain internalPid) where sliftIO f = InterleavedChain $ \p x -> do { a <- f ; return (a, x, p) } class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where type BuildPidTyMapT prog stlst buildPidTyMap :: prog -> stlst -> IO tymap instance (BuildPidTyMap' prog stlst (TyMap Nil Nil) tymap) => BuildPidTyMap prog stlst tymap where type BuildPidTyMapT prog stlst = BuildPidTyMapT' prog stlst (TyMap Nil Nil) buildPidTyMap prog stlst = buildPidTyMap' prog stlst emptyMap class BuildPidTyMap' prog stlist tymap1 tymap2 | prog stlist tymap1 -> tymap2 where type BuildPidTyMapT' prog stlist tymap1 buildPidTyMap' :: prog -> stlist -> tymap1 -> IO tymap2 instance BuildPidTyMap' prog Nil acc acc where type BuildPidTyMapT' prog Nil acc = acc buildPidTyMap' _ _ m = return m -- this instance reverses the stList in the keys of the map. So if the stList is sorted then this will be reverse . sorted instance ( BuildPidTyMap' prog nxt (TyMap keyToIdx' idxToValue') (TyMap keyToIdx'' idxToValue'') , MapInsert (TyMap keyToIdx idxToValue) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)))))) (TyMap keyToIdx' idxToValue') , TyList nxt ) => BuildPidTyMap' prog (Cons (init, False) nxt) (TyMap keyToIdx idxToValue) (TyMap keyToIdx'' idxToValue'') where type BuildPidTyMapT' prog (Cons (init, False) nxt) (TyMap keyToIdx idxToValue) = BuildPidTyMapT' prog nxt (TyMap (Cons init keyToIdx) -- HERE LIES TROUBLE! -- the use of DualT to make the inverse may be dangerous (Cons ((MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog (DualT prog) ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))))))) idxToValue)) buildPidTyMap' prog lst m = do { mvar <- newMVar Map.empty ; buildPidTyMap' prog nxt (m' mvar) } where (init, FF) = tyHead lst nxt = tyTail lst m' :: (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)))))) -> TyMap keyToIdx' idxToValue' m' mvar = mapInsert init mvar m instance ( BuildPidTyMap' prog nxt (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') , TyList nxt ) => BuildPidTyMap' prog (Cons (init, True) nxt) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') where type BuildPidTyMapT' prog (Cons (init, True) nxt) (TyMap keyToIdx idxToValue) = BuildPidTyMapT' prog nxt (TyMap keyToIdx idxToValue) buildPidTyMap' prog lst m = buildPidTyMap' prog (tyTail lst) m type instance Outgoing prog (Cons (RecvPid False t) nxt) = Outgoing prog nxt type instance Outgoing prog (Cons (SendPid False t) nxt) = Cons (Pid prog (LHS (BuildPidTyMapT prog t)) (RHS (BuildPidTyMapT prog t))) (Outgoing prog nxt) type instance Outgoing prog (Cons (RecvPid True t) nxt) = Outgoing (DualT prog) nxt type instance Outgoing prog (Cons (SendPid True t) nxt) = Cons (Pid (DualT prog) (LHS (BuildPidTyMapT prog t)) (RHS (BuildPidTyMapT prog t))) (Outgoing prog nxt) instance ( ExpandPids prog nxt nxt' , TyList nxt , TyList nxt' , BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs) , If invert prog' prog progO , Dual prog prog' ) => ExpandPids prog (Cons (RecvPid invert t) nxt) (Cons (Recv (Pid progO sessionsToIdx idxsToPairStructs)) nxt') where expandPids prog lst = modifyCons (const undefined) (expandPids prog) lst instance ( ExpandPids prog nxt nxt' , TyList nxt , TyList nxt' , BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs) , If invert prog' prog progO , Dual prog prog' ) => ExpandPids prog (Cons (SendPid invert t) nxt) (Cons (Send (Pid progO sessionsToIdx idxsToPairStructs)) nxt') where expandPids prog lst = modifyCons (const undefined) (expandPids prog) lst type family LHS thing type instance LHS (TyMap sessionsToIdx idxsToPairStructs) = sessionsToIdx type family RHS thing type instance RHS (TyMap sessionsToIdx idxsToPairStructs) = idxsToPairStructs data PairStruct :: * -> * -> * -> * -> * where PS ::RawPid -> (SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ()) -> PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) instance Eq (PairStruct init prog prog' start) where (==) (PS x _) (PS y _) = x == y instance Ord (PairStruct init prog prog' start) where compare (PS x _) (PS y _) = compare x y -- TyMap :: (init, InvertBool) -> MVar (Map (RawPid, RawPid) (MVar PairStruct init prog progOut progIn (fromO, fromI))) -- | Provides the ability to make a new session / channel with the -- given Pid. Supply the index to the Session Type, whether or not -- you're locally inverting (dualing) the Session Type, and the Pid, -- and so long as the Pid supports the dual of your local Session -- Type, this will block until the Pid gets around to servicing you. -- Thus this is a synchronous operation and both Pids must know of -- each other to create a new session / channel between them. class CreateSession invert init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where createSession :: init -> invert -> Pid prog sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem instance forall init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem current current' . ( ProgramToMVarsOutgoingT prog prog ~ progOut , ProgramToMVarsOutgoingT prog' prog' ~ progIn , ProgramToMVarsOutgoing prog prog progOut , ProgramToMVarsOutgoing prog' prog' progIn , SWellFormedConfig init (D0 E) prog , SWellFormedConfig init (D0 E) prog' , TyListIndex progOut init (MVar (ProgramCell (Cell fromO))) , TyListIndex progIn init (MVar (ProgramCell (Cell fromI))) , TyListIndex prog init current' , ExpandPids prog current' current , MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)))))) , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe') ) => CreateSession False init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where createSession init FF (Pid remotePid _ _) = InterleavedChain $ \ipid@(IPid (Pid localPid _ localSTMap) _) mp -> do { let pidFuncMapMVar :: MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))))) = mapLookup localSTMap init ; pidFuncMap <- takeMVar pidFuncMapMVar ; emptyMVar :: MVar (TyMap keyToIdxMe' idxToValueMe') <- newEmptyMVar ; psMVar :: MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))) <- case Map.lookup (localPid, remotePid) pidFuncMap of Nothing -> do { empty <- newEmptyMVar ; putMVar pidFuncMapMVar (Map.insert (localPid, remotePid) empty pidFuncMap) ; return empty } (Just mv) -> do { putMVar pidFuncMapMVar pidFuncMap ; return mv } ; let idxOfThem :: idxOfThem = mapSize mp ps :: PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) = PS localPid (f idxOfThem mp emptyMVar) ; putMVar psMVar ps ; mp' <- takeMVar emptyMVar ; return (idxOfThem, mp', ipid) } where f :: idxOfThem -> (TyMap keyToIdxMe idxToValueMe) -> MVar (TyMap keyToIdxMe' idxToValueMe') -> SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO () f idxOfThem mp mv localST = do { ((), localST') <- runSessionChain sjump localST ; putMVar mv (mapInsert idxOfThem localST' mp) } instance forall init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem current current' currentUX currentUX' . ( ProgramToMVarsOutgoingT prog prog ~ progOut , ProgramToMVarsOutgoingT prog' prog' ~ progIn , ProgramToMVarsOutgoing prog prog progOut , ProgramToMVarsOutgoing prog' prog' progIn , SWellFormedConfig init (D0 E) prog , SWellFormedConfig init (D0 E) prog' , TyListIndex progOut init (MVar (ProgramCell (Cell fromO))) , TyListIndex progIn init (MVar (ProgramCell (Cell fromI))) , TyListIndex prog init currentUX , ExpandPids prog currentUX current , TyListIndex prog' init currentUX' , ExpandPids prog' currentUX' current' , MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init (MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)))))) , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe') , Dual prog prog' ) => CreateSession True init prog prog' fromO fromI progOut progIn sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where createSession init TT (Pid remotePid prog remoteSTMap) = InterleavedChain $ \ipid@(IPid (Pid localPid _ _) _) mp -> do { let pidFuncMapMVar :: MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))))) = mapLookup remoteSTMap init prog' = dual prog ; pidFuncMap <- takeMVar pidFuncMapMVar ; mvarsOut <- programToMVarsOutgoing prog prog ; mvarsIn <- programToMVarsOutgoing prog' prog' ; let (theirST :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))) = SessionState prog prog' mvarsOut mvarsIn undefined undefined undefined (myST :: SessionState prog' prog ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil))) = SessionState prog' prog mvarsIn mvarsOut undefined undefined undefined idxOfThem :: idxOfThem = mapSize mp ; case Map.lookup (remotePid, localPid) pidFuncMap of Nothing -> do { newEmptyMVar <- newEmptyMVar ; putMVar pidFuncMapMVar (Map.insert (remotePid, localPid) newEmptyMVar pidFuncMap) ; ps <- takeMVar newEmptyMVar ; modifyMVar_ pidFuncMapMVar (return . Map.delete (remotePid, localPid)) ; case ps of (PS _ (f :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ())) -> f theirST } (Just fullMVar) -> do { ps <- takeMVar fullMVar ; putMVar pidFuncMapMVar (Map.delete (remotePid, localPid) pidFuncMap) ; case ps of (PS _ (f :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ())) -> f theirST } ; ((), myST') <- runSessionChain sjump myST ; return (idxOfThem, mapInsert idxOfThem myST' mp, ipid) }