0 | module IO.Async.Loop.Epoll
  1 |
  2 | import public Data.Nat
  3 | import Control.Monad.Elin
  4 | import Data.Array.Core as AC
  5 | import Data.Array.Mutable
  6 | import Data.Bits
  7 | import Data.DPair
  8 | import Data.Linear.Traverse1
  9 | import Data.Queue
 10 | import Data.Vect
 11 |
 12 | import IO.Async.Internal.Ref
 13 | import IO.Async.Loop.Poller
 14 | import IO.Async.Loop.Queue
 15 | import IO.Async.Loop.SignalST
 16 | import IO.Async.Loop.TimerST
 17 | import IO.Async.Signal
 18 |
 19 | import public IO.Async
 20 | import public IO.Async.Loop
 21 | import public IO.Async.Loop.PollH
 22 | import public IO.Async.Loop.Posix
 23 | import public IO.Async.Loop.SignalH
 24 | import public IO.Async.Loop.TimerH
 25 |
 26 | import System
 27 | import System.Clock
 28 | import System.Linux.Epoll.Prim
 29 | import System.Posix.File.Prim
 30 | import System.Posix.Limits
 31 |
 32 | %default total
 33 |
 34 | --------------------------------------------------------------------------------
 35 | -- Epoll
 36 | --------------------------------------------------------------------------------
 37 |
 38 | -- State used for file descriptor polling
 39 | record Epoll where
 40 |   constructor P
 41 |   ||| Number of file descriptors currently waiting to be
 42 |   ||| polled
 43 |   waiting  : IORef Nat
 44 |
 45 |   ||| Maximum number of files that can be opened (based
 46 |   ||| on reading the corresponding system limit at
 47 |   ||| startup)
 48 |   maxFiles : Nat
 49 |
 50 |   ||| File event handles. This are invoked after receiving
 51 |   ||| events from `epoll`
 52 |   handles  : IOArray maxFiles FileHandle
 53 |
 54 |   ||| C array used to store file events during polling.
 55 |   events   : CArrayIO maxFiles SEpollEvent
 56 |
 57 |   ||| The `epoll` file descriptor used for polling
 58 |   epoll    : Epollfd
 59 |
 60 | mkEpoll : IO1 Epoll
 61 | mkEpoll t =
 62 |   let maxfiles    := cast {to = Nat} (sysconf SC_OPEN_MAX)
 63 |       waiting # t := ref1 Z t
 64 |       handles # t := marray1 maxfiles hdummy t
 65 |       events  # t := malloc1 SEpollEvent maxfiles t
 66 |       epoll   # t := dieOnErr (epollCreate EPOLL_CLOEXEC) t
 67 |    in P waiting maxfiles handles events epoll # t
 68 |
 69 | --------------------------------------------------------------------------------
 70 | -- Polling for File Events
 71 | --------------------------------------------------------------------------------
 72 |
 73 | parameters (p : Epoll)
 74 |
 75 |   %inline
 76 |   getHandle : Fd -> IO1 FileHandle
 77 |   getHandle f t =
 78 |     case tryNatToFin (cast f.fd) of
 79 |       Just v  => AC.get p.handles v t
 80 |       Nothing => hdummy # t
 81 |
 82 |   handleEvs : List PollPair -> IO1 ()
 83 |   handleEvs []            t = () # t
 84 |   handleEvs (PP fd ev::es) t =
 85 |     let h # t := getHandle fd t
 86 |         _ # t := h ev t
 87 |      in  handleEvs es t
 88 |
 89 |   -- Uses `epoll` to poll for file events. As long as we have
 90 |   -- other work to do, `timeout` will be 0, and this funtion will only
 91 |   -- be invoked after every `POLL_ITER` iteration of the work loop.
 92 |   --
 93 |   -- If we go to sleep, `timeout` will be set to 1 ms.
 94 |   pollWaitImpl : (timeout : Clock Duration) -> IO1 ()
 95 |   pollWaitImpl to t =
 96 |     let vs # t := dieOnErr (epollPwait2Vals p.epoll p.events to []) t
 97 |      in handleEvs vs t
 98 |
 99 |   pollImpl : IO1 ()
100 |   pollImpl t =
101 |     let S _ # t := read1 p.waiting t | _ # t => () # t
102 |      in pollWaitImpl (makeDuration 0 0) t
103 |
104 |   release : IO1 ()
105 |   release t =
106 |     let _ # t := free1 p.events t
107 |      in toF1 (close' p.epoll) t
108 |
109 | --------------------------------------------------------------------------------
110 | -- Interfaces
111 | --------------------------------------------------------------------------------
112 |
113 | parameters (p         : Epoll)
114 |            (fd        : Fd)
115 |            (ev        : PollEvent)
116 |            (autoClose : Bool)
117 |            (cb        : Either Errno PollEvent -> IO1 ())
118 |
119 |   -- calls `epoll_ctl` via the FFI to handle the file descriptor
120 |   %inline
121 |   ctl  : EpollOp -> E1 World [Errno] ()
122 |   ctl op = epollCtl p.epoll op fd ev
123 |
124 |   -- close the file descriptor if `autoClose` is set to `True`
125 |   -- this must be done *after* invoking `cb`.
126 |   %inline
127 |   closefd : IO1 ()
128 |   closefd = when1 autoClose (toF1 $ close' fd)
129 |
130 |   -- resets the file handle to `hdummy` and removes `fd` from the epoll set
131 |   %inline
132 |   cleanup : Fin p.maxFiles -> IO1 ()
133 |   cleanup v t =
134 |     let _ # t := Queue.dec p.waiting t
135 |         _ # t := AC.set p.handles v hdummy t
136 |      in e1ToF1 (ctl Del) t
137 |
138 |   -- invokes `cleanup` before running the file handle, and closes
139 |   -- the file descriptor in case `autoClose` is set to `True`.
140 |   %inline
141 |   act : Fin p.maxFiles -> FileHandle
142 |   act v e t =
143 |     let _ # t := Epoll.cleanup v t
144 |         _ # t := cb (Right e) t
145 |      in closefd t
146 |
147 |   -- we got a result before the file handle was registered.
148 |   -- we invoke the callback and close the file returning a
149 |   -- dummy cleanup hook
150 |   %inline
151 |   abrt : Either Errno PollEvent -> IO1 (IO1 ())
152 |   abrt res t =
153 |     let _ # t := cb res t
154 |         _ # t := closefd t
155 |      in unit1 # t
156 |
157 |   -- cancelation hook: like `act` but without invoking the callback
158 |   %inline
159 |   cncl : Fin p.maxFiles -> FileHandle
160 |   cncl v e t =
161 |     let _ # t := Epoll.cleanup v t
162 |      in closefd t
163 |
164 |   pollFileImpl : IO1 (IO1 ())
165 |   pollFileImpl t =
166 |     -- tries to convert the file descriptor to an index into the array
167 |     -- of file descriptors
168 |     case tryNatToFin (cast fd.fd) of
169 |       -- now trying to register the file descriptor at epoll
170 |       Just v  => case ctl Add t of
171 |         -- oops, this failed
172 |         E (Here x) t => case x == EPERM of
173 |           -- not a pollable file descriptor. we just invoke the callback with the
174 |           -- given `PollEvent`. this allows us to use the event loop even with
175 |           -- regular files, giving us a single interface for asynchronous
176 |           -- reading and writing of files
177 |           True  => abrt (Right ev) t
178 |
179 |           -- there was another event. pass it to the callback
180 |           False => abrt (Left x) t
181 |
182 |         -- success! We now register an event handler to be invoked
183 |         -- once an epoll event is ready. care must be taken to only cleanup
184 |         -- stuff once, lest we cleanup a new file descriptor while this one
185 |         -- has been closed in the meantime
186 |         R _ t   =>
187 |          let -- atomic boolean flag indicating if the handle is still active
188 |              -- this will be atomically set to `False` (using `once`)
189 |              -- before running or canceling the file handle
190 |              --
191 |              -- `cleanup` needs to be atomic because there is a race condition
192 |              -- between running the file handle once an event is ready and
193 |              -- cancelation, which might happen externally and from a different
194 |              -- thread
195 |              r # t := ref1 True t
196 |              _ # t := AC.set p.handles v (\e => once r (act v e)) t
197 |              _ # t := Queue.inc p.waiting t
198 |           in once r (cleanup v) # t
199 |       Nothing => abrt (Left EINVAL) t
200 |
201 | ||| Initialize the state of a Linux epoll poller.
202 | export
203 | epollPoller : IO1 Poller
204 | epollPoller t =
205 |   let ep # t := mkEpoll t
206 |    in MkPoller (pollImpl ep) (pollWaitImpl ep) (release ep) (pollFileImpl ep) # t
207 |
208 | ||| Simplified version of `app`.
209 | |||
210 | ||| We use environment variable `IDRIS2_ASYNC_THREADS` to determine the
211 | ||| number of threads to use (default: 2) and cancel the running program
212 | ||| on receiving `SIGINT`.
213 | |||
214 | ||| By default, only `SIGINT` is masked. To handle other signals
215 | ||| within your program, give `{sigs = [...]}` as the first
216 | ||| argument. One of the signals must be SIGINT, which is enforced by
217 | ||| the `Has SIGINT sigs` constraint.
218 | export covering
219 | epollApp
220 |   : {default [SIGINT] sigs : List Signal}
221 |   -> Has SIGINT sigs
222 |   => Async Poll [] ()
223 |   -> IO ()
224 | epollApp {sigs} prog = do
225 |   n <- asyncThreads
226 |   app n sigs epollPoller cprog
227 |
228 |   where
229 |     cprog : Async Poll [] ()
230 |     cprog =
231 |       race_
232 |         [ prog
233 |         , dropErrs {es = [Errno]} $ onSignal SIGINT (pure ())
234 |         ]
235 |