diff options
| -rw-r--r-- | source/Api.hs | 98 | ||||
| -rw-r--r-- | source/Checking/Declaration.hs | 142 | ||||
| -rw-r--r-- | source/Provers.hs | 939 | ||||
| -rw-r--r-- | source/Test/Unit/Provers.hs | 326 |
4 files changed, 1193 insertions, 312 deletions
diff --git a/source/Api.hs b/source/Api.hs index 2220434..25359da 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -420,12 +420,18 @@ data VerificationMeasurements = VerificationMeasurements , verificationPreparedObligationCount :: !Int , verificationMaximumObligationBatchSize :: !Int , verificationPreparedRequestBytes :: !Word64 + , verificationRequestPreparationNanoseconds :: !Word64 , verificationVampireRunCount :: !Int , verificationModuleRootHitCount :: !Int , verificationModuleRootMissCount :: !Int , verificationFirstVampireStartNanoseconds :: !(Maybe Word64) + , verificationFinalVampireSubmissionNanoseconds + :: !(Maybe Word64) + , verificationFinalVampireCompletionNanoseconds + :: !(Maybe Word64) , verificationVampireExecutionNanoseconds :: !Word64 + , verificationLongestVampireExecutionNanoseconds :: !Word64 } deriving (Show, Eq) @@ -442,11 +448,15 @@ data VerificationObservation = VerificationObservation , observedPreparedObligationCount :: !Int , observedMaximumObligationBatchSize :: !Int , observedPreparedRequestBytes :: !Word64 + , observedRequestPreparationNanoseconds :: !Word64 , observedVampireRunCount :: !Int , observedModuleRootHitCount :: !Int , observedModuleRootMissCount :: !Int , observedFirstVampireStart :: !(Maybe Word64) + , observedFinalVampireSubmission :: !(Maybe Word64) + , observedFinalVampireCompletion :: !(Maybe Word64) , observedVampireExecutionNanoseconds :: !Word64 + , observedLongestVampireExecutionNanoseconds :: !Word64 } initialVerificationObservation :: VerificationObservation @@ -464,11 +474,15 @@ initialVerificationObservation = , observedPreparedObligationCount = 0 , observedMaximumObligationBatchSize = 0 , observedPreparedRequestBytes = 0 + , observedRequestPreparationNanoseconds = 0 , observedVampireRunCount = 0 , observedModuleRootHitCount = 0 , observedModuleRootMissCount = 0 , observedFirstVampireStart = Nothing + , observedFinalVampireSubmission = Nothing + , observedFinalVampireCompletion = Nothing , observedVampireExecutionNanoseconds = 0 + , observedLongestVampireExecutionNanoseconds = 0 } newtype VerificationRequestObserver = VerificationRequestObserver @@ -855,12 +869,6 @@ verifyMeasuredThrowingWithStore . VerificationFoundationManifestError) pure Foundation.checkedFoundation - preludeResolver <- - typedVampireResolver - runInIO - executor - 0 - observationRef preparationStart <- getMonotonicTimeNSec prepared <- prepareDefaultSourceRequest file @@ -869,7 +877,13 @@ verifyMeasuredThrowingWithStore pure let (mounts, request) = prepared preparationEnd <- getMonotonicTimeNSec - prelude <- + prelude <- withVampireRequestOwner executor \owner -> do + preludeResolver <- + typedVampireResolver + runInIO + owner + 0 + observationRef Typed.acquireFinalPreludeSession memo store foundation preludeResolver >>= either @@ -1150,7 +1164,8 @@ checkTypedWorkspace sealedByAddress candidate - checkModule task sealedByAddress = do + checkModule task sealedByAddress = + withVampireRequestOwner executor \requestOwner -> do let parsed = moduleTaskParsed task source = Felix.parsedModuleResolved parsed address = Felix.parsedModuleAddress parsed @@ -1167,7 +1182,7 @@ checkTypedWorkspace resolver <- typedVampireResolver runInIO - executor + requestOwner (moduleTaskOrdinal task) observationRef input <- @@ -1481,14 +1496,15 @@ typedVampireResolver :: forall io . (MonadIO io, MonadLogger io) => (forall value. io value -> IO value) - -> VampireExecutor + -> VampireRequestOwner -> Natural -> IORef VerificationObservation -> IO Declaration.VampireResolver typedVampireResolver - runInIO executor moduleOrdinal observationRef = do + runInIO requestOwner moduleOrdinal observationRef = do localOrdinalRef <- newIORef 1 - pure (Declaration.vampireBatchResolver \prepared -> do + pure (Declaration.vampireBatchResolverWithPreparationObserver + (\prepared -> do let batchSize = NonEmpty.length prepared ordinalCount = fromIntegral batchSize firstOrdinal <- atomicModifyIORef' localOrdinalRef @@ -1531,11 +1547,20 @@ typedVampireResolver (\(position, task) -> runInIO (runPreparedTypedProverWithExecutor - executor + requestOwner position task)) (NonEmpty.toList positioned) pure (NonEmpty.fromList results)) + (\elapsed -> + atomicModifyIORef' observationRef \observation -> + ( observation + { observedRequestPreparationNanoseconds = + observedRequestPreparationNanoseconds observation + + elapsed + } + , () + ))) observeModuleRootAcquisition :: IORef VerificationObservation @@ -1610,8 +1635,14 @@ mergeExecutorObservation observationRef executorObserved = vampireExecutorMaximumLiveCount executorObserved , observedFirstVampireStart = vampireExecutorFirstStartNanoseconds executorObserved + , observedFinalVampireSubmission = + vampireExecutorFinalSubmissionNanoseconds executorObserved + , observedFinalVampireCompletion = + vampireExecutorFinalCompletionNanoseconds executorObserved , observedVampireExecutionNanoseconds = vampireExecutorExecutionNanoseconds executorObserved + , observedLongestVampireExecutionNanoseconds = + vampireExecutorLongestExecutionNanoseconds executorObserved } , () ) @@ -1662,6 +1693,8 @@ finalizeVerificationMeasurements observedMaximumObligationBatchSize observation , verificationPreparedRequestBytes = observedPreparedRequestBytes observation + , verificationRequestPreparationNanoseconds = + observedRequestPreparationNanoseconds observation , verificationVampireRunCount = observedVampireRunCount observation , verificationModuleRootHitCount = @@ -1672,8 +1705,18 @@ finalizeVerificationMeasurements fmap (\started -> started - invocationStart) (observedFirstVampireStart observation) + , verificationFinalVampireSubmissionNanoseconds = + fmap + (\submitted -> submitted - invocationStart) + (observedFinalVampireSubmission observation) + , verificationFinalVampireCompletionNanoseconds = + fmap + (\completed -> completed - invocationStart) + (observedFinalVampireCompletion observation) , verificationVampireExecutionNanoseconds = observedVampireExecutionNanoseconds observation + , verificationLongestVampireExecutionNanoseconds = + observedLongestVampireExecutionNanoseconds observation } renderVerificationMeasurements @@ -1764,6 +1807,9 @@ renderVerificationMeasurements measurements = measurements) , "prepared_bytes=" <> renderIntegral (verificationPreparedRequestBytes measurements) + , "request_preparation_ms=" + <> renderNanoseconds + (verificationRequestPreparationNanoseconds measurements) , "vampire_runs=" <> renderIntegral (verificationVampireRunCount measurements) , "module_root_hits=" <> renderIntegral @@ -1780,6 +1826,27 @@ renderVerificationMeasurements measurements = <> renderNanoseconds (verificationVampireExecutionNanoseconds measurements) + , "final_submission_ms=" + <> maybe + "none" + renderNanoseconds + (verificationFinalVampireSubmissionNanoseconds + measurements) + , "final_completion_ms=" + <> maybe + "none" + renderNanoseconds + (verificationFinalVampireCompletionNanoseconds + measurements) + , "vampire_span_ms=" + <> maybe + "none" + renderNanoseconds + (vampireExecutionSpan measurements) + , "longest_vampire_ms=" + <> renderNanoseconds + (verificationLongestVampireExecutionNanoseconds + measurements) , "max_ready_modules=" <> renderIntegral (verificationMaximumReadyModuleCount measurements) @@ -1792,6 +1859,11 @@ renderVerificationMeasurements measurements = parseMeasurements = verificationParseMeasurements measurements + vampireExecutionSpan measured = do + started <- verificationFirstVampireStartNanoseconds measured + completed <- verificationFinalVampireCompletionNanoseconds measured + pure (completed - started) + renderNanoseconds :: Word64 -> Text renderNanoseconds nanoseconds = renderIntegral (nanoseconds `div` 1000000) diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 15c8282..3919630 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -38,6 +38,7 @@ module Checking.Declaration , failModuleDriver , VampireResolver , vampireBatchResolver + , vampireBatchResolverWithPreparationObserver , vampireResolver , Declaration , failDeclaration @@ -436,7 +437,7 @@ forceCommittedBatch (declarationValidationRecordCertificates record) -newtype VampireResolver = VampireResolver +data VampireResolver = VampireResolver { resolveVampireBatch :: forall local origin. NonEmpty @@ -450,6 +451,7 @@ newtype VampireResolver = VampireResolver (Either Provers.ProverProcessError Provers.ProverAnswer)) + , observeVampirePreparationNanoseconds :: !(Word64 -> IO ()) } vampireBatchResolver @@ -466,7 +468,25 @@ vampireBatchResolver Provers.ProverProcessError Provers.ProverAnswer))) -> VampireResolver -vampireBatchResolver = +vampireBatchResolver resolve = + vampireBatchResolverWithPreparationObserver resolve (const (pure ())) + +vampireBatchResolverWithPreparationObserver + :: (forall local origin. + NonEmpty + (Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId) + -> IO + (NonEmpty + (Either + Provers.ProverProcessError + Provers.ProverAnswer))) + -> (Word64 -> IO ()) + -> VampireResolver +vampireBatchResolverWithPreparationObserver = VampireResolver vampireResolver @@ -1985,27 +2005,30 @@ prepareScopedVampireObligationForMode prepareScopedVampireObligationForMode taskMode claimSupport claim scopedLocals auxiliaryTags selection = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get + DriverState resolver builder _prefix _validation <- State.get let closure = logicalBuilderObjectClosure builder globalType = (`lookupCheckedObjectType` closure) - pure do - supportedClaim <- - first VampireObligationClaimProjectionFailed - (Backend.projectSupportedProposition - globalType - claimSupport - claim) - locals <- traverse - (prepareLocal globalType) - scopedLocals - prepareVampireObligationWith - taskMode - builder - closure - supportedClaim - locals - auxiliaryTags - selection + preparation = do + supportedClaim <- + first VampireObligationClaimProjectionFailed + (Backend.projectSupportedProposition + globalType + claimSupport + claim) + locals <- traverse + (prepareLocal globalType) + scopedLocals + prepareVampireObligationWith + taskMode + builder + closure + supportedClaim + locals + auxiliaryTags + selection + State.lift + (Except.liftIO + (measureVampirePreparation resolver preparation)) where prepareLocal globalType (ScopedVampirePremise @@ -2098,6 +2121,32 @@ prepareVampireObligationWith problem) pure (PreparedVampireObligation problem task) +measureVampirePreparation + :: VampireResolver + -> Either + (VampireObligationPreparationError local) + (PreparedVampireObligation local origin) + -> IO + (Either + (VampireObligationPreparationError local) + (PreparedVampireObligation local origin)) +measureVampirePreparation resolver preparation = do + started <- getMonotonicTimeNSec + prepared <- Exception.evaluate (forcePrepared preparation) + finished <- getMonotonicTimeNSec + observeVampirePreparationNanoseconds resolver (finished - started) + pure prepared + where + forcePrepared result = + case result of + Left err -> err `seq` result + Right prepared@(PreparedVampireObligation _ task) -> + let request = Provers.preparedTypedProverRequest task + in Provers.preparedVerificationByteCount request `seq` + Provers.preparedVerificationRequestId request `seq` + prepared `seq` + result + selectVampireFacts :: (ObjectId -> Maybe CoreType) -> LogicalBuilder @@ -2840,35 +2889,39 @@ prepareCurrentCandidateVampire = CandidateProof do closed proposition = embedClosedCore [] (checkedPropositionTerm proposition) - supportedTarget <- - State.lift - (Except.liftEither - (first - (CurrentCandidateVampirePreparationFailed - . VampireObligationClaimProjectionFailed) + resolver = + declarationVampireResolver + (candidateProofDeclaration initial) + preparation = do + supportedTarget <- + first + VampireObligationClaimProjectionFailed (Backend.projectSupportedProposition globalType (Vector.empty :: Vector (Void, CoreType)) - (closed target)))) - locals <- + (closed target)) + locals <- + traverse + (prepareLocal globalType) + (zip [0 :: Natural ..] premises) + prepareVampireObligationWith + Provers.DirectTask + builder + closure + supportedTarget + locals + [] + VampireLocalPremises + preparedResult <- State.lift - (Except.liftEither - (first CurrentCandidateVampirePreparationFailed - (traverse - (prepareLocal globalType) - (zip [0 :: Natural ..] premises)))) + (liftIO + (measureVampirePreparation resolver preparation)) prepared <- State.lift (Except.liftEither - (first CurrentCandidateVampirePreparationFailed - (prepareVampireObligationWith - Provers.DirectTask - builder - closure - supportedTarget - locals - [] - VampireLocalPremises))) + (first + CurrentCandidateVampirePreparationFailed + preparedResult)) pure prepared where prepareLocal globalType (index, CandidatePremise proposition) = do @@ -3223,7 +3276,8 @@ validateAcceptedVampireResult prepared result = do traverse_ (\accepted -> unless - (Provers.acceptedVampireRequest accepted == request) + (Provers.acceptedVampireRequestId accepted + == Provers.preparedVerificationRequestId request) (Except.throwError VampireRequestMismatch)) (either (const Nothing) Provers.provedVampireRun resolved)) result diff --git a/source/Provers.hs b/source/Provers.hs index 941360c..56497f6 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -8,6 +8,7 @@ module Provers , VampireTaskMode(..) , VampireStatus(..) , CanonicalAtpOutcome(..) + , CanonicalAtpRejection(..) , VampireProtocolError(..) , classifyVampireProtocol , vampireStatusParser @@ -35,10 +36,9 @@ module Provers , PreparedTypedProverTask , prepareTypedProverTask , preparedTypedProverLogicalProblem - , preparedTypedProverTptpProblem , preparedTypedProverRequest , AcceptedVampireRun - , acceptedVampireRequest + , acceptedVampireRequestId , provedVampireRun , runPreparedTypedProver , runPreparedTypedProverWithObserver @@ -52,8 +52,18 @@ module Provers , workPositionModuleOrdinal , workPositionLocalRequestOrdinal , VampireExecutor + , VampireExecutorFault , VampireExecutorObservation(..) + , VampireRequestOwner + , VampireHandle + , VampireTerminal(..) + , renderVampireTerminalDiagnostic + , VampireCompletion(..) , withVampireExecutor + , withVampireRequestOwner + , submitVampireRequest + , awaitVampireRequest + , cancelVampireRequest , runPreparedTypedProverWithExecutor , vampireExecutorObservation ) where @@ -64,7 +74,8 @@ import Checking.Backend.Problem import Checking.Backend.Tptp import Control.Concurrent.STM - ( TBQueue + ( STM + , TBQueue , TMVar , TVar , atomically @@ -74,11 +85,13 @@ import Control.Concurrent.STM , newTBQueueIO , newTVarIO , orElse - , putTMVar + , readTMVar , readTBQueue , readTVar , readTVarIO - , takeTMVar + , throwSTM + , tryPutTMVar + , tryReadTMVar , writeTBQueue , writeTVar ) @@ -90,9 +103,10 @@ import Control.Exception , fromException ) import Control.Exception qualified as Exception -import Control.Monad (forever, replicateM, unless) +import Control.Monad (replicateM, unless, when) import Control.Monad.Logger import Data.ByteString qualified as ByteString +import Data.IntMap.Strict qualified as IntMap import Data.IORef ( IORef , atomicModifyIORef' @@ -103,6 +117,7 @@ import Data.IORef import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.Encoding qualified as TextEncoding +import Data.Text.Encoding.Error qualified as TextEncodingError import Data.Time import Numeric.Natural (Natural) import System.Exit (ExitCode(..)) @@ -269,6 +284,15 @@ data CanonicalAtpOutcome | Indeterminate deriving (Show, Eq, Ord) +-- | The closed non-accepting subset of canonical ATP outcomes. Protocol +-- disagreement is represented separately from a semantic non-proof, while an +-- accepting result is unrepresentable here. +data CanonicalAtpRejection + = RejectedCounterexample + | RejectedContradictoryInput + | RejectedIndeterminate + deriving (Show, Eq) + data VampireProtocolError = UnsuccessfulVampireExit ExitCode | UnsupportedVampireStatuses (Set Text) @@ -305,6 +329,37 @@ instance Show PartialCapturedStreams where ) ) +data BoundedBytes = BoundedBytes + { boundedBytesOriginalCount :: !Int + , boundedBytesRetained :: !ByteString.ByteString + , boundedBytesTruncated :: !Bool + } + deriving (Eq) + +instance Show BoundedBytes where + showsPrec precedence BoundedBytes{..} = + showParen (precedence > applicationPrecedence) + ( showString "BoundedBytes " + . shows + ( boundedBytesOriginalCount + , ByteString.length boundedBytesRetained + , boundedBytesTruncated + ) + ) + +data BoundedCapturedStreams = BoundedCapturedStreams + { boundedStdout :: !BoundedBytes + , boundedStderr :: !BoundedBytes + } + deriving (Show, Eq) + +data BoundedDiagnostic = BoundedDiagnostic + { boundedDiagnosticSummary :: !Text + , boundedDiagnosticStdout :: !BoundedBytes + , boundedDiagnosticStderr :: !BoundedBytes + } + deriving (Show, Eq) + -- | Classify parsed Vampire statuses without depending on stream or line order. classifyVampireProtocol :: VampireTaskMode @@ -381,10 +436,21 @@ data PreparedVerificationRequest = PreparedVerificationRequest { preparedVerificationDialect :: !VerificationDialect , preparedVerificationMode :: !VampireTaskMode , preparedVerificationInput :: !ByteString.ByteString - , preparedVerificationText :: !Text + , preparedVerificationIdentity :: !Authority.PreparedRequestId } deriving (Eq) +-- | Decode the one canonical serialized request only at a textual boundary. +-- Prepared requests deliberately do not retain an equivalent 'Text' copy. +preparedVerificationText :: PreparedVerificationRequest -> Text +preparedVerificationText request = + let encoded = preparedVerificationInput request + withoutFinalNewline = + case ByteString.unsnoc encoded of + Just (body, 10) -> body + _ -> encoded + in TextEncoding.decodeUtf8 withoutFinalNewline + preparedVerificationByteCount :: PreparedVerificationRequest -> Int @@ -400,21 +466,14 @@ preparedVerificationBytes = preparedVerificationRequestId :: PreparedVerificationRequest -> Authority.PreparedRequestId -preparedVerificationRequestId request = - Authority.preparedRequestId - (case preparedVerificationDialect request of - VerificationFof -> Authority.PreparedRequestFof - VerificationTh0 -> Authority.PreparedRequestTh0) - (case preparedVerificationMode request of - DirectTask -> Authority.PreparedRequestDirect - IndirectTask -> Authority.PreparedRequestIndirect) - (preparedVerificationBytes request) +preparedVerificationRequestId = + preparedVerificationIdentity data PreparedTypedProverTask ref local origin global = PreparedTypedProverTask !(TypedProblem ref local origin global) - !(PreparedTypedTptpProblem ref local global) !PreparedVerificationRequest + !Text prepareTypedProverTask :: (Ord local, Ord global) @@ -426,27 +485,34 @@ prepareTypedProverTask prepareTypedProverTask mode problem = do prepared <- prepareTypedTptpProblem problem - let preparedRequest = + let dialect = + case preparedTypedTptpRoute prepared of + RouteFof -> VerificationFof + RouteTh0 -> VerificationTh0 + bytes = + TextEncoding.encodeUtf8 + (preparedTypedTptpTextNewline prepared) + identity = + Authority.preparedRequestId + (case dialect of + VerificationFof -> Authority.PreparedRequestFof + VerificationTh0 -> Authority.PreparedRequestTh0) + (case mode of + DirectTask -> Authority.PreparedRequestDirect + IndirectTask -> Authority.PreparedRequestIndirect) + bytes + preparedRequest = PreparedVerificationRequest - { preparedVerificationDialect = - case preparedTypedTptpRoute prepared of - RouteFof -> - VerificationFof - RouteTh0 -> - VerificationTh0 + { preparedVerificationDialect = dialect , preparedVerificationMode = mode - , preparedVerificationInput = - TextEncoding.encodeUtf8 - (preparedTypedTptpTextNewline - prepared) - , preparedVerificationText = - preparedTypedTptpText prepared + , preparedVerificationInput = bytes + , preparedVerificationIdentity = identity } pure (PreparedTypedProverTask problem - prepared - preparedRequest) + preparedRequest + (preparedTypedTptpConjectureText prepared)) preparedTypedProverLogicalProblem :: PreparedTypedProverTask ref local origin global @@ -454,35 +520,22 @@ preparedTypedProverLogicalProblem preparedTypedProverLogicalProblem (PreparedTypedProverTask problem - _prepared - _request) = + _request + _conjecture) = problem -preparedTypedProverTptpProblem - :: PreparedTypedProverTask ref local origin global - -> PreparedTypedTptpProblem ref local global -preparedTypedProverTptpProblem - (PreparedTypedProverTask - _problem - prepared - _request) = - prepared - preparedTypedProverRequest :: PreparedTypedProverTask ref local origin global -> PreparedVerificationRequest preparedTypedProverRequest (PreparedTypedProverTask _problem - _prepared - request) = + request + _conjecture) = request data AcceptedVampireRun = AcceptedVampireRun - { acceptedVampireRequest :: !PreparedVerificationRequest - , acceptedVampireCommand :: !Vampire - , acceptedVampireTranscript :: !CompletedTranscript - } + { acceptedVampireRequestId :: !Authority.PreparedRequestId } deriving (Eq) data ProverAnswer @@ -554,15 +607,15 @@ data ProverProcessError | ProverTimedOut !FilePath !TimeLimit - !PartialCapturedStreams + !BoundedCapturedStreams | ProverOutputLimitExceeded !FilePath !ProverOutputStream - !PartialCapturedStreams + !BoundedCapturedStreams | ProverTerminatedBySignal !FilePath !Int - !PartialCapturedStreams + !BoundedCapturedStreams | ProverLifecycleFailed !FilePath !Text deriving (Show, Eq) @@ -613,37 +666,33 @@ runPreparedTypedProverWithObserver vampireCommand (PreparedTypedProverTask _problem - prepared - preparedRequest) = do + preparedRequest + conjecture) = do startTime <- liftIO getCurrentTime - transcriptResult <- - liftIO - (runPreparedVampireProcessWithObserver - observer - vampireCommand - preparedRequest) - let answer = - classifyPreparedVampireAnswer - "typed obligation" - vampireCommand - preparedRequest - <$> transcriptResult + terminal <- liftIO + (runPreparedVerificationTerminal + observer + vampireCommand + preparedRequest) + answer <- liftIO + (completionProverResult + preparedRequest + (VampireCompletion terminal)) endTime <- liftIO getCurrentTime let duration = timeDifferenceToText startTime endTime dialect = - case preparedTypedTptpRoute prepared of - RouteFof -> + case preparedVerificationDialect preparedRequest of + VerificationFof -> "FOF" - RouteTh0 -> + VerificationTh0 -> "TH0" logInfoN (duration <> " " - <> preparedTypedTptpConjectureText - prepared + <> conjecture <> " [typed " <> dialect <> "]") @@ -654,7 +703,8 @@ runPreparedTypedProverWithObserver -- checker builders and typed tasks never cross this boundary. data VampireExecutor = VampireExecutor { executorQueue :: !(TBQueue ExecutorJob) - , executorClosed :: !(TVar Bool) + , executorState :: !(TVar VampireExecutorState) + , executorNextHandle :: !(TVar Int) , executorCommand :: !Vampire , executorRequestObserver :: !(WorkPosition -> PreparedVerificationRequest -> IO ()) @@ -665,20 +715,75 @@ data ExecutorJob = ExecutorJob { executorJobPosition :: !WorkPosition , executorJobRequest :: !PreparedVerificationRequest , executorJobCancelled :: !(TVar Bool) + , executorJobStarted :: !(TVar Bool) , executorJobCompletion - :: !(TMVar - (Either - SomeException - (Either ProverProcessError ProverAnswer))) + :: !(TMVar VampireCompletion) } +data VampireExecutorState + = ExecutorRunning + | ExecutorClosing + | ExecutorFaulted !VampireExecutorFault + +-- | A global executor fault is distinct from one request's declared process +-- or protocol outcome. Its bounded message carries no process transcript. +newtype VampireExecutorFault = VampireExecutorFault Text + deriving (Show) + +instance Exception.Exception VampireExecutorFault + +data VampireRequestOwner = VampireRequestOwner + { requestOwnerExecutor :: !VampireExecutor + , requestOwnerState :: !(TVar VampireRequestOwnerState) + } + +data VampireRequestOwnerState + = RequestOwnerOpen !(IntMap VampireHandle) + | RequestOwnerClosed + +-- | An opaque, owner-scoped completion handle. It deliberately retains no +-- prepared request, command, transcript, builder, or parser state. +data VampireHandle = VampireHandle + { vampireHandleOrdinal :: !Int + , vampireHandleOwner :: !VampireRequestOwner + , vampireHandleCancelled :: !(TVar Bool) + , vampireHandleStarted :: !(TVar Bool) + , vampireHandleCompletion :: !(TMVar VampireCompletion) + } + +data VampireTerminal + = VampireAccepted !Authority.PreparedRequestId + | VampireRejected !CanonicalAtpRejection !BoundedDiagnostic + | VampireProtocolFailed !BoundedDiagnostic + | VampireProcessFailed !ProverProcessError + | VampireCancelled + deriving (Show, Eq) + +newtype VampireCompletion = VampireCompletion + { vampireCompletionTerminal :: VampireTerminal } + deriving (Show, Eq) + +renderVampireTerminalDiagnostic :: VampireTerminal -> Maybe Text +renderVampireTerminalDiagnostic = \case + VampireAccepted{} -> Nothing + VampireRejected _rejection diagnostic -> + Just (renderBoundedDiagnostic diagnostic) + VampireProtocolFailed diagnostic -> + Just (renderBoundedDiagnostic diagnostic) + VampireProcessFailed processFailure -> + Just (Text.pack (show processFailure)) + VampireCancelled -> Nothing + data VampireExecutorRuntime = VampireExecutorRuntime { runtimeSubmittedCount :: !Int , runtimeRunCount :: !Int , runtimeLiveCount :: !Int , runtimeMaximumLiveCount :: !Int , runtimeFirstStartNanoseconds :: !(Maybe Word64) + , runtimeFinalSubmissionNanoseconds :: !(Maybe Word64) + , runtimeFinalCompletionNanoseconds :: !(Maybe Word64) , runtimeExecutionNanoseconds :: !Word64 + , runtimeLongestExecutionNanoseconds :: !Word64 } data VampireExecutorObservation = VampireExecutorObservation @@ -686,7 +791,10 @@ data VampireExecutorObservation = VampireExecutorObservation , vampireExecutorRunCount :: !Int , vampireExecutorMaximumLiveCount :: !Int , vampireExecutorFirstStartNanoseconds :: !(Maybe Word64) + , vampireExecutorFinalSubmissionNanoseconds :: !(Maybe Word64) + , vampireExecutorFinalCompletionNanoseconds :: !(Maybe Word64) , vampireExecutorExecutionNanoseconds :: !Word64 + , vampireExecutorLongestExecutionNanoseconds :: !Word64 } deriving (Show, Eq) @@ -695,6 +803,11 @@ data VampireExecutorClosed = VampireExecutorClosed instance Exception.Exception VampireExecutorClosed +data VampireRequestOwnerClosed = VampireRequestOwnerClosed + deriving (Show) + +instance Exception.Exception VampireRequestOwnerClosed + data RequestObserverFailure = RequestObserverFailure SomeException instance Show RequestObserverFailure where @@ -711,7 +824,10 @@ initialVampireExecutorRuntime = , runtimeLiveCount = 0 , runtimeMaximumLiveCount = 0 , runtimeFirstStartNanoseconds = Nothing + , runtimeFinalSubmissionNanoseconds = Nothing + , runtimeFinalCompletionNanoseconds = Nothing , runtimeExecutionNanoseconds = 0 + , runtimeLongestExecutionNanoseconds = 0 } -- | Bracket exactly the selected number of workers. Cancelling the bracket @@ -731,48 +847,91 @@ withVampireExecutor selected command observer action = acquire = do queue <- newTBQueueIO (fromIntegral workerCount * 2) - closed <- newTVarIO False + state <- newTVarIO ExecutorRunning + nextHandle <- newTVarIO 0 runtime <- newTVarIO initialVampireExecutorRuntime let executor = VampireExecutor { executorQueue = queue - , executorClosed = closed + , executorState = state + , executorNextHandle = nextHandle , executorCommand = command , executorRequestObserver = observer , executorRuntime = runtime } - workers <- replicateM workerCount (async (executorWorker executor)) + workers <- replicateM workerCount + (async (superviseExecutorWorker executor)) pure (executor, workers) release (executor, workers) = do - atomically (writeTVar (executorClosed executor) True) + atomically do + state <- readTVar (executorState executor) + case state of + ExecutorRunning -> + writeTVar (executorState executor) ExecutorClosing + ExecutorClosing -> + pure () + ExecutorFaulted{} -> + pure () traverse_ cancel workers traverse_ waitCatch workers +-- | Bracket the complete set of handles submitted by one module pipeline. +-- Normal early return, failure, and asynchronous cancellation all cancel and +-- reap the remaining owned work before the scope is left. +withVampireRequestOwner + :: VampireExecutor + -> (VampireRequestOwner -> IO value) + -> IO value +withVampireRequestOwner executor = + Exception.bracket acquire release + where + acquire = + VampireRequestOwner executor + <$> newTVarIO (RequestOwnerOpen IntMap.empty) + + release owner = Exception.mask_ do + handles <- atomically do + state <- readTVar (requestOwnerState owner) + case state of + RequestOwnerClosed -> + pure [] + RequestOwnerOpen owned -> do + writeTVar (requestOwnerState owner) RequestOwnerClosed + pure (IntMap.elems owned) + traverse_ signalVampireCancellation handles + traverse_ awaitVampireCancellation handles + traverse_ deregisterVampireHandle handles + runPreparedTypedProverWithExecutor :: (MonadIO io, MonadLogger io) - => VampireExecutor + => VampireRequestOwner -> WorkPosition -> PreparedTypedProverTask ref local origin global -> io (Either ProverProcessError ProverAnswer) runPreparedTypedProverWithExecutor - executor + owner position (PreparedTypedProverTask _problem - prepared - preparedRequest) = do + preparedRequest + conjecture) = do startTime <- liftIO getCurrentTime - answer <- liftIO (submitVampireRequest executor position preparedRequest) + answer <- liftIO do + handle <- submitVampireRequest owner position preparedRequest + completion <- + awaitVampireRequest handle + `Exception.onException` cancelVampireRequest handle + completionProverResult preparedRequest completion endTime <- liftIO getCurrentTime let dialect = - case preparedTypedTptpRoute prepared of - RouteFof -> "FOF" - RouteTh0 -> "TH0" + case preparedVerificationDialect preparedRequest of + VerificationFof -> "FOF" + VerificationTh0 -> "TH0" logInfoN (timeDifferenceToText startTime endTime <> " " - <> preparedTypedTptpConjectureText prepared + <> conjecture <> " [typed " <> dialect <> "]") @@ -791,96 +950,254 @@ vampireExecutorObservation executor = do runtimeMaximumLiveCount runtime , vampireExecutorFirstStartNanoseconds = runtimeFirstStartNanoseconds runtime + , vampireExecutorFinalSubmissionNanoseconds = + runtimeFinalSubmissionNanoseconds runtime + , vampireExecutorFinalCompletionNanoseconds = + runtimeFinalCompletionNanoseconds runtime , vampireExecutorExecutionNanoseconds = runtimeExecutionNanoseconds runtime + , vampireExecutorLongestExecutionNanoseconds = + runtimeLongestExecutionNanoseconds runtime } submitVampireRequest - :: VampireExecutor + :: VampireRequestOwner -> WorkPosition -> PreparedVerificationRequest - -> IO (Either ProverProcessError ProverAnswer) -submitVampireRequest executor position request = - Exception.mask \restore -> do - -- Force the compact queue payload before handing it to a worker. - _ <- Exception.evaluate (preparedVerificationByteCount request) - _ <- Exception.evaluate - (Text.length (preparedVerificationText request)) + -> IO VampireHandle +submitVampireRequest owner position request = do + -- Force the compact queue payload before masked ownership acquisition. + _ <- Exception.evaluate (preparedVerificationByteCount request) + _ <- Exception.evaluate (preparedVerificationRequestId request) + Exception.mask_ do cancelled <- newTVarIO False + started <- newTVarIO False completion <- newEmptyTMVarIO - let job = - ExecutorJob - { executorJobPosition = position - , executorJobRequest = request - , executorJobCancelled = cancelled - , executorJobCompletion = completion - } - cancelJob = atomically (writeTVar cancelled True) - enqueue = atomically do - closed <- readTVar (executorClosed executor) - if closed - then pure False - else do - writeTBQueue (executorQueue executor) job - modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeSubmittedCount = - runtimeSubmittedCount runtime + 1 - }) - pure True - accepted <- restore enqueue `Exception.onException` cancelJob - unless accepted (Exception.throwIO VampireExecutorClosed) - outcome <- - restore (atomically (takeTMVar completion)) - `Exception.onException` cancelJob - either Exception.throwIO pure outcome + let executor = requestOwnerExecutor owner + handle <- atomically do + executorStatus <- readTVar (executorState executor) + case executorStatus of + ExecutorClosing -> throwSTM VampireExecutorClosed + ExecutorFaulted fault -> throwSTM fault + ExecutorRunning -> pure () + ownerStatus <- readTVar (requestOwnerState owner) + owned <- case ownerStatus of + RequestOwnerClosed -> throwSTM VampireRequestOwnerClosed + RequestOwnerOpen current -> pure current + ordinal <- readTVar (executorNextHandle executor) + writeTVar (executorNextHandle executor) (ordinal + 1) + let acquired = + VampireHandle + { vampireHandleOrdinal = ordinal + , vampireHandleOwner = owner + , vampireHandleCancelled = cancelled + , vampireHandleStarted = started + , vampireHandleCompletion = completion + } + job = + ExecutorJob + { executorJobPosition = position + , executorJobRequest = request + , executorJobCancelled = cancelled + , executorJobStarted = started + , executorJobCompletion = completion + } + writeTBQueue (executorQueue executor) job + writeTVar + (requestOwnerState owner) + (RequestOwnerOpen (IntMap.insert ordinal acquired owned)) + modifyTVar' + (executorRuntime executor) + (\runtime -> + runtime + { runtimeSubmittedCount = + runtimeSubmittedCount runtime + 1 + }) + pure acquired + submitted <- getMonotonicTimeNSec + atomically + (modifyTVar' + (executorRuntime executor) + (\runtime -> + runtime + { runtimeFinalSubmissionNanoseconds = + Just + (maybe submitted + (max submitted) + (runtimeFinalSubmissionNanoseconds + runtime)) + })) + pure handle + +awaitVampireRequest :: VampireHandle -> IO VampireCompletion +awaitVampireRequest handle = Exception.mask \restore -> do + let executor = requestOwnerExecutor (vampireHandleOwner handle) + completion <- restore (atomically do + executorStatus <- readTVar (executorState executor) + case executorStatus of + ExecutorFaulted fault -> throwSTM fault + ExecutorRunning -> readTMVar (vampireHandleCompletion handle) + ExecutorClosing -> + (readTMVar (vampireHandleCompletion handle)) + `orElse` throwSTM VampireExecutorClosed) + deregisterVampireHandle handle + pure completion + +cancelVampireRequest :: VampireHandle -> IO () +cancelVampireRequest handle = Exception.mask_ do + signalVampireCancellation handle + awaitVampireCancellation handle + deregisterVampireHandle handle + +signalVampireCancellation :: VampireHandle -> IO () +signalVampireCancellation handle = do + let executor = requestOwnerExecutor (vampireHandleOwner handle) + completion = VampireCompletion VampireCancelled + _ <- Exception.evaluate completion + published <- getMonotonicTimeNSec + atomically do + writeTVar (vampireHandleCancelled handle) True + started <- readTVar (vampireHandleStarted handle) + unless started + (void + (publishVampireTerminalSTM + executor + (vampireHandleCompletion handle) + published + completion)) + +awaitVampireCancellation :: VampireHandle -> IO () +awaitVampireCancellation handle = + -- A running worker acknowledges ordinary cancellation only after + -- terminating and reaping its owned process group. After a global fault, + -- the worker lifecycle flag is the acknowledgement because the terminal + -- cell deliberately remains subordinate to that fault. + atomically do + executorStatus <- readTVar + (executorState (requestOwnerExecutor (vampireHandleOwner handle))) + case executorStatus of + ExecutorFaulted{} -> do + stillRunning <- readTVar (vampireHandleStarted handle) + check (not stillRunning) + _ -> void (readTMVar (vampireHandleCompletion handle)) + +deregisterVampireHandle :: VampireHandle -> IO () +deregisterVampireHandle handle = atomically do + let owner = vampireHandleOwner handle + state <- readTVar (requestOwnerState owner) + case state of + RequestOwnerClosed -> pure () + RequestOwnerOpen owned -> + writeTVar + (requestOwnerState owner) + (RequestOwnerOpen + (IntMap.delete (vampireHandleOrdinal handle) owned)) + +superviseExecutorWorker :: VampireExecutor -> IO () +superviseExecutorWorker executor = do + result <- Exception.try (executorWorker executor) + case result of + Right () -> pure () + Left workerFailure -> do + state <- readTVarIO (executorState executor) + case state of + ExecutorRunning -> + recordExecutorFault executor workerFailure + ExecutorClosing -> + pure () + ExecutorFaulted{} -> + pure () + +recordExecutorFault :: VampireExecutor -> SomeException -> IO () +recordExecutorFault executor workerFailure = atomically do + state <- readTVar (executorState executor) + case state of + ExecutorRunning -> + writeTVar + (executorState executor) + (ExecutorFaulted + (VampireExecutorFault + (boundedText + (Text.pack (displayException workerFailure))))) + ExecutorClosing -> pure () + ExecutorFaulted{} -> pure () executorWorker :: VampireExecutor -> IO () -executorWorker executor = - forever do - job <- atomically (readTBQueue (executorQueue executor)) - cancelled <- readTVarIO (executorJobCancelled job) - unless cancelled (executeJob executor job) +executorWorker executor = do + next <- atomically do + state <- readTVar (executorState executor) + case state of + ExecutorRunning -> Just <$> readTBQueue (executorQueue executor) + ExecutorClosing -> pure Nothing + ExecutorFaulted{} -> pure Nothing + case next of + Nothing -> pure () + Just job -> do + shouldRun <- atomically do + completed <- tryReadTMVar (executorJobCompletion job) + case completed of + Just _ -> pure False + Nothing -> do + writeTVar (executorJobStarted job) True + pure True + when shouldRun + (executeJob executor job + `Exception.finally` + atomically (writeTVar (executorJobStarted job) False)) + executorWorker executor data JobWait value = JobFinished !(Either SomeException value) | JobCancelled + | JobExecutorStopped executeJob :: VampireExecutor -> ExecutorJob -> IO () executeJob executor job = Exception.mask \restore -> do running <- async (restore - (observeExecutorRun executor - (runPreparedVerificationRequest - (executorRequestObserver executor - (executorJobPosition job)) - (executorCommand executor) - (executorJobRequest job)))) + (timedExecutorRun executor job)) waited <- restore (atomically - ( (JobFinished <$> waitCatchSTM running) - `orElse` - (do - cancelled <- readTVar - (executorJobCancelled job) - check cancelled - pure JobCancelled) - )) + (do + state <- readTVar (executorState executor) + case state of + ExecutorRunning -> + (JobFinished <$> waitCatchSTM running) + `orElse` + (do + cancelled <- readTVar + (executorJobCancelled job) + check cancelled + pure JobCancelled) + ExecutorClosing -> pure JobExecutorStopped + ExecutorFaulted{} -> pure JobExecutorStopped)) `Exception.onException` (cancel running >> void (waitCatch running)) case waited of - JobFinished result -> - atomically - (putTMVar (executorJobCompletion job) result) + JobFinished result -> case result of + Left workerFailure -> Exception.throwIO workerFailure + Right terminal -> + publishVampireTerminal + executor + (executorJobCompletion job) + terminal JobCancelled -> do cancel running void (waitCatch running) + publishVampireTerminal + executor + (executorJobCompletion job) + VampireCancelled + JobExecutorStopped -> do + cancel running + void (waitCatch running) -observeExecutorRun :: VampireExecutor -> IO value -> IO value -observeExecutorRun executor action = do +timedExecutorRun + :: VampireExecutor + -> ExecutorJob + -> IO VampireTerminal +timedExecutorRun executor job = Exception.mask \restore -> do started <- getMonotonicTimeNSec atomically (modifyTVar' @@ -895,33 +1212,147 @@ observeExecutorRun executor action = do , runtimeFirstStartNanoseconds = runtimeFirstStartNanoseconds runtime <|> Just started })) - action `Exception.finally` do - finished <- getMonotonicTimeNSec - atomically - (modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeLiveCount = runtimeLiveCount runtime - 1 - , runtimeExecutionNanoseconds = - runtimeExecutionNanoseconds runtime - + (finished - started) - })) + terminal <- restore + (runPreparedVerificationTerminal + (executorRequestObserver executor (executorJobPosition job)) + (executorCommand executor) + (executorJobRequest job)) + `Exception.onException` finishExecutorRun executor started + finishExecutorRun executor started + pure terminal + +finishExecutorRun :: VampireExecutor -> Word64 -> IO () +finishExecutorRun executor started = do + finished <- getMonotonicTimeNSec + let elapsed = finished - started + atomically + (modifyTVar' + (executorRuntime executor) + (\runtime -> + runtime + { runtimeLiveCount = runtimeLiveCount runtime - 1 + , runtimeExecutionNanoseconds = + runtimeExecutionNanoseconds runtime + elapsed + , runtimeLongestExecutionNanoseconds = + max elapsed (runtimeLongestExecutionNanoseconds runtime) + })) + +publishVampireTerminal + :: VampireExecutor + -> TMVar VampireCompletion + -> VampireTerminal + -> IO () +publishVampireTerminal executor completionCell terminal = do + let completion = VampireCompletion terminal + _ <- Exception.evaluate completion + published <- getMonotonicTimeNSec + void + (atomically + (publishVampireTerminalSTM + executor completionCell published completion)) + +publishVampireTerminalSTM + :: VampireExecutor + -> TMVar VampireCompletion + -> Word64 + -> VampireCompletion + -> STM Bool +publishVampireTerminalSTM executor completionCell published completion = do + inserted <- tryPutTMVar completionCell completion + when inserted + (modifyTVar' + (executorRuntime executor) + (\runtime -> + runtime + { runtimeFinalCompletionNanoseconds = + Just + (maybe published + (max published) + (runtimeFinalCompletionNanoseconds runtime)) + })) + pure inserted -runPreparedVerificationRequest +runPreparedVerificationTerminal :: (PreparedVerificationRequest -> IO ()) -> Vampire -> PreparedVerificationRequest - -> IO (Either ProverProcessError ProverAnswer) -runPreparedVerificationRequest observer command request = do + -> IO VampireTerminal +runPreparedVerificationTerminal observer command request = do transcriptResult <- runPreparedVampireProcessWithObserver observer command request - pure - (classifyPreparedVampireAnswer - "typed obligation" - command - request - <$> transcriptResult) + pure case transcriptResult of + Left processFailure -> + VampireProcessFailed processFailure + Right transcript -> + case classifyVampireCompleted + (preparedVerificationMode request) + transcript of + Left protocolFailure -> + VampireProtocolFailed + (boundedTranscriptDiagnostic + (Text.pack (show protocolFailure)) + transcript) + Right Proved -> + VampireAccepted (preparedVerificationRequestId request) + Right Counterexample -> + VampireRejected + RejectedCounterexample + (boundedTranscriptDiagnostic + "Vampire found a countermodel" + transcript) + Right ContradictoryInput -> + VampireRejected + RejectedContradictoryInput + (boundedTranscriptDiagnostic + "Vampire reported contradictory input" + transcript) + Right Indeterminate -> + VampireRejected + RejectedIndeterminate + (boundedTranscriptDiagnostic + "Vampire did not establish the obligation" + transcript) + +completionProverResult + :: PreparedVerificationRequest + -> VampireCompletion + -> IO (Either ProverProcessError ProverAnswer) +completionProverResult request completion = + case vampireCompletionTerminal completion of + VampireAccepted acceptedId + | acceptedId == preparedVerificationRequestId request -> + pure + (Right + (ProvedAnswer + (AcceptedVampireRun acceptedId))) + | otherwise -> + Exception.throwIO + (VampireExecutorFault + "accepted Vampire result has the wrong request id") + VampireRejected rejection _diagnostic -> + pure + (Right + (case rejection of + RejectedCounterexample -> + CounterSatisfiable task + RejectedContradictoryInput -> + ContradictoryAxioms task + RejectedIndeterminate -> + Uncertain task)) + VampireProtocolFailed diagnostic -> + pure + (Right + (Error + "typed obligation" + (renderBoundedDiagnostic diagnostic))) + VampireProcessFailed processFailure -> + pure (Left processFailure) + VampireCancelled -> + Exception.throwIO + (VampireExecutorFault + "active admission encountered a cancelled Vampire request") + where + task = preparedVerificationText request runPreparedVampireProcessWithObserver :: (PreparedVerificationRequest -> IO ()) @@ -997,11 +1428,13 @@ runPreparedVampireProcessWithObserver then ProverLifecycleFailed executable - (exceptionText ioFailure) + (boundedText + (exceptionText ioFailure)) else ProverLaunchFailed executable - (exceptionText ioFailure))) + (boundedText + (exceptionText ioFailure)))) | otherwise -> Exception.throwIO err @@ -1069,7 +1502,7 @@ superviseVampireProcess (ProverTimedOut executable timeLimit - partial)) + (boundedCapturedStreams partial))) Just (Left abort) -> do terminateOwnedProcess partial <- @@ -1096,7 +1529,7 @@ superviseVampireProcess (ProverTerminatedBySignal executable (negate signalCode) - partial)) + (boundedCapturedStreams partial))) _ -> pure do stdout <- decodeOutput @@ -1241,6 +1674,86 @@ capturedBytes capture = . captureChunksReversed <$> readIORef capture +boundedTranscriptBytes :: Int +boundedTranscriptBytes = 32 * 1024 + +boundedTranscriptHalf :: Int +boundedTranscriptHalf = boundedTranscriptBytes `div` 2 + +boundedBytes :: ByteString.ByteString -> BoundedBytes +boundedBytes bytes = + let original = ByteString.length bytes + in if original <= boundedTranscriptBytes + then + BoundedBytes + { boundedBytesOriginalCount = original + , boundedBytesRetained = bytes + , boundedBytesTruncated = False + } + else + BoundedBytes + { boundedBytesOriginalCount = original + , boundedBytesRetained = + ByteString.take boundedTranscriptHalf bytes + <> ByteString.drop + (original - boundedTranscriptHalf) + bytes + , boundedBytesTruncated = True + } + +boundedText :: Text -> Text +boundedText = + decodeBoundedBytes . boundedBytes . TextEncoding.encodeUtf8 + +decodeBoundedBytes :: BoundedBytes -> Text +decodeBoundedBytes = + TextEncoding.decodeUtf8With TextEncodingError.lenientDecode + . boundedBytesRetained + +boundedCapturedStreams + :: PartialCapturedStreams + -> BoundedCapturedStreams +boundedCapturedStreams PartialCapturedStreams{..} = + BoundedCapturedStreams + { boundedStdout = boundedBytes partialStdout + , boundedStderr = boundedBytes partialStderr + } + +boundedTranscriptDiagnostic + :: Text + -> CompletedTranscript + -> BoundedDiagnostic +boundedTranscriptDiagnostic summary CompletedTranscript{completedStreams = streams} = + BoundedDiagnostic + { boundedDiagnosticSummary = boundedText summary + , boundedDiagnosticStdout = + boundedBytes + (TextEncoding.encodeUtf8 (completedStdout streams)) + , boundedDiagnosticStderr = + boundedBytes + (TextEncoding.encodeUtf8 (completedStderr streams)) + } + +renderBoundedDiagnostic :: BoundedDiagnostic -> Text +renderBoundedDiagnostic BoundedDiagnostic{..} = + Text.unlines + [ boundedDiagnosticSummary + , renderBoundedStream "stdout" boundedDiagnosticStdout + , renderBoundedStream "stderr" boundedDiagnosticStderr + ] + +renderBoundedStream :: Text -> BoundedBytes -> Text +renderBoundedStream streamLabel bytes = + streamLabel + <> (if boundedBytesTruncated bytes + then + " (retained first and last 16 KiB of " + <> Text.pack (show (boundedBytesOriginalCount bytes)) + <> " bytes)" + else "") + <> ":\n" + <> decodeBoundedBytes bytes + supervisorAbortError :: FilePath -> PartialCapturedStreams @@ -1248,11 +1761,14 @@ supervisorAbortError -> ProverProcessError supervisorAbortError executable partial = \case SupervisorCommunicationFailed stream message -> - ProverCommunicationFailed executable stream message + ProverCommunicationFailed executable stream (boundedText message) SupervisorOutputLimitExceeded stream -> - ProverOutputLimitExceeded executable stream partial + ProverOutputLimitExceeded + executable + stream + (boundedCapturedStreams partial) SupervisorLifecycleFailed message -> - ProverLifecycleFailed executable message + ProverLifecycleFailed executable (boundedText message) wallTimeoutMicroseconds :: TimeLimit -> Int wallTimeoutMicroseconds (Seconds seconds) = @@ -1296,7 +1812,7 @@ decodeOutput executable stream bytes = (ProverOutputMalformedUtf8 executable stream - (Text.pack (show err))) + (boundedText (Text.pack (show err)))) Right output -> Right output @@ -1304,31 +1820,6 @@ exceptionText :: IOException -> Text exceptionText = Text.pack . displayException -classifyPreparedVampireAnswer - :: Text - -> Vampire - -> PreparedVerificationRequest - -> CompletedTranscript - -> ProverAnswer -classifyPreparedVampireAnswer - errorLabel - vampireCommand - preparedRequest - transcript@CompletedTranscript{..} = - case classifyVampireCompleted - (preparedVerificationMode preparedRequest) - transcript of - Left protocolError -> - Error - errorLabel - (renderProtocolError protocolError completedStreams) - Right outcome -> - canonicalOutcomeAnswer - preparedRequest - vampireCommand - transcript - outcome - classifyVampireCompleted :: VampireTaskMode -> CompletedTranscript @@ -1364,46 +1855,6 @@ statusesFromCompleteStreams CompleteCapturedStreams{..} | otherwise -> mempty -canonicalOutcomeAnswer - :: PreparedVerificationRequest - -> Vampire - -> CompletedTranscript - -> CanonicalAtpOutcome - -> ProverAnswer -canonicalOutcomeAnswer - preparedRequest - vampireCommand - transcript = \case - Proved -> - ProvedAnswer - AcceptedVampireRun - { acceptedVampireRequest = preparedRequest - , acceptedVampireCommand = vampireCommand - , acceptedVampireTranscript = transcript - } - Counterexample -> - CounterSatisfiable - (preparedVerificationText preparedRequest) - ContradictoryInput -> - ContradictoryAxioms - (preparedVerificationText preparedRequest) - Indeterminate -> - Uncertain - (preparedVerificationText preparedRequest) - -renderProtocolError - :: VampireProtocolError - -> CompleteCapturedStreams - -> Text -renderProtocolError protocolError CompleteCapturedStreams{..} = - Text.unlines - [ "Vampire protocol error: " <> Text.pack (show protocolError) - , "stdout:" - , completedStdout - , "stderr:" - , completedStderr - ] - vampireStatusFromText :: Text -> VampireStatus vampireStatusFromText = \case "Theorem" -> StatusTheorem diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs index 22a6b5b..f0f0e8f 100644 --- a/source/Test/Unit/Provers.hs +++ b/source/Test/Unit/Provers.hs @@ -7,9 +7,15 @@ import Checking.Backend.Problem import Checking.Core import Provers -import Control.Concurrent (threadDelay) +import Control.Concurrent + ( newEmptyMVar + , putMVar + , takeMVar + , threadDelay + ) import Control.Exception (bracket) import Control.Exception qualified as Exception +import Control.Monad (when) import Control.Monad.Logger (runNoLoggingT) import Data.IORef ( newIORef @@ -35,6 +41,7 @@ import Test.Tasty.HUnit import Text.Read (readMaybe) import Text.Megaparsec (parseMaybe) import UnliftIO.Async (cancel, mapConcurrently, withAsync) +import UnliftIO.Async qualified as Async unitTests :: TestTree unitTests = @@ -79,7 +86,38 @@ jobsSelectionTests = vampireExecutorTests :: TestTree vampireExecutorTests = testGroup "bounded Vampire executor" - [ testCase "bounds live one-core processes" do + [ testCase "opaque handles complete out of submission order" do + prepared <- preparedTypedTask 0 + firstStarted <- newEmptyMVar + releaseFirst <- newEmptyMVar + withFakeVampire + [ "cat >/dev/null" + , "printf '%s\n' '% SZS status Theorem for fake'" + ] + \vampireCommand -> + withVampireExecutor + (positiveJobs 2) + vampireCommand + (\position _request -> + when + (workPositionLocalRequestOrdinal position == 1) + (putMVar firstStarted () >> takeMVar releaseFirst)) + \executor -> withVampireRequestOwner executor \owner -> do + first <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + takeMVar firstStarted + second <- submitVampireRequest + owner + (workPosition 1 2) + (preparedTypedProverRequest prepared) + secondCompletion <- awaitVampireRequest second + assertAcceptedRequest prepared secondCompletion + putMVar releaseFirst () + firstCompletion <- awaitVampireRequest first + assertAcceptedRequest prepared firstCompletion + , testCase "bounds live one-core processes" do prepared <- preparedTypedTask 0 withFakeVampire [ "previous=''" @@ -101,12 +139,12 @@ vampireExecutorTests = (positiveJobs 2) vampireCommand (\_position _request -> pure ()) - \executor -> do + \executor -> withVampireRequestOwner executor \owner -> do answers <- mapConcurrently (\ordinal -> runNoLoggingT (runPreparedTypedProverWithExecutor - executor + owner (workPosition 1 ordinal) prepared)) [1..4] @@ -128,17 +166,17 @@ vampireExecutorTests = (\_position _request -> Exception.throwIO (userError "observer failed")) - \executor -> do + \executor -> withVampireRequestOwner executor \owner -> do result <- Exception.try (runNoLoggingT (runPreparedTypedProverWithExecutor - executor + owner (workPosition 1 1) prepared)) case result of - Left (failure :: Exception.IOException) -> + Left (failure :: VampireExecutorFault) -> assertBool - "observer exception" + "global executor fault" ("observer failed" `Text.isInfixOf` Text.pack (show failure)) @@ -156,11 +194,11 @@ vampireExecutorTests = (positiveJobs 1) vampireCommand (\_position _request -> pure ()) - \executor -> + \executor -> withVampireRequestOwner executor \owner -> withAsync (runNoLoggingT (runPreparedTypedProverWithExecutor - executor + owner (workPosition 1 1) prepared)) \running -> do @@ -168,7 +206,7 @@ vampireExecutorTests = withAsync (runNoLoggingT (runPreparedTypedProverWithExecutor - executor + owner (workPosition 2 1) prepared)) \queued -> do @@ -182,6 +220,239 @@ vampireExecutorTests = vampireExecutorRunCount observed `shouldBe` 1 assertProcessesGone processIds + , testCase "explicit cancellation completes queued and running handles" do + prepared <- preparedTypedTask 0 + withProcessGroupFake + defaultTimeLimit + [] + \pidFile vampireCommand -> + withVampireExecutor + (positiveJobs 1) + vampireCommand + (\_position _request -> pure ()) + \executor -> withVampireRequestOwner executor \owner -> do + running <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + processIds <- waitForProcessIds pidFile + queued <- submitVampireRequest + owner + (workPosition 1 2) + (preparedTypedProverRequest prepared) + cancelVampireRequest queued + awaitVampireRequest queued >>= assertCancelled + afterQueued <- vampireExecutorObservation executor + assertBool + "queued terminal updates final completion" + (isJust + (vampireExecutorFinalCompletionNanoseconds + afterQueued)) + cancelVampireRequest running + awaitVampireRequest running >>= assertCancelled + assertProcessesGone processIds + , testCase "structured shutdown wakes waiter and full-queue submitter" do + prepared <- preparedTypedTask 0 + withProcessGroupFake + defaultTimeLimit + [] + \pidFile vampireCommand -> do + (waiter, blockedSubmit, processIds) <- + withVampireExecutor + (positiveJobs 1) + vampireCommand + (\_position _request -> pure ()) + \executor -> + withVampireRequestOwner executor \owner -> do + running <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + processIds <- waitForProcessIds pidFile + _queuedOne <- submitVampireRequest + owner + (workPosition 1 2) + (preparedTypedProverRequest prepared) + _queuedTwo <- submitVampireRequest + owner + (workPosition 1 3) + (preparedTypedProverRequest prepared) + waiter <- Async.async + (awaitVampireRequest running) + submitStarted <- newEmptyMVar + blockedSubmit <- Async.async do + putMVar submitStarted () + submitVampireRequest + owner + (workPosition 1 4) + (preparedTypedProverRequest prepared) + takeMVar submitStarted + waitForSubmittedCount executor 3 + pure (waiter, blockedSubmit, processIds) + Async.waitCatch waiter >>= \case + Right completion -> assertCancelled completion + Left failure -> + assertFailure + ("shutdown waiter failed: " <> show failure) + Async.waitCatch blockedSubmit >>= \case + Left failure -> + assertBool + "backpressured submit observes owner shutdown" + ("VampireRequestOwnerClosed" + `Text.isInfixOf` + Text.pack (show failure)) + Right _handle -> + assertFailure + "backpressured submit survived structured shutdown" + assertProcessesGone processIds + , testCase "worker fault wakes a waiter and a full-queue submitter" do + prepared <- preparedTypedTask 0 + observerEntered <- newEmptyMVar + failObserver <- newEmptyMVar + withFakeVampire + [ "cat >/dev/null" + , "printf '%s\n' '% SZS status Theorem for fake'" + ] + \vampireCommand -> + withVampireExecutor + (positiveJobs 1) + vampireCommand + (\position _request -> + when + (workPositionLocalRequestOrdinal position == 1) + (putMVar observerEntered () + >> takeMVar failObserver + >> Exception.throwIO + (userError "fatal observer fault"))) + \executor -> withVampireRequestOwner executor \owner -> do + first <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + takeMVar observerEntered + _second <- submitVampireRequest + owner + (workPosition 1 2) + (preparedTypedProverRequest prepared) + _third <- submitVampireRequest + owner + (workPosition 1 3) + (preparedTypedProverRequest prepared) + withAsync + (submitVampireRequest + owner + (workPosition 1 4) + (preparedTypedProverRequest prepared)) + \blockedSubmit -> do + waitForSubmittedCount executor 3 + putMVar failObserver () + awaitFault (awaitVampireRequest first) + Async.waitCatch blockedSubmit >>= \case + Left failure -> + assertExecutorFault failure + Right _handle -> + assertFailure + "full-queue submission survived executor fault" + , testCase "declared launch failure remains request-local" do + prepared <- preparedTypedTask 0 + let missing = vampire + "/definitely/missing/felix-vampire" + defaultTimeLimit + defaultMemoryLimit + withVampireExecutor + (positiveJobs 1) + missing + (\_position _request -> pure ()) + \executor -> withVampireRequestOwner executor \owner -> do + handle <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + completion <- awaitVampireRequest handle + case vampireCompletionTerminal completion of + VampireProcessFailed ProverLaunchFailed{} -> pure () + terminal -> + assertFailure + ("expected a local launch failure, got " + <> show terminal) + , testCase "protocol failure is distinct from ATP rejection" do + prepared <- preparedTypedTask 0 + withFakeVampire + [ "cat >/dev/null" + , "printf '%s\n' 'completed without an SZS status'" + ] + \vampireCommand -> + withVampireExecutor + (positiveJobs 1) + vampireCommand + (\_position _request -> pure ()) + \executor -> withVampireRequestOwner executor \owner -> do + handle <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + completion <- awaitVampireRequest handle + case vampireCompletionTerminal completion of + VampireProtocolFailed{} -> pure () + terminal -> + assertFailure + ("expected a protocol terminal, got " + <> show terminal) + , testCase "completed rejection diagnostics are compact" do + prepared <- preparedTypedTask 0 + let headMarker :: Text + headMarker = "HEAD-MARKER" + tailMarker :: Text + tailMarker = "TAIL-MARKER" + status :: Text + status = "% SZS status CounterSatisfiable for fake" + originalByteCount = + Text.length headMarker + + 1048576 + + Text.length tailMarker + 1 + + Text.length status + 1 + withFakeVampire + [ "printf '%s' 'HEAD-MARKER'" + , "head -c 1048576 /dev/zero" + , "printf '%s\n' 'TAIL-MARKER'" + , "printf '%s\n' '% SZS status CounterSatisfiable for fake'" + ] + \vampireCommand -> + withVampireExecutor + (positiveJobs 1) + vampireCommand + (\_position _request -> pure ()) + \executor -> withVampireRequestOwner executor \owner -> do + handle <- submitVampireRequest + owner + (workPosition 1 1) + (preparedTypedProverRequest prepared) + completion <- awaitVampireRequest handle + case renderVampireTerminalDiagnostic + (vampireCompletionTerminal completion) of + Just diagnostic -> do + assertBool + "retained diagnostic is bounded" + (Text.length diagnostic < 70000) + assertBool + "truncation is reported" + ("retained first and last 16 KiB" + `Text.isInfixOf` diagnostic) + assertBool + "original byte count is reported" + (("of " + <> Text.pack + (show originalByteCount) + <> " bytes)") + `Text.isInfixOf` diagnostic) + assertBool + "diagnostic head is retained" + (headMarker `Text.isInfixOf` diagnostic) + assertBool + "diagnostic tail is retained" + (tailMarker `Text.isInfixOf` diagnostic) + Nothing -> + assertFailure "expected a rejected terminal" ] positiveJobs :: Int -> EffectiveJobs @@ -485,6 +756,39 @@ assertProved = \case answer -> assertFailure ("expected a proof, got " <> show answer) +assertAcceptedRequest + :: PreparedTypedProverTask ref local origin global + -> VampireCompletion + -> Assertion +assertAcceptedRequest prepared completion = + case vampireCompletionTerminal completion of + VampireAccepted requestId -> + requestId + `shouldBe` + preparedVerificationRequestId + (preparedTypedProverRequest prepared) + terminal -> + assertFailure ("expected an accepted terminal, got " <> show terminal) + +assertCancelled :: VampireCompletion -> Assertion +assertCancelled completion = + vampireCompletionTerminal completion `shouldBe` VampireCancelled + +awaitFault :: IO value -> Assertion +awaitFault action = do + result <- Exception.try action + case result of + Left failure -> assertExecutorFault failure + Right _value -> assertFailure "expected a global executor fault" + +assertExecutorFault :: Exception.SomeException -> Assertion +assertExecutorFault failure = + case Exception.fromException failure :: Maybe VampireExecutorFault of + Just _fault -> pure () + Nothing -> + assertFailure + ("expected VampireExecutorFault, got " <> show failure) + assertProtocolError :: Text -> Either ProverProcessError ProverAnswer |