Skip to content

Commit 8d90457

Browse files
committed
Remove mutex around LLVM calls from booster
Previously the LLVM backend was not thread-safe so the simplification calls had to be sequentialised for concurrent RPC requests. Since thread-local storage is now used, the calls can be executed concurrently/in parallel using multiple cores. This PR removes the mutex that sequentialised the calls before.
1 parent f6e0f33 commit 8d90457

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

booster/library/Booster/LLVM/Internal.hs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -104,21 +104,19 @@ data API = API
104104
, simplifyBool :: KorePatternPtr -> IO (Either LlvmError Bool)
105105
, simplify :: KorePatternPtr -> KoreSortPtr -> IO (Either LlvmError ByteString)
106106
, collect :: IO ()
107-
, mutex :: MVar ()
108107
}
109108

110109
newtype LLVM a = LLVM (ReaderT API IO a)
111110
deriving newtype (Functor, Applicative, Monad, MonadIO, MonadThrow, MonadCatch, MonadMask)
112111

113-
{- | Uses dlopen to load a .so/.dylib C library at runtime. For doucmentation of flags such as `RTL_LAZY`, consult e.g.
112+
{- | Uses dlopen to load a .so/.dylib C library at runtime. For documentation of flags such as `RTL_LAZY`, consult e.g.
114113
https://man7.org/linux/man-pages/man3/dlopen.3.html
115114
-}
116115
withDLib :: FilePath -> (Linker.DL -> IO a) -> IO a
117116
withDLib dlib = Linker.withDL dlib [Linker.RTLD_LAZY]
118117

119118
runLLVM :: API -> LLVM a -> IO a
120-
runLLVM api (LLVM m) =
121-
withMVar api.mutex $ const $ runReaderT m api
119+
runLLVM api (LLVM m) = runReaderT m api
122120

123121
mkAPI :: Linker.DL -> IO API
124122
mkAPI dlib = flip runReaderT dlib $ do
@@ -282,8 +280,7 @@ mkAPI dlib = flip runReaderT dlib $ do
282280
stderr
283281
"[Warn] Using an LLVM backend compiled with --llvm-mutable-bytes (unsound byte array semantics)"
284282

285-
mutex <- liftIO $ newMVar ()
286-
pure API{patt, symbol, sort, simplifyBool, simplify, collect, mutex}
283+
pure API{patt, symbol, sort, simplifyBool, simplify, collect}
287284

288285
ask :: LLVM API
289286
ask = LLVM Reader.ask

0 commit comments

Comments
 (0)