Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hotfix bound threads for workers unsafe calls for llvm #4081

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions booster/library/Booster/LLVM/TH.hs
Original file line number Diff line number Diff line change
Expand Up @@ -89,9 +89,9 @@ foreignImport name' ty' = do
libHandle <- TH.newName "libHandle"

pure
[ -- foreign import ccall "dynamic" <camel_name>Unwrap :: FunPtr <ty> -> <ty>
[ -- foreign import ccall unsafe "dynamic" <camel_name>Unwrap :: FunPtr <ty> -> <ty>
TH.ForeignD $
TH.ImportF TH.CCall TH.Safe "dynamic" nameUnwrap $
TH.ImportF TH.CCall TH.Unsafe "dynamic" nameUnwrap $
TH.AppT (TH.AppT TH.ArrowT $ TH.AppT (TH.ConT ''FunPtr) ty) ty
, -- <camel_name>FunPtr :: ReaderT DL IO (FunPtr <ty>)
TH.SigD
Expand Down
1 change: 1 addition & 0 deletions booster/tools/booster/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -334,6 +334,7 @@ main = do
server =
jsonRpcServer
srvSettings
(isJust mLlvmLibrary) -- run with bound threads if LLVM API in use
( \rawReq req ->
let reqId = getReqId rawReq
in runBoosterLogger $ do
Expand Down
3 changes: 2 additions & 1 deletion dev-tools/booster-dev/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ import Control.Monad.Trans.Reader (runReaderT)
import Data.Conduit.Network (serverSettings)
import Data.Map (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (fromMaybe, isNothing)
import Data.Maybe (fromMaybe, isJust, isNothing)
import Data.Text (Text, unpack)
import Data.Text.Encoding qualified as Text
import Options.Applicative
Expand Down Expand Up @@ -163,6 +163,7 @@ runServer port definitions defaultMain mLlvmLibrary rewriteOpts logFile mSMTOpti
}
jsonRpcServer
(serverSettings port "*")
(isJust mLlvmLibrary) -- run in bound threads if LLVM library in use
( \rawReq req ->
flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions)
. Booster.Log.unLoggerT
Expand Down
1 change: 1 addition & 0 deletions dev-tools/kore-rpc-dev/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -240,6 +240,7 @@ main = do
server =
jsonRpcServer
srvSettings
False -- no bound threads
(\rawReq -> runBoosterLogger . respond (koreRespond $ getReqId rawReq))
[Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
interruptHandler _ = do
ehildenb marked this conversation as resolved.
Show resolved Hide resolved
Expand Down
15 changes: 10 additions & 5 deletions kore-rpc-types/src/Kore/JsonRpc/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Kore.JsonRpc.Server (
JsonRpcHandler (..),
) where

import Control.Concurrent (forkIO, throwTo)
import Control.Concurrent (forkIO, forkOS, throwTo)
import Control.Concurrent.STM.TChan (newTChan, readTChan, writeTChan)
import Control.Exception (Exception (fromException), catch, mask, throw)
import Control.Monad (forever)
Expand Down Expand Up @@ -78,11 +78,14 @@ jsonRpcServer ::
(MonadUnliftIO m, FromRequestCancellable q, ToJSON r) =>
-- | Connection settings
ServerSettings ->
-- | run workers in bound threads (required if worker below uses
-- foreign calls with thread-local state)
Bool ->
-- | Action to perform on connecting client thread
(Request -> Respond q IO r) ->
[JsonRpcHandler] ->
m a
jsonRpcServer serverSettings respond handlers =
jsonRpcServer serverSettings runBound respond handlers =
runGeneralTCPServer serverSettings $ \cl ->
Log.runNoLoggingT $
runJSONRPCT
Expand All @@ -93,17 +96,18 @@ jsonRpcServer serverSettings respond handlers =
False
(appSink cl)
(appSource cl)
(srv respond handlers)
(srv runBound respond handlers)

data JsonRpcHandler = forall e. Exception e => JsonRpcHandler (e -> IO ErrorObj)

srv ::
forall m q r.
(MonadLoggerIO m, FromRequestCancellable q, ToJSON r) =>
Bool ->
(Request -> Respond q IO r) ->
[JsonRpcHandler] ->
JSONRPCT m ()
srv respond handlers = do
srv runBound respond handlers = do
reqQueue <- liftIO $ atomically newTChan
let mainLoop tid =
let loop =
Expand Down Expand Up @@ -170,7 +174,8 @@ srv respond handlers = do
restore (thing a) `catch` catchesHandler a

liftIO $
forkIO $
-- workers should run in bound threads (to secure foreign calls) when flagged
(if runBound then forkOS else forkIO) $
forever $
bracketOnReqException
(atomically $ readTChan reqQueue)
Expand Down
1 change: 1 addition & 0 deletions kore/src/Kore/JsonRpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -731,6 +731,7 @@ runServer port serverState mainModule runSMT Log.LoggerEnv{logAction} = do
flip runLoggingT logFun $
jsonRpcServer
srvSettings
False -- no bound threads
( \req parsed ->
log (InfoJsonRpcProcessRequest (getReqId req) parsed)
>> respond (fromId $ getReqId req) serverState mainModule runSMT parsed
Expand Down
Loading