'Minisat::OutOfMemoryException' during build

[b-lang-org]

'Minisat::OutOfMemoryException' during build

[quark17]

Can you say more about the environment that you're running in (OS, GHC version, GCC version)? I have run into this when building on Debian 10, which uses GHC 8.4. Some issues prevented me from installing other GHC versions (without spending more time), so I haven't tested if just changing the GHC version will fix it. (I note that the error does not come up when I use GHC 8.0 or earlier, on other OSes.) The behavior I saw was that BSC was indeed taking as many gigs of memory as it could, before eventually failing in the STP solver. I don't believe that STP is at fault, because I changed the solver to be Yices instead (using the -sat-yices flag or by changing the default value in FlagsDecode.hs) and BSC built with GHC 8.4 on Debian 10 would still increase in memory until it ran out.

@bpfoley has also reported seeing this error, even when just running "bsc -help", when building with GHC 8.4 and GCC 9. It's unclear if his issue is the same, but similar message.

As I said, this error has not come up when using GHC 8.0 or earlier, on other OSes.

[flokli]

Full repro, including the environment is here: flokli/nixpkgs@e9db094

This is currently using GHC 8.6.5 and GCC 9.2.0 - just invoke nix-build -A bluespec-bsc from the repo root (requires nix, can be installed from https://nixos.org/nix/).

I'll check with other compiler combinations and report back.

Is there a Slack / IRC channel to discuss these findings?

[flokli]

I can confirm I also run into the same memory consumption issues with GHC 8.4.4.

Older GHC's aren't part of nixpkgs anymore - only the last 3 major releases are kept there.

8.2.2 was removed in September 2019 with 1f157b8cf8a640389b789ae24fd49752f53de1d7, and
8.0.2 in November 2018 with 2f0de54ddbfdb03540128f8d2abcc47221d42b25.

I'm currently performing some necromancy to see if I can get it to run with a GHC 8.2.2, and if that doesn't work with 8.0.2, but bluespec should really work on a somewhat recent GHC release.

[q3k]

Hitting same issue on Fedora 31, GHC 8.6.5, GCC 9.2.1, when building bsvlib/Prelude.bo. Minisat::OutOfMemoryException after bsc eats ~30G of memory. (machine has more memory available, no ulimit as far as I can tell)

[bpfoley]

For what it's worth, this seems to be tied to the version of GCC you're using, not GHC.

With GHC 8.4.4 and GCC 7.3, the compilation of Prelude.bo works fine for me. If I build stp with GCC 8 or later, I get this OutOfMemoryException. (NB because of the recursive makefiles, dependency analysis is broken, so you'll need to do a make clean followed by a make in the src dir if you change GCC version.

[q3k]

Confirmed on another system (Gentoo, GHC 8.0.2) that I am observing the same issue with GCC 9.2.0 but not with GCC 7.4.0.

[vowstar]

I have same problem with debian (in docker)

Environment

hostmachine:

uname -a
Linux ryzen 5.5.2-gentoo #1 SMP PREEMPT Wed Feb 5 21:46:42 CST 2020 x86_64 AMD Ryzen 9 3900X 12-Core Processor AuthenticAMD GNU/Linux

docker with debian:bullseye

The Dockerfile:

FROM debian:bullseye as installer
LABEL maintainer="Huang Rui"
# Update and install software
RUN DEBIAN_FRONTEND=noninteractive apt-get update -qq && \
    DEBIAN_FRONTEND=noninteractive apt-get install -yq \
        ghc \
        libghc-regex-compat-dev \
        libghc-syb-dev \
        libghc-old-time-dev \
        libfontconfig1-dev \
        libxft-dev \
        build-essential \
        autoconf \
        gperf \
        bison \
        flex \
        file \
        wget \
        python \
        unzip \
        rsync \
        sudo \
        git \
        curl

RUN git clone --progress --recursive https://github.com/B-Lang-org/bsc

RUN cd bsc && \
    make PREFIX=/opt/bluespec

GHC version

Glasgow Haskell Compiler, Version 8.6.5, stage 2 booted by GHC version 8.6.5
Using binary package database: /usr/lib/ghc/package.conf.d/package.cache
package flags []
loading package database /usr/lib/ghc/package.conf.d
wired-in package ghc-prim mapped to ghc-prim-0.5.3
wired-in package integer-gmp mapped to integer-gmp-1.0.2.0
wired-in package base mapped to base-4.12.0.0
wired-in package rts mapped to rts
wired-in package template-haskell mapped to template-haskell-2.14.0.0
wired-in package ghc mapped to ghc-8.6.5

GCC version

gcc version 9.2.1 20200123 (Debian 9.2.1-25)

Error log

The command is

${PROJ}/bsc/inst/bin/bsc -stdlib-names -bdir ${PROJ}/bsc/build/bsvlib -p . -vsearch ${PROJ}/bsc/build/bsvlib -no-use-prelude Prelude.bs

The message is

Warning: "Prelude.bs", line 3744, column 25: (P0223)
 Definition of `kind' is not used.
Warning: "Prelude.bs", line 3747, column 25: (P0223)
 Definition of `kind' is not used.
Warning: "Prelude.bs", line 3750, column 25: (P0223)
 Definition of `kind' is not used.
Warning: "Prelude.bs", line 3980, column 8: (P0223)
 Definition of `value' is not used.
terminate called after throwing an instance of 'Minisat::OutOfMemoryException'
make[3]: Leaving directory '/bsc/src/Libraries/Base1'
make[3]: *** [Makefile:22: /bsc/build/bsvlib/Prelude.bo] Aborted (core dumped)
make[2]: *** [Makefile:31: build] Error 2
make[2]: Leaving directory '/bsc/src/Libraries'
make[1]: Leaving directory '/bsc/src'
make[1]: *** [Makefile:16: install] Error 2
make: *** [Makefile:24: install] Error 2
The command '/bin/sh -c cd bsc &&     make PREFIX=/opt/bluespec' returned a non-zero code: 2`

[linuxbest]

FROM debian:bullseye as installer
change to
FROM debian:stretch as installer
then the build can be done.
Thanks.

[quark17]

I suspect that this and #20 are both due to the old STP code not compiling well with newer GCC. (The "imperative statement" error could result from some kind of memory corruption?) I have run an experiment where I removed STP entirely from BSC and no issues occur.

The code in src/stp/ is a very old snapshot. I don't think people should waste time getting it to work. We should either update to use the latest STP (that is now on GitHub and can become a submodule) or remove STP entirely (now that BSC is using a recent Yices as a submodule).

For the most part, BSC uses one solver, which can either be CUDD, STP, or Yices. The default is STP (for historical reasons), but you can switch to others with -sat-cudd and -sat yices. The one exception is in SATPred.hs, which seems to always use STP regardless of that flag! There is commented out code to enable using Yices (and CUDD is not an option because it's too inefficient); we can reinstate that, and see if there are any issues. (And we can certainly remove CUDD at this point, as it was never sufficiently efficient for other purposes and doesn't seem to be supported any more.)