Hotfix bound threads for workers unsafe calls for llvm (#4081)

Fixes a problem with recently-introduced thread-local storage in the
LLVM backend.
We have to make sure that all foreign calls relating to an LLVM-based
term evaluation use the same OS thread, which can only be achieved [via
bound
threads](https://downloads.haskell.org/ghc/latest/docs/libraries/base-4.20.0.0-1f57/Control-Concurrent.html#g:8)
.

This PR
* adds a flag to the generic RPC server in `kore-rpc-types` to run
request worker threads in bound threads (using `forkOS`)
* `kore-rpc-booster` uses this flag for bound threads when an LLVM
backend library is used
* declares the LLVM backend calls `unsafe` to make executing OS threads
block instead of having new OS threads created for concurrent Haskell
execution (they won't read HS heap data and never call back into
Haskell).

This _should_ protect us against problems related to using thread-local
storage in the LLVM backend. Needs to be thoroughly tested before
merging, because issues only materialised in proofs with substantial
workload and parallel exploration.

PR #4080 uses `runInBoundThread` on the individual request processing
calls instead of running the whole worker thread in the server as a
bound thread. This was not solving the problem.

Author: jberthold

booster/library/Booster/LLVM/TH.hs

@@ -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

booster/tools/booster/Server.hs

@@ -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

dev-tools/booster-dev/Server.hs

@@ -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
@@ -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

dev-tools/kore-rpc-dev/Server.hs

@@ -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

kore-rpc-types/src/Kore/JsonRpc/Server.hs

@@ -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)
@@ -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
@@ -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 =
@@ -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)

kore/src/Kore/JsonRpc.hs

@@ -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