-
Notifications
You must be signed in to change notification settings - Fork 0
/
Interpreter.hs
169 lines (148 loc) · 5.85 KB
/
Interpreter.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
-- This file is part of FairCheck
--
-- FairCheck 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.
--
-- FairCheck 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 FairCheck. If not, see <http://www.gnu.org/licenses/>.
--
-- Copyright 2021 Luca Padovani
-- | Implementation of the interpreter for processes.
module Interpreter where
import Data.Map (Map)
import qualified Data.Map as Map
import System.Random (randomIO)
import Control.Monad (forM_, when, unless)
import Control.Exception (throw)
import Control.Concurrent
import Atoms
import Process
import Exceptions
import Render
-- | A session endpoint consists of a symbolic name, a boolean value
-- used to distinguish an endpoint from its peer, and a pair of
-- channels, the first one is used for receiving messages and the
-- second one for sending messages. The peer endpoint has the
-- opposite polarity and same two channels in the opposite order.
data Endpoint = Endpoint ChannelName Bool (Chan Message) (Chan Message)
instance Show Endpoint where
show (Endpoint u pol _ _) = show u ++ if pol then "⁺" else "⁻"
-- | Representation of messages.
data Message
-- | Termination signal.
= CloseM
-- | Delegation.
| EndpointM Endpoint
-- | Label message.
| LabelM Label
-- | An __environment__ maps channel names to session endpoints.
type Environment = Map ChannelName Endpoint
-- | Map from process names to bound names and process body.
type ProcessMap = Map ProcessName ([ChannelName], Process)
-- | Throw a runtime error.
runtimeError :: String -> a
runtimeError = throw . ErrorRuntime
-- | Generate a random integer.
randomInt :: Int -> IO Int
randomInt n = (`mod` n) <$> randomIO
-- | Given a list ws of weights and a weight n picks a random index
-- with probability that is proportional to the weight at that
-- index.
pick :: Int -> [Int] -> Int
pick m (n : _) | m < n = 0
pick m (n : ns) = 1 + pick (m - n) ns
type Thread = MVar ()
-- | Run a process.
run :: Bool -> [ProcessDef] -> Process -> IO ()
run logging pdefs = aux [] Map.empty
where
find :: Environment -> ChannelName -> Endpoint
find env u | Just c <- Map.lookup u env = c
| otherwise = runtimeError $ "unbound channel name " ++ show u
pmap :: ProcessMap
pmap = Map.fromList [ (pname, (map fst xs, p)) | (pname, xs, Just p) <- pdefs ]
new :: ChannelName -> IO (Endpoint, Endpoint)
new u = do
c <- newChan
d <- newChan
return (Endpoint u True c d, Endpoint u False d c)
send :: Environment -> ChannelName -> Message -> IO ()
send σ u | Endpoint _ _ _ x <- find σ u = writeChan x
receive :: Environment -> ChannelName -> IO Message
receive σ u | Endpoint _ _ x _ <- find σ u = readChan x
fork :: IO () -> IO Thread
fork io = do
mvar <- newEmptyMVar
forkFinally io (\_ -> putMVar mvar ())
return mvar
wait :: [Thread] -> IO ()
wait = mapM_ takeMVar
aux :: [Thread] -> Environment -> Process -> IO ()
aux threads σ Done = do
wait threads
log "done"
aux threads σ (Call pname us) =
case Map.lookup pname pmap of
Nothing -> runtimeError $ "undefined process " ++ show pname
Just (xs, p) -> do
unless (length us == length xs) $ runtimeError $ "wrong number of arguments when invoking " ++ show pname
let σ' = foldr (uncurry Map.insert) σ (zip xs (map (find σ) us))
aux threads σ' p
aux threads σ (Wait u p) = do
m <- receive σ u
case m of
CloseM -> do
log $ "closed session " ++ show (find σ u)
aux threads σ p
_ -> runtimeError $ "wait: wrong message type from " ++ show u
aux threads σ (Close u) = do
log $ "closing session " ++ show (find σ u)
send σ u CloseM
wait threads
aux threads σ (Channel u Out v p) = do
log $ "sending endpoint " ++ show (find σ v) ++ " on " ++ show (find σ u)
send σ u (EndpointM (find σ v))
aux threads (Map.delete v σ) p
aux threads σ (Channel u In x p) = do
m <- receive σ u
case m of
EndpointM s -> do
log $ "received endpoint " ++ show s ++ " from " ++ show (find σ u)
aux threads (Map.insert x s σ) p
_ -> runtimeError $ "endpoint input: wrong message type from " ++ show u
aux threads σ (Label u Out ws gs) = do
n <- randomInt (sum ws)
let (tag, p) = gs!!pick n ws
log $ "sending label " ++ show tag ++ " on " ++ show (find σ u)
send σ u (LabelM tag)
aux threads σ p
aux threads σ (Label u In _ gs) = do
m <- receive σ u
case m of
LabelM tag -> do
log $ "received label " ++ show tag ++ " from " ++ show (find σ u)
case lookup tag gs of
Just p -> aux threads σ p
Nothing -> runtimeError $ "label input: unexpected label " ++ show tag
_ -> runtimeError $ "label input: wrong message type from " ++ show u
aux threads σ (New u _ p q) = do
(x, y) <- new u
log $ "creating session " ++ show x
thread <- fork (aux [] (Map.insert u x σ) p)
aux (thread : threads) (Map.insert u y σ) q
aux threads σ (Choice m p n q) = do
i <- randomInt (m + n)
log $ "performing an internal choice " ++ show (i < m)
aux threads σ (if i < m then p else q)
aux threads σ (Cast _ _ p) = aux threads σ p
log :: String -> IO ()
log msg = do
t <- myThreadId
when logging $ printWarning $ show t ++ " " ++ msg