Skip to content

Commit

Permalink
Added example for dual handoff
Browse files Browse the repository at this point in the history
  • Loading branch information
LLaeufer committed Dec 19, 2022
1 parent 88030ae commit b328820
Show file tree
Hide file tree
Showing 6 changed files with 141 additions and 6 deletions.
36 changes: 36 additions & 0 deletions dev-examples/bidirhandoff/client.ldgvnw
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
-- Simple example of Label-Dependent Session Types
-- Interprets addition of two numbers

type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit
type SendIntClient : ! ~ssn = !Int. ?Int. Unit
type SendSendIntClient : ! ~ssn = !SendIntClient. Unit
type SendIntServer : ! ~ssn = ?Int. !Int. Unit
type SendSendIntServer : ! ~ssn = !SendIntServer. Unit

val send2 (c: SendInt) =
let x = ((send c) 1) in
let <n, x2> = recv x in
let y = ((send x2) 41) in
let <m, y2> = recv y in
let y3 = end y2 in
(m + n)

val add2 (c1: dualof SendInt) =
let <m, c2> = recv c1 in
let c22 = (send c2) 1300 in
let <n, c3> = recv c22 in
let c32 = (send c3) 37 in
let c4 = end c32 in
(m + n)

val main : Int
val main =
let sock = (create 4343) in
let con = (connect sock SendInt "127.0.0.1" 4242 ) in -- This cannot be localhost, since this might break on containerized images
let x = ((send con) 1) in
let <n, x2> = recv x in
let con2 = (connect sock SendSendIntClient "127.0.0.1" 4340) in
let con22 = ((send con2) x2) in
let con23 = end con22 in
(n)

35 changes: 35 additions & 0 deletions dev-examples/bidirhandoff/clienthandoff.ldgvnw
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
-- Simple example of Label-Dependent Session Types
-- Interprets addition of two numbers

type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit
type SendIntClient : ! ~ssn = !Int. ?Int. Unit
type SendSendIntClient : ! ~ssn = !SendIntClient. Unit
type SendIntServer : ! ~ssn = ?Int. !Int. Unit
type SendSendIntServer : ! ~ssn = !SendIntServer. Unit

val send2 (c: SendInt) =
let x = ((send c) 1) in
let <n, x2> = recv x in
let y = ((send x2) 41) in
let <m, y2> = recv y in
let y3 = end y2 in
(m + n)

val add2 (c1: dualof SendInt) =
let <m, c2> = recv c1 in
let c22 = (send c2) 1300 in
let <n, c3> = recv c22 in
let c32 = (send c3) 37 in
let c4 = end c32 in
(m + n)

val main : Int
val main =
let sock = (create 4340) in
let con = (accept sock (dualof SendSendIntClient)) in -- This cannot be localhost, since this might break on containerized images
let <talk, y> = (recv con) in
let x = ((send talk) 41) in
let <n, x2> = recv x in
let con2 = end x2 in
(n)

35 changes: 35 additions & 0 deletions dev-examples/bidirhandoff/server.ldgvnw
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
-- Simple example of Label-Dependent Session Types
-- Interprets addition of two numbers

type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit
type SendIntClient : ! ~ssn = !Int. ?Int. Unit
type SendSendIntClient : ! ~ssn = !SendIntClient. Unit
type SendIntServer : ! ~ssn = ?Int. !Int. Unit
type SendSendIntServer : ! ~ssn = !SendIntServer. Unit

val send2 (c: SendInt) =
let x = ((send c) 1) in
let <n, x2> = recv x in
let y = ((send x2) 41) in
let <m, y2> = recv y in
let y3 = end y2 in
(m + n)

val add2 (c1: dualof SendInt) =
let <m, c2> = recv c1 in
let c22 = (send c2) 1300 in
let <n, c3> = recv c22 in
let c32 = (send c3) 37 in
let c4 = end c32 in
(m + n)

val main : Int
val main =
let sock = (create 4242) in
let con = (accept sock (dualof SendInt)) in
let <m, c2> = recv con in
let c22 = (send c2) 1300 in
let con2 = (accept sock (SendSendIntServer)) in
let con3 = ((send con2) c22) in
let con4 = end con3 in
(m)
34 changes: 34 additions & 0 deletions dev-examples/bidirhandoff/serverhandoff.ldgvnw
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
-- Simple example of Label-Dependent Session Types
-- Interprets addition of two numbers

type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit
type SendIntClient : ! ~ssn = !Int. ?Int. Unit
type SendSendIntClient : ! ~ssn = !SendIntClient. Unit
type SendIntServer : ! ~ssn = ?Int. !Int. Unit
type SendSendIntServer : ! ~ssn = !SendIntServer. Unit

val send2 (c: SendInt) =
let x = ((send c) 1) in
let <n, x2> = recv x in
let y = ((send x2) 41) in
let <m, y2> = recv y in
let y3 = end y2 in
(m + n)

val add2 (c1: dualof SendInt) =
let <m, c2> = recv c1 in
let c22 = (send c2) 1300 in
let <n, c3> = recv c22 in
let c32 = (send c3) 37 in
let c4 = end c32 in
(m + n)

val main : Int
val main =
let sock = (create 4240) in
let con = (connect sock (dualof SendSendIntServer) "127.0.0.1" 4242) in
let <talk, c1> = recv con in
let <m, c2> = recv talk in
let c22 = (send c2) 37 in
let con4 = end c22 in
(m)
2 changes: 1 addition & 1 deletion src/Networking/Client.hs
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ sendVChanMessages newhost newport input = case input of
VChan nc _ _-> do
sendNetworkMessage nc (Messages.ChangePartnerAddress (Data.Maybe.fromMaybe "" $ ncOwnUserID nc) newhost newport)
_ <- MVar.takeMVar $ ncConnectionState nc
putStrLn $ "Set RedirectRequest for " ++ (Data.Maybe.fromMaybe "" $ ncPartnerUserID nc) ++ " to " ++ newhost ++ ":" ++ newport
Config.traceIO $ "Set RedirectRequest for " ++ (Data.Maybe.fromMaybe "" $ ncPartnerUserID nc) ++ " to " ++ newhost ++ ":" ++ newport
MVar.putMVar (ncConnectionState nc) $ NCon.RedirectRequest newhost newport
_ -> return ()
where
Expand Down
5 changes: 0 additions & 5 deletions src/Networking/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -96,13 +96,10 @@ acceptClient mvar clientlist clientsocket = do

checkRedirectRequest :: Map.Map String (NetworkConnection Value) -> String -> IO Bool
checkRedirectRequest ncmap userid = do
putStrLn $ "Checking redirect request of user: " ++ userid
case Map.lookup userid ncmap of
Nothing -> do
putStrLn $ "Warning user " ++ userid ++ " not found when processing redirect request!"
return False
Just networkconnection -> do
putStrLn $ "Trying to check connectionstate of user: " ++ userid
constate <- MVar.readMVar $ ncConnectionState networkconnection
print constate
case constate of
Expand All @@ -112,7 +109,6 @@ checkRedirectRequest ncmap userid = do

sendRedirect :: Handle -> Map.Map String (NetworkConnection Value) -> String -> IO ()
sendRedirect handle ncmap userid = do
putStrLn "WARNING: Trying to send redirect!"
case Map.lookup userid ncmap of
Nothing -> return ()
Just networkconnection -> do
Expand Down Expand Up @@ -163,7 +159,6 @@ handleChangePartnerAddress mvar userid hostname port = do
NCon.changePartnerAddress networkconnection hostname port
-- For some reason constate doesn't seem to properly apply
MVar.putMVar mvar networkconnectionmap
putStrLn "Changed partner address!"

Nothing -> MVar.putMVar mvar networkconnectionmap -- Nothing needs to be done here, the connection hasn't been established yet. No need to save that

Expand Down

0 comments on commit b328820

Please sign in to comment.