diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index a09de21a3..fe6d829bc 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -82,6 +82,11 @@ jobs: run: brew install gperf if: runner.os == 'macOS' + - name: Installing dependencies (libnuma-dev) on Linux - needed for runsolver + shell: bash + run: sudo apt-get install -y libnuma-dev + if: runner.os == 'Linux' + - name: Build solvers shell: bash run: | diff --git a/.github/workflows/solvers.yml b/.github/workflows/solvers.yml index 8997bfd6e..6601a370f 100644 --- a/.github/workflows/solvers.yml +++ b/.github/workflows/solvers.yml @@ -57,6 +57,11 @@ jobs: run: brew install gperf if: runner.os == 'macOS' + - name: Installing dependencies (libnuma-dev) on Linux - needed for runsolver + shell: bash + run: sudo apt-get install -y libnuma-dev + if: runner.os == 'Linux' + - name: Building solvers shell: bash run: BIN_DIR=${HOME}/.local/bin PROCESSES=2 make solvers diff --git a/Dockerfile b/Dockerfile index b43a86020..6af6c5994 100644 --- a/Dockerfile +++ b/Dockerfile @@ -30,6 +30,7 @@ RUN apt-get install -y --no-install-recommends autoconf # needed RUN apt-get install -y --no-install-recommends gperf # needed when building some solvers (for example yices) RUN apt-get install -y --no-install-recommends python3 # needed when building some solvers (for example z3) RUN apt-get install -y --no-install-recommends default-jre-headless # savilerow +RUN apt-get install -y --no-install-recommends libnuma-dev # runsolver # Only copying the install*.sh scripts RUN mkdir -p etc @@ -51,6 +52,7 @@ RUN PROCESSES=2 etc/build/install-open-wbo.sh RUN PROCESSES=2 etc/build/install-ortools.sh RUN PROCESSES=2 etc/build/install-yices.sh RUN PROCESSES=2 etc/build/install-z3.sh +RUN PROCESSES=2 etc/build/install-runsolver.sh # An attempt to cache more COPY Makefile Makefile diff --git a/Makefile b/Makefile index 6ba770b86..729101097 100644 --- a/Makefile +++ b/Makefile @@ -157,4 +157,5 @@ solvers: @etc/build/silent-wrapper.sh etc/build/install-minizinc.sh @etc/build/silent-wrapper.sh etc/build/install-yices.sh @etc/build/silent-wrapper.sh etc/build/install-z3.sh + @etc/build/silent-wrapper.sh etc/build/install-runsolver.sh @if ls make-solvers-*.stderr make-solvers-*.stdout > /dev/null 2> /dev/null; then echo "At least one solver didn't build successfully."; exit 1; fi diff --git a/docs/conjure-help.html b/docs/conjure-help.html index 51b247958..a6f0c2967 100644 --- a/docs/conjure-help.html +++ b/docs/conjure-help.html @@ -134,6 +134,9 @@  --seed=INTRandom number generator seed.  --limit-models=INTMaximum number of models to generate.  --use-existing-models=FILEFile names of Essence' models generated beforehand.
If given, Conjure skips the modelling phase and uses the existing models for solving.
The models should be inside the output directory (See -o). +runsolver: + --runsolver-cpu-time-limit=INTUse runsolver to limit total CPU time (in seconds) + --runsolver-memory-limit=INTUse runsolver to limit total memory usage (Maximum RSS - in megabytes). Options for other tools:  --savilerow-options=ITEMOptions passed to Savile Row.  --solver-options=ITEMOptions passed to the backend solver. diff --git a/docs/conjure-help.txt b/docs/conjure-help.txt index 729e539ec..fad98d45b 100644 --- a/docs/conjure-help.txt +++ b/docs/conjure-help.txt @@ -261,6 +261,9 @@ If given, Conjure skips the modelling phase and uses the existing models for solving. The models should be inside the output directory (See -o). + runsolver: + --runsolver-cpu-time-limit=INT Use runsolver to limit total CPU time (in seconds) + --runsolver-memory-limit=INT Use runsolver to limit total memory usage (Maximum RSS - in megabytes). Options for other tools: --savilerow-options=ITEM Options passed to Savile Row. --solver-options=ITEM Options passed to the backend solver. diff --git a/etc/build/install-runsolver.sh b/etc/build/install-runsolver.sh new file mode 100755 index 000000000..450512061 --- /dev/null +++ b/etc/build/install-runsolver.sh @@ -0,0 +1,40 @@ +#!/bin/bash + +# version as of 25 March 2024 +# alas, none of the published releases compile correctly +VERSION='3f923c08285bdc5186f995296e1c6bffa0588710' + +set -o errexit +set -o nounset + +DIR="$( cd "$( dirname "$0" )" && pwd )" + +export BIN_DIR=${BIN_DIR:-${HOME}/.local/bin} +export PROCESSES=${PROCESSES:-1} + +OS=$(uname) + +if [ "$OS" == "Linux" ]; then + rm -rf tmp-install-runsolver + mkdir tmp-install-runsolver + pushd tmp-install-runsolver + git clone https://github.com/utpalbora/runsolver.git + cd runsolver + git checkout $VERSION + cd src + if make -j${PROCESSES} ; then + echo "Built." + else + echo "Build failed, trying again with a local patch" + echo "This might happen when building with an old version of libnuma-dev" + patch runsolver.cc ${DIR}/runsolver.patch + make -j${PROCESSES} + fi + cp runsolver ${BIN_DIR}/runsolver + echo "runsolver executable is at ${BIN_DIR}/runsolver" + ls -l ${BIN_DIR}/runsolver + popd + rm -rf tmp-install-runsolver +else + echo "Your OS is (according to uname): ${OS} -- runsolver only works on linux." +fi diff --git a/etc/build/runsolver.patch b/etc/build/runsolver.patch new file mode 100644 index 000000000..24d695b01 --- /dev/null +++ b/etc/build/runsolver.patch @@ -0,0 +1,13 @@ +diff --git a/src/runsolver.cc b/src/runsolver.cc +index f42c9a1..312c985 100644 +--- a/src/runsolver.cc ++++ b/src/runsolver.cc +@@ -906,7 +906,7 @@ void numaInfo() { + return; + + int nbNodes = numa_num_configured_nodes(); +- long mem, memFree; ++ long long mem, memFree; + + cout << "NUMA information:\n"; + cout << " number of nodes: " << nbNodes << endl; diff --git a/etc/build/silent-wrapper.sh b/etc/build/silent-wrapper.sh index 2cb14d3e3..0e47345e8 100755 --- a/etc/build/silent-wrapper.sh +++ b/etc/build/silent-wrapper.sh @@ -1,13 +1,15 @@ #!/bin/bash -# set -o errexit -# set -o nounset +set -o errexit +set -o nounset if [ $# -ne 1 ]; then echo "Only provide a single argument, the path to a bash script." exit 1 fi +export CI=${CI:-false} + echo "Running $1" PID=$$ @@ -24,11 +26,19 @@ else echo " Exit code: ${EXITCODE}" echo " Outputs saved to: make-solvers-${PID}.stdout and make-solvers-${PID}.stderr" echo "" - echo "Last 10 lines of the stdout was:" - tail -n10 make-solvers-${PID}.stdout - echo "" - echo "Last 10 lines of the stderr was:" - tail -n10 make-solvers-${PID}.stderr + if ${CI}; then + echo "stdout was:" + cat make-solvers-${PID}.stdout + echo "" + echo "stderr was:" + cat make-solvers-${PID}.stderr + else + echo "Last 10 lines of the stdout was:" + tail -n10 make-solvers-${PID}.stdout + echo "" + echo "Last 10 lines of the stderr was:" + tail -n10 make-solvers-${PID}.stderr + fi echo "" echo "" echo "" diff --git a/src/Conjure/Process/Enumerate.hs b/src/Conjure/Process/Enumerate.hs index cb006fb71..5160fec4f 100644 --- a/src/Conjure/Process/Enumerate.hs +++ b/src/Conjure/Process/Enumerate.hs @@ -143,6 +143,8 @@ enumerateDomain d = liftIO' $ withSystemTempDirectory ("conjure-enumerateDomain- , nbSolutions = show enumerateDomainMax , copySolutions = False , solutionsInOneFile = False + , runsolverCPUTimeLimit = Nothing + , runsolverMemoryLimit = Nothing , logLevel = LogNone -- default values for the rest , essenceParams = [] diff --git a/src/Conjure/UI.hs b/src/Conjure/UI.hs index ac90e8c27..a596eeab0 100644 --- a/src/Conjure/UI.hs +++ b/src/Conjure/UI.hs @@ -99,6 +99,8 @@ data UI , responses :: String , responsesRepresentation :: String , solutionsInOneFile :: Bool + , runsolverCPUTimeLimit :: Maybe Int + , runsolverMemoryLimit :: Maybe Int -- flags related to logging , logLevel :: LogLevel , verboseTrail :: Bool @@ -739,6 +741,18 @@ ui = modes &= explicit &= help "Place all solutions in a single file instead of generating a separate file per solution.\n\ \Off by default." + , runsolverCPUTimeLimit + = def + &= name "runsolver-cpu-time-limit" + &= groupname "runsolver" + &= explicit + &= help "Use runsolver to limit total CPU time (in seconds)" + , runsolverMemoryLimit + = def + &= name "runsolver-memory-limit" + &= groupname "runsolver" + &= explicit + &= help "Use runsolver to limit total memory usage (Maximum RSS - in megabytes)." , logLevel = def &= name "log-level" diff --git a/src/Conjure/UI/MainHelper.hs b/src/Conjure/UI/MainHelper.hs index 469e1a31f..c6d4c9a81 100644 --- a/src/Conjure/UI/MainHelper.hs +++ b/src/Conjure/UI/MainHelper.hs @@ -800,10 +800,18 @@ savileRowNoParam ui@Solve{..} (modelPath, eprimeModel) = sh $ errExit False $ do when (logLevel >= LogDebug) $ do liftIO $ putStrLn "Using the following options for Savile Row:" liftIO $ putStrLn $ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs) - (stdoutSR, solutions) <- partitionEithers <$> runHandle savilerowScriptName srArgs - (liftIO . srStdoutHandler - (outBase, modelPath, "", ui) - tr (1::Int)) + let handler = liftIO . srStdoutHandler + (outBase, modelPath, "", ui) + tr (1::Int) + let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++ + maybe [] (\ limit -> ["-R", show limit]) runsolverMemoryLimit + (stdoutSR, solutions) <- partitionEithers <$> + if null runsolverArgs + then runHandle savilerowScriptName srArgs handler + else + if os /= "linux" + then return [Left "runsolver is only supported on linux"] + else runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions savileRowNoParam _ _ = bug "savileRowNoParam" @@ -841,10 +849,19 @@ savileRowWithParams ui@Solve{..} (modelPath, eprimeModel) (paramPath, essencePar when (logLevel >= LogDebug) $ do liftIO $ putStrLn "Using the following options for Savile Row:" liftIO $ putStrLn $ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs) - (stdoutSR, solutions) <- partitionEithers <$> runHandle savilerowScriptName srArgs - (liftIO . srStdoutHandler - (outBase, modelPath, paramPath, ui) - tr (1::Int)) + let handler = liftIO . srStdoutHandler + (outBase, modelPath, paramPath, ui) + tr (1::Int) + let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++ + maybe [] (\ limit -> ["-V", show limit]) runsolverMemoryLimit + (stdoutSR, solutions) <- partitionEithers <$> + if null runsolverArgs + then runHandle savilerowScriptName srArgs handler + else + if os /= "linux" + then return [Left "runsolver is only supported on linux"] + else runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler + srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions savileRowWithParams _ _ _ = bug "savileRowWithParams"