Skip to content

Commit

Permalink
Remove mutex around LLVM calls from booster
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
jberthold committed Jan 17, 2025
1 parent f6e0f33 commit 070305f
Showing 1 changed file with 3 additions and 7 deletions.
10 changes: 3 additions & 7 deletions booster/library/Booster/LLVM/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ module Booster.LLVM.Internal (
LlvmError (..),
) where

import Control.Concurrent.MVar (MVar, newMVar, withMVar)
import Control.Exception (IOException)
import Control.Monad (foldM, forM_, void, (>=>))
import Control.Monad.Catch (MonadCatch, MonadMask, MonadThrow, catch)
Expand Down Expand Up @@ -104,21 +103,19 @@ data API = API
, simplifyBool :: KorePatternPtr -> IO (Either LlvmError Bool)
, simplify :: KorePatternPtr -> KoreSortPtr -> IO (Either LlvmError ByteString)
, collect :: IO ()
, mutex :: MVar ()
}

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

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

runLLVM :: API -> LLVM a -> IO a
runLLVM api (LLVM m) =
withMVar api.mutex $ const $ runReaderT m api
runLLVM api (LLVM m) = runReaderT m api

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

mutex <- liftIO $ newMVar ()
pure API{patt, symbol, sort, simplifyBool, simplify, collect, mutex}
pure API{patt, symbol, sort, simplifyBool, simplify, collect}

ask :: LLVM API
ask = LLVM Reader.ask
Expand Down

0 comments on commit 070305f

Please sign in to comment.