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 server #3704

Merged
merged 10 commits into from
Dec 14, 2023
Merged

Concurrent kore-rpc server #3704

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
01a5876
return module ids for add-module
goodlyrottenapple Dec 12, 2023
0248a44
short-circuit if the module already exists in indexedModules map
goodlyrottenapple Dec 12, 2023
721c7ef
move new DuplicateModule error to the end so as to not change the err…
goodlyrottenapple Dec 12, 2023
c2ed4ae
use take/putMVar to prevent concurrency bugs when two threads try to …
goodlyrottenapple Dec 13, 2023
be69ad7
fix add-module rpc test
goodlyrottenapple Dec 13, 2023
35f014e
add name-as-id
goodlyrottenapple Dec 13, 2023
e036e7e
only verify the module once and then make a copy with original name i…
goodlyrottenapple Dec 13, 2023
20ba138
Format with fourmolu
invalid-email-address Dec 13, 2023
be0240b
make add-module idempotent when the content is exactly the same even …
goodlyrottenapple Dec 14, 2023
b469495
Format with fourmolu
invalid-email-address Dec 14, 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.freeze
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ constraints: any.Cabal ==3.6.3.0,
any.json-rpc ==1.0.4,
any.junit-xml ==0.1.0.2,
any.kan-extensions ==5.2.5,
kore -threaded,
kore +threaded,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libyaml ==0.1.2,
Expand Down
1 change: 1 addition & 0 deletions kore-rpc-types/src/Kore/JsonRpc/Error.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ data JsonRpcBackendError
| SmtSolverError
| Aborted
| MultipleStates
| DuplicateModule
deriving stock (Enum, Show)

backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj
Expand Down
3 changes: 2 additions & 1 deletion kore-rpc-types/src/Kore/JsonRpc/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,11 +75,12 @@ data SimplifyRequest = SimplifyRequest

data AddModuleRequest = AddModuleRequest
{ _module :: Text
, nameAsId :: !(Maybe Bool)
}
deriving stock (Generic, Show, Eq)
deriving
(FromJSON, ToJSON)
via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleRequest
via CustomJSON '[FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleRequest

data GetModelRequest = GetModelRequest
{ state :: KoreJson
Expand Down
127 changes: 78 additions & 49 deletions kore/src/Kore/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@ module Kore.JsonRpc (
) where

import Control.Concurrent.MVar qualified as MVar
import Control.Monad.Except (runExceptT)
import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, withExceptT)
import Control.Monad.Logger (runLoggingT)
import Control.Monad.Trans.Except (catchE)
import Crypto.Hash (SHA256 (..), hashWith)
import Data.Aeson.Types (ToJSON (..))
import Data.Coerce (coerce)
import Data.Conduit.Network (serverSettings)
Expand All @@ -23,7 +25,9 @@ import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Sequence as Seq (Seq, empty)
import Data.Set qualified as Set
import Data.String (fromString)
import Data.Text (Text)
import Data.Text.Encoding (encodeUtf8)
import GlobalMain (
LoadedDefinition (..),
SerializedDefinition (..),
Expand Down Expand Up @@ -455,54 +459,79 @@ respond serverState moduleName runSMT =
OrPattern.toTermLike sort result
, logs = allLogs
}
AddModule AddModuleRequest{_module} ->
case parseKoreModule "<add-module>" _module of
Left err -> pure $ Left $ backendError CouldNotParsePattern err
Right parsedModule@Module{moduleName = name} -> do
LoadedDefinition{indexedModules, definedNames, kFileLocations} <-
liftIO $ loadedDefinition <$> MVar.readMVar serverState
let verified =
verifyAndIndexDefinitionWithBase
(indexedModules, definedNames)
Builtin.koreVerifiers
(Definition (def @Attributes) [parsedModule])
case verified of
Left err -> pure $ Left $ backendError CouldNotVerifyPattern err
Right (indexedModules', definedNames') ->
case Map.lookup (coerce name) indexedModules' of
Nothing -> pure $ Left $ backendError CouldNotFindModule name
Just mainModule -> do
let metadataTools = MetadataTools.build mainModule
lemmas = getSMTLemmas mainModule
serializedModule' <-
liftIO
. runSMT metadataTools lemmas
$ Exec.makeSerializedModule mainModule
internedTextCache <- liftIO $ readIORef globalInternedTextCache

liftIO . MVar.modifyMVar_ serverState $
\ServerState{serializedModules} -> do
let serializedDefinition =
SerializedDefinition
{ serializedModule = serializedModule'
, locations = kFileLocations
, internedTextCache
, lemmas
}
loadedDefinition =
LoadedDefinition
{ indexedModules = indexedModules'
, definedNames = definedNames'
, kFileLocations
}
pure
ServerState
{ serializedModules =
Map.insert (coerce name) serializedDefinition serializedModules
, loadedDefinition
}

pure . Right . AddModule $ AddModuleResult (getModuleName name)
AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
let nameAsId = fromMaybe False nameAsId'
parsedModule@Module{moduleName = name} <-
withExceptT (backendError CouldNotParsePattern) $
liftEither $
parseKoreModule "<add-module>" _module
st@ServerState
{ serializedModules
, loadedDefinition = LoadedDefinition{indexedModules, definedNames, kFileLocations}
} <-
liftIO $ MVar.takeMVar serverState
let moduleHash = ModuleName . fromString . ('m' :) . show . hashWith SHA256 $ encodeUtf8 _module

-- put the original state back if we fail at any point
flip catchE (\e -> liftIO (MVar.putMVar serverState st) >> throwError e) $ do
when (nameAsId && isJust (Map.lookup (coerce name) indexedModules)) $
throwError $
backendError DuplicateModule name

case Map.lookup (coerce moduleHash) indexedModules of
Just{} -> do
-- the module already exists so we don't need to add it again
liftIO $ MVar.putMVar serverState st
pure . AddModule $ AddModuleResult (getModuleName moduleHash)
Nothing -> do
(newIndexedModules, newDefinedNames) <-
withExceptT (backendError CouldNotVerifyPattern) $
liftEither $
verifyAndIndexDefinitionWithBase
(indexedModules, definedNames)
Builtin.koreVerifiers
(Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])

newModule <-
liftEither $
maybe (Left $ backendError CouldNotFindModule moduleHash) Right $
Map.lookup (coerce moduleHash) newIndexedModules

let metadataTools = MetadataTools.build newModule
lemmas = getSMTLemmas newModule
serializedModule <-
liftIO
. runSMT metadataTools lemmas
$ Exec.makeSerializedModule newModule
internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache

let serializedDefinition =
SerializedDefinition
{ serializedModule = serializedModule
, locations = kFileLocations
, internedTextCache = internedTextCacheHash
, lemmas = lemmas
}
newSerializedModules =
Map.fromList $
if nameAsId
then [(coerce moduleHash, serializedDefinition), (coerce name, serializedDefinition)]
else [(coerce moduleHash, serializedDefinition)]
loadedDefinition =
LoadedDefinition
{ indexedModules = (if nameAsId then Map.insert (coerce name) newModule else id) newIndexedModules
, definedNames = newDefinedNames
, kFileLocations
}

liftIO . MVar.putMVar serverState $
ServerState
{ serializedModules =
serializedModules `Map.union` newSerializedModules
, loadedDefinition
}

pure . AddModule $ AddModuleResult (getModuleName moduleHash)
GetModel GetModelRequest{state, _module} ->
withMainModule (coerce _module) $ \serializedModule lemmas ->
case verifyIn serializedModule state of
Expand Down
3 changes: 2 additions & 1 deletion test/rpc-server/add-module/add/params.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{
"module" : "module NEW\n import TEST []\n\n// rule `<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"d\",\"State\"))~>_DotVar1),_DotVar0)=>`<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859), label(NEW.DE), org.kframework.attributes.Location(Location(10,14,10,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule3LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"d\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.DE\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(10,14,10,33)\")]\n\n// rule `<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0)=>`<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"f\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(326083bfd90582092d450c8db2c16552b080ed66344a5d424a189caab7fe33ef), label(NEW.EF), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule4LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"f\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.EF\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(11,14,11,33)\")]\n\n\nendmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(3,1,13,10)\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\")]\n"
"module" : "module NEW\n import TEST []\n\n// rule `<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"d\",\"State\"))~>_DotVar1),_DotVar0)=>`<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859), label(NEW.DE), org.kframework.attributes.Location(Location(10,14,10,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule3LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"d\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.DE\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(10,14,10,33)\")]\n\n// rule `<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0)=>`<generatedTop>`(`<k>`(inj{State,KItem}(#token(\"f\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(326083bfd90582092d450c8db2c16552b080ed66344a5d424a189caab7fe33ef), label(NEW.EF), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule4LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"f\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.EF\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(11,14,11,33)\")]\n\n\nendmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(3,1,13,10)\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\")]\n",
"name-as-id": true
}
2 changes: 1 addition & 1 deletion test/rpc-server/add-module/add/response.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"jsonrpc":"2.0","id":1,"result":{"module":"NEW"}}
{"jsonrpc":"2.0","id":1,"result":{"module":"m8e723e34b156f187e7cce8658dbb513244788a1ab81c1f496b909b1a2d1cc0c3"}}
Loading