0 | ||| This provides wrappers around the `sys/eventfd.h` module: An "event"
  1 | ||| file descriptort that can be monitored via `epoll` and written to
  2 | ||| programmatically to wake up a dormant thread.
  3 | |||
  4 | ||| The file descriptor can work in `EFD_SEMAPHORE` mode, in which case it
  5 | ||| can indeed be used liked a `System.Concurrent.Semaphore` or a
  6 | ||| `System.Concurrent.Condition`.
  7 | module System.Linux.EventFD
  8 |
  9 | import Data.Bits
 10 | import Derive.Prelude
 11 | import System.Linux.Error
 12 | import System.Linux.File
 13 |
 14 | %language ElabReflection
 15 | %default total
 16 |
 17 | --------------------------------------------------------------------------------
 18 | -- FFI
 19 | --------------------------------------------------------------------------------
 20 |
 21 | %foreign "C:ep_readEventFile,epoll-idris"
 22 | prim__ep_readEventFile : Bits32 -> PrimIO Bits64
 23 |
 24 | %foreign "C:ep_writeEventFile,epoll-idris"
 25 | prim__ep_writeEventFile : Bits32 -> Bits64 -> PrimIO ()
 26 |
 27 | %foreign "C:ep_efd_cloexec,epoll-idris"
 28 | ep_efd_cloexec : Bits32
 29 |
 30 | %foreign "C:ep_efd_nonblock,epoll-idris"
 31 | ep_efd_nonblock : Bits32
 32 |
 33 | %foreign "C:ep_efd_semaphore,epoll-idris"
 34 | ep_efd_semaphore : Bits32
 35 |
 36 | %foreign "C:eventfd,epoll-idris"
 37 | prim__eventfd : Bits64 -> Bits32 -> PrimIO Bits32
 38 |
 39 | --------------------------------------------------------------------------------
 40 | -- API
 41 | --------------------------------------------------------------------------------
 42 |
 43 | ||| Flags describing the behavior of an event file descriptor.
 44 | |||
 45 | ||| Several flags can be combined using `(<+>)`.
 46 | export
 47 | record Flags where
 48 |   constructor F
 49 |   value : Bits32
 50 |
 51 | %runElab derive "Flags" [Show,Eq,Ord]
 52 |
 53 | export %inline
 54 | flagCode : Flags -> Bits32
 55 | flagCode = value
 56 |
 57 | export %inline
 58 | Semigroup Flags where
 59 |   F x <+> F y = F (x .|. y)
 60 |
 61 | export %inline
 62 | Monoid Flags where neutral = F 0
 63 |
 64 | export %inline
 65 | EFD_CLOEXEC : Flags
 66 | EFD_CLOEXEC = F ep_efd_cloexec
 67 |
 68 | ||| Sets the file descriptor to non-blocking: Reading from
 69 | ||| an `EventFD` via `readEv` will usually block the calling thread
 70 | ||| unless the file descriptor's stored value is greater than zero.
 71 | |||
 72 | ||| With this flag being set, `readEv` will never block but will return
 73 | ||| `Left EAGAIN` in case of an empty file descriptor.
 74 | export %inline
 75 | EFD_NONBLOCK : Flags
 76 | EFD_NONBLOCK = F ep_efd_nonblock
 77 |
 78 | ||| Changes the file descriptor to work in "semaphore mode": Usually,
 79 | ||| `readEv` will return the whole 64-bit value currently stored in the
 80 | ||| file descriptor. In semaphore mode, `readEv` will always return 1
 81 | ||| (unliss the file descriptor is empty) and likewise reduce the stored
 82 | ||| value by 1.
 83 | export %inline
 84 | EFD_SEMAPHORE : Flags
 85 | EFD_SEMAPHORE = F ep_efd_semaphore
 86 |
 87 | ||| An event file descriptor that can be monitored via `epoll`
 88 | ||| and programmatically written to and read from.
 89 | public export
 90 | record EventFD where
 91 |   constructor EFD
 92 |   file : Bits32
 93 |
 94 | export %inline
 95 | FileDesc EventFD where fileDesc = file
 96 |
 97 | ||| Creates a new `EventFD` with the given initial value a flags set.
 98 | export %inline
 99 | eventfd : (init : Bits64) -> Flags -> PrimIO EventFD
100 | eventfd i (F f) w =
101 |   let MkIORes file w := prim__eventfd i f w
102 |    in MkIORes (EFD file) w
103 |
104 | ||| Writes (adds) the given 64-bit value to the value currently stored
105 | ||| in the given event file descriptor.
106 | export %inline
107 | writeEv : EventFD -> Bits64 -> PrimIO ()
108 | writeEv (EFD f) v = prim__ep_writeEventFile f v
109 |
110 | ||| Reads the current value from an event file descriptor, setting the
111 | ||| stored value to 0.
112 | |||
113 | ||| If the `EFD_SEMAPHORE` flag was set when creating the file descriptor,
114 | ||| this will always return 1 in case the event file is non-empty. Likewise,
115 | ||| the value stored in the event file will be reduced by one.
116 | export %inline
117 | readEv : EventFD -> PrimIO (Either EpollErr Bits64)
118 | readEv (EFD f) w =
119 |   let MkIORes v w := prim__ep_readEventFile f w
120 |    in case v of
121 |         0 => getErr w
122 |         n => MkIORes (Right n) w
123 |
124 | ||| Creates and finally closes and event file descriptor.
125 | export
126 | withEv : Bits64 -> Flags -> (EventFD -> PrimIO a) -> PrimIO a
127 | withEv i fs f w =
128 |   let MkIORes ev  w := eventfd i fs w
129 |       MkIORes res w := f ev w
130 |       MkIORes _   w := close ev w
131 |    in MkIORes res w
132 |