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.

Sign up for GitHub

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

Concurrent kore-rpc-booster #414

Closed
wants to merge 4 commits into from
Closed

Concurrent kore-rpc-booster #414

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
ff4c45f
update json rpc server
goodlyrottenapple Dec 7, 2023
3ae8383
chain multiple calls in rpc-client
goodlyrottenapple Dec 7, 2023
e5cb3f6
format
goodlyrottenapple Dec 7, 2023
6bef957
Merge branch 'main' into sam/concurrent-booster
goodlyrottenapple Dec 8, 2023
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
2 changes: 1 addition & 1 deletion cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,6 @@ source-repository-package
source-repository-package
type: git
location: https://github.com/runtimeverification/haskell-backend.git
tag: a5847301404583e16d55cd4d051b8e605d704fbc
tag: 67a4029caef9474009c24f648a5d2b61ecfb37f1
--sha256:
subdir: kore kore-rpc-types
69 changes: 1 addition & 68 deletions cabal.project.freeze
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,23 +5,16 @@ constraints: any.Cabal ==3.6.3.0,
any.OneTuple ==0.3.1,
any.Only ==0.1,
any.QuickCheck ==2.14.3,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.adjunctions ==4.4.2,
any.aeson ==2.0.3.0,
aeson -cffi +ordered-keymap,
any.aeson-pretty ==0.8.9,
aeson-pretty -lib-only,
any.ansi-terminal ==0.11.4,
ansi-terminal -example +win32-2-13-1,
any.ansi-wl-pprint ==0.6.9,
ansi-wl-pprint -example,
any.array ==0.5.4.0,
any.assoc ==1.0.2,
any.async ==2.2.4,
async -bench,
any.attoparsec ==0.14.4,
attoparsec -developer,
any.auto-update ==0.1.6,
any.barbies ==2.0.4.0,
any.base ==4.16.4.0,
Expand All @@ -31,52 +24,37 @@ constraints: any.Cabal ==3.6.3.0,
any.base16 ==0.3.2.1,
any.basement ==0.0.16,
any.bifunctors ==5.5.15,
bifunctors +semigroups +tagged,
any.binary ==0.8.9.0,
any.blaze-builder ==0.4.2.2,
any.blaze-html ==0.9.1.2,
any.blaze-markup ==0.8.2.8,
any.blaze-textual ==0.2.3.1,
blaze-textual -developer -integer-simple +native,
any.boring ==0.2.1,
boring +tagged,
any.bytebuild ==0.3.13.0,
bytebuild -checked,
any.byteslice ==0.2.7.0,
byteslice +avoid-rawmemchr,
any.bytesmith ==0.3.9.1,
any.bytestring ==0.11.4.0,
any.bz2 ==1.0.1.0,
bz2 -cross +with-bzlib,
any.c2hs ==0.28.8,
c2hs +base3 -regression,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.casing ==0.1.4.1,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.cereal-conduit ==0.8.0,
any.chronos ==1.1.5,
any.clock ==0.8.3,
clock -llvm,
any.cmdargs ==0.10.22,
cmdargs +quotation -testprog,
any.co-log ==0.5.0.0,
any.co-log-core ==0.3.2.0,
any.colour ==2.3.6,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-output ==1.10.18,
any.conduit ==1.3.5,
any.conduit-extra ==1.3.6,
any.constraints ==0.13.4,
any.containers ==0.6.5.1,
any.contiguous ==0.6.3.0,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cryptonite ==0.30,
cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes,
any.data-array-byte ==0.1.0.1,
any.data-default ==0.7.1.1,
any.data-default-class ==0.1.2.0,
Expand All @@ -88,22 +66,17 @@ constraints: any.Cabal ==3.6.3.0,
any.deepseq ==1.4.6.1,
any.deriving-aeson ==0.2.9,
any.direct-sqlite ==2.3.28,
direct-sqlite +fulltextsearch +haveusleep +json1 -systemlib +urifilenames,
any.directory ==1.3.6.2,
any.distributive ==0.6.2.1,
distributive +semigroups +tagged,
any.dlist ==1.0,
dlist -werror,
any.easy-file ==0.2.5,
any.entropy ==0.4.1.10,
entropy -donotgetentropy,
any.erf ==2.0.0.0,
any.errors ==2.3.0,
any.exceptions ==0.10.4,
any.extra ==1.7.13,
any.fast-logger ==3.1.2,
any.fgl ==5.7.0.3,
fgl +containers042,
any.filepath ==1.4.2.2,
any.free ==5.1.10,
any.generic-lens ==2.2.2.0,
Expand All @@ -120,13 +93,9 @@ constraints: any.Cabal ==3.6.3.0,
any.ghci ==9.2.8,
any.gitrev ==1.3.1,
any.graphviz ==2999.20.1.0,
graphviz -test-parsing,
any.hashable ==1.4.2.0,
hashable +integer-gmp -random-initial-seed,
any.hashtables ==1.3.1,
hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks,
any.haskeline ==0.8.2.1,
haskeline +examples +terminfo,
any.haskell-lexer ==1.1.1,
any.haskell-src-exts ==1.23.1,
any.haskell-src-meta ==0.8.12,
Expand All @@ -145,7 +114,6 @@ constraints: any.Cabal ==3.6.3.0,
any.indexed-traversable-instances ==0.1.1.2,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.intern ==0.9.4,
any.invariant ==0.6.1,
any.json-rpc ==1.0.4,
Expand All @@ -155,52 +123,40 @@ constraints: any.Cabal ==3.6.3.0,
kore +threaded,
any.kore-rpc-types ==0.60.0.0,
any.language-c ==0.9.2,
language-c -allwarnings +iecfpextension +usebytestrings,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libyaml ==0.1.2,
libyaml -no-unicode -system-libyaml,
any.lifted-async ==0.10.2.4,
any.lifted-base ==0.2.3.12,
any.logict ==0.8.0.0,
any.loop ==0.3.0,
any.markdown-unlit ==0.5.1,
any.math-functions ==0.3.4.2,
math-functions +system-erf +system-expm1,
any.matrix ==0.3.6.1,
any.megaparsec ==9.2.2,
megaparsec -dev,
any.memory ==0.17.0,
memory +support_bytestring +support_deepseq,
any.mmorph ==1.2.0,
any.monad-control ==1.0.3.1,
any.monad-logger ==0.3.40,
monad-logger +template_haskell,
any.monad-loops ==0.4.3,
monad-loops +base4,
any.monad-validate ==1.2.0.1,
any.mono-traversable ==1.0.15.3,
any.mtl ==2.2.2,
any.multiset ==0.3.4.3,
any.mwc-random ==0.15.0.2,
any.natural-arithmetic ==0.1.4.0,
any.network ==3.1.4.0,
network -devel,
any.network-run ==0.2.5,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.3,
any.optparse-applicative ==0.17.1.0,
optparse-applicative +process,
any.parallel ==3.2.2.0,
any.parsec ==3.1.15.0,
any.parser-combinators ==1.3.0,
parser-combinators -dev,
any.polyparse ==1.13,
any.pqueue ==1.4.3.0,
any.pretty ==1.1.3.6,
any.pretty-show ==1.10,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.primitive ==0.7.3.0,
any.primitive-addr ==0.1.0.2,
any.primitive-offset ==0.2.0.0,
Expand All @@ -210,9 +166,7 @@ constraints: any.Cabal ==3.6.3.0,
any.quickcheck-io ==0.2.0,
any.random ==1.2.1.1,
any.recursion-schemes ==5.2.2.4,
recursion-schemes +template-haskell,
any.reflection ==2.1.7,
reflection -slow +template-haskell,
any.regex-base ==0.94.0.2,
any.regex-pcre-builtin ==0.95.2.3.8.44,
any.resourcet ==1.2.6,
Expand All @@ -221,36 +175,27 @@ constraints: any.Cabal ==3.6.3.0,
any.safe ==0.3.19,
any.safe-exceptions ==0.1.7.3,
any.scientific ==0.3.7.0,
scientific -bytestring-builder -integer-simple,
any.secp256k1-haskell ==0.6.1,
any.semialign ==1.2.0.1,
semialign +semigroupoids,
any.semigroupoids ==5.3.7,
semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers,
any.semigroups ==0.20,
semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers,
any.setenv ==0.1.1.3,
any.smtlib-backends ==0.3,
any.smtlib-backends-process ==0.3,
any.sop-core ==0.5.0.2,
any.split ==0.2.3.5,
any.splitmix ==0.1.0.4,
splitmix -optimised-mixer,
any.sqlite-simple ==0.4.18.2,
any.stm ==2.5.0.2,
any.stm-chans ==3.0.0.9,
any.stm-conduit ==4.0.1,
any.streaming-commons ==0.2.2.6,
streaming-commons -use-bytestring-builder,
any.streams ==3.3.2,
any.strict ==0.4.0.1,
strict +assoc,
any.string-conversions ==0.4.0.1,
any.syb ==0.7.2.3,
any.tagged ==0.8.6.1,
tagged +deepseq +transformers,
any.tar ==0.5.1.1,
tar -old-bytestring -old-time,
any.tasty ==1.4.3,
tasty +unix,
any.tasty-discover ==5.0.0,
Expand All @@ -265,7 +210,6 @@ constraints: any.Cabal ==3.6.3.0,
any.terminfo ==0.4.1.5,
any.text ==1.2.5.0,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.4.5.0,
any.th-compat ==0.1.4,
Expand All @@ -274,45 +218,34 @@ constraints: any.Cabal ==3.6.3.0,
any.th-orphans ==0.13.14,
any.th-reify-many ==0.1.10,
any.these ==1.1.1.1,
these +assoc,
any.time ==1.11.1.1,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.torsor ==0.1,
any.transformers ==0.5.6.2,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.tuples ==0.1.0.0,
any.type-equality ==1,
any.typed-process ==0.2.11.0,
any.typerep-map ==0.5.0.0,
any.unix ==2.7.2.2,
any.unix-compat ==0.5.4,
unix-compat -old-time,
any.unix-time ==0.4.9,
any.unliftio ==0.2.25.0,
any.unliftio-core ==0.2.1.0,
any.unordered-containers ==0.2.19.1,
unordered-containers -debug,
any.utf8-string ==1.0.2,
any.uuid-types ==1.0.5,
any.vector ==0.12.3.1,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.8.0.4,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.void ==0.7.3,
void -safe,
any.wide-word ==0.1.5.0,
any.witherable ==0.4.2,
any.wl-pprint-annotated ==0.1.0.1,
any.wl-pprint-text ==1.2.0.2,
any.xml-conduit ==1.9.1.2,
any.xml-types ==0.3.8,
any.yaml ==0.11.11.1,
yaml +no-examples +no-exe,
any.zigzag ==0.0.1.0,
any.zlib ==0.6.3.0,
zlib -bundled-c-zlib -non-blocking-ffi -pkg-config
any.zlib ==0.6.3.0
index-state: hackage.haskell.org 2023-06-28T20:31:18Z
43 changes: 22 additions & 21 deletions dev-tools/kore-rpc-dev/Server.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ License : BSD-3-Clause
module Main (main) where

import Control.Concurrent.MVar (newMVar)
import Control.Concurrent.MVar qualified as MVar

import Control.Exception (AsyncException (UserInterrupt), handleJust)
import Control.Monad (forM_, void, when)
import Control.Monad.Catch (bracket)
Expand All @@ -24,6 +24,7 @@ import Control.Monad.Logger (
import Control.Monad.Logger qualified as Log
import Control.Monad.Logger qualified as Logger
import Data.Aeson.Types (Value (..))
import Data.Bifunctor (second)
import Data.Conduit.Network (serverSettings)
import Data.IORef (writeIORef)
import Data.InternedText (globalInternedTextCache)
Expand Down Expand Up @@ -76,7 +77,7 @@ import Options.SMT as KoreSMT (KoreSolverOptions (..), Solver (..))
import SMT qualified as KoreSMT

data KoreServer = KoreServer
{ serverState :: MVar.MVar Kore.ServerState
{ serverState :: Kore.ServerState
, mainModule :: Text
, runSMT ::
forall a.
Expand All @@ -88,17 +89,17 @@ data KoreServer = KoreServer
}

respond ::
forall m.
forall m s.
Log.MonadLogger m =>
Respond (API 'Req) m (API 'Res) ->
Respond (API 'Req) m (API 'Res)
Respond (API 'Req) m (API 'Res, Maybe s) ->
Respond (API 'Req) m (API 'Res, Maybe s)
respond kore req = case req of
Execute _ ->
loggedKore ExecuteM req >>= \case
Right (Execute koreResult) -> do
Right (Execute koreResult, _) -> do
Log.logInfoNS "proxy" . Text.pack $
"Kore " <> show koreResult.reason <> " at " <> show koreResult.depth
pure . Right . Execute $ koreResult
pure . Right . (,Nothing) . Execute $ koreResult
res -> pure res
Implies _ -> loggedKore ImpliesM req
Simplify simplifyReq -> handleSimplify simplifyReq
Expand All @@ -108,19 +109,19 @@ respond kore req = case req of
Cancel ->
pure $ Left $ ErrorObj "Cancel not supported" (-32601) Null
where
handleSimplify :: SimplifyRequest -> m (Either ErrorObj (API 'Res))
handleSimplify :: SimplifyRequest -> m (Either ErrorObj (API 'Res, Maybe s))
handleSimplify simplifyReq = do
let koreReq = Simplify simplifyReq
koreResult <- kore koreReq
case koreResult of
Right (Simplify koreRes) -> do
pure . Right . Simplify $
Right (Simplify koreRes, _) -> do
pure . Right . (,Nothing) . Simplify $
SimplifyResult
{ state = koreRes.state
, logs = koreRes.logs
}
koreError ->
pure koreError
pure $ second (const Nothing) <$> koreError

loggedKore method r = do
Log.logInfoNS "proxy" . Text.pack $ show method <> " (using kore)"
Expand Down Expand Up @@ -174,12 +175,14 @@ main = do
kore@KoreServer{runSMT} <- mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
runLoggingT (Logger.logInfoNS "proxy" "Starting RPC server") monadLogger

let koreRespond :: Respond (API 'Req) (LoggingT IO) (API 'Res)
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
let koreRespond ::
Kore.ServerState -> Respond (API 'Req) (LoggingT IO) (API 'Res, Maybe Kore.ServerState)
koreRespond s = Kore.respond s (ModuleName kore.mainModule) runSMT
server =
jsonRpcServer
srvSettings
(const $ respond koreRespond)
kore.serverState
(\_rawReq s -> respond (koreRespond s))
[handleErrorCall, handleSomeException]
interruptHandler _ = do
when (logLevel >= LevelInfo) $
Expand Down Expand Up @@ -264,13 +267,11 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
liftIO $ writeIORef globalInternedTextCache internedTextCache

loadedDefinition <- GlobalMain.loadDefinitions [definitionFile]
serverState <-
liftIO $
MVar.newMVar
Kore.ServerState
{ serializedModules = Map.singleton (ModuleName mainModuleName) sd
, loadedDefinition
}
let serverState =
Kore.ServerState
{ serializedModules = Map.singleton (ModuleName mainModuleName) sd
, loadedDefinition
}

pure $
KoreServer
Expand Down
Loading
Loading