Static-Compilation

[Mystelven]

One good feature for a solver is the ability to be compiled as a static executable. Do you think it is possible to add such feature ?

Because I compile moloss on my machine and tried to run it on our super-calculator, but I get the following problem:

Fatal error: cannot load shared library dllminisat_stubs
Reason: dllminisat_stubs.so: cannot open shared object file: No such file or directory

Keep me informed if you think it is possible :).

[jogiet]

make custom should compile a static executable. Keep me informed if it works.

[Mystelven]

Still not working. I get the error ./moloss: /lib64/libc.so.6: version 'GLIBC_2.17' not found (required by ./moloss)

Maybe this link (https://stackoverflow.com/questions/17390117/reducing-the-version-of-libc-required) can help you fix it?

[tofgarion]

Hi Valentin,

Using the -custom option of ocamlbuild only compiles an executable embedding the runtime, but does not statically compile against libc for instance. Thus, the "best" solution is to statically include libc in the executable... For a simple solution, is it possible for you to compile MOLOSS directly on your super-calculator?

Anyway, I am currently struggling with ocamlc options to statically compile MOLOSS against libc. Adding -static option to the C compiler via ocamlbuild tags produces a linking error with libcamlrun library concerning terminfo. I suspect this error to be the same as https://caml.inria.fr/mantis/view.php?id=7164

I keep you up to date.

[tofgarion]

Using Ocaml version 4.06.0 solves only one part of the problem, as (I think) termcap is no more used in this version. But I cannot statically compile MOLOSS against libc with 4.06.0, as there are (of course) some dynamic symbol like strcmp in libc.a. I must confess I am stuck for the moment...

[Mystelven]

Hello Christophe,

 For a simple solution, is it possible for you to compile MOLOSS directly on your super-calculator?

It is unfortunately not that simple, the super-calculator is used by the whole laboratory and it is not that easy to ask to install so many libraries for just one executable :/.

I tried many things on my side also to see what I can do to make it link statically the exe, but I did not manage either. Here is the list of shared libraries that are needed :

valentinmontmirail@Ubuntu:~/moloss$ readelf -d ./moloss.byte | grep library

0x0000000000000001 (NEEDED)             Shared library: [libm.so.6]
0x0000000000000001 (NEEDED)             Shared library: [libdl.so.2]
0x0000000000000001 (NEEDED)             Shared library: [libtinfo.so.5]
0x0000000000000001 (NEEDED)             Shared library: [libpthread.so.0]
0x0000000000000001 (NEEDED)             Shared library: [libc.so.6]

Don't you think it is possible to add their statically-available version to the program during the linking ?

[tofgarion]

It should normally be possible to generate an executable with all dependencies linked statically. I was trying to by adding the following line in _tags :

true: ccopt(-static)

This should add the -static option when calling gcc. Unfortunately, I have either a link error with termcap with ocaml 4.05.0 or a problem with strcmp with ocaml 4.06.0. I will ask for help on the Caml list.

By the way, what is the system on your super-calculator ? I have no problem to execute the "custom" version of MOLOSS on our servers with CentOS 7 installed, whereas CentOS 7 is not considered to have recent version of librairies.

[tofgarion]

Hi Valentin,

There is a (non satisfactory) solution that I have pushed in the static branch of the repo. Using

make static

should produce a _build/src/moloss.native executable without dynamic dependencies. Could you please test it?

This is not a good solution, as I pass the -static option to GCC regardless of the target to be built. I should write a new rule for static compilation in a myocamlbuild.ml file.

[Mystelven]

Hi Christophe,

Still not statically compiled. I tried to add a verbose mode in the _tags for you to have more information about how Ocaml can deal with that :/

Here is the stacktrace:

valentinmontmirail@Ubuntu:~/MOLOSS$ make static

ocamlfind query unix
/usr/local/lib/ocaml

ocamlfind query minisat
/home/valentinmontmirail/.opam/system/lib/minisat

ocamlfind query msat
/home/valentinmontmirail/.opam/system/lib/msat

ocamlbuild -use-ocamlfind -I src -I tests -tag custom src/moloss.native
+ ocamlfind ocamlopt -linkpkg -ccopt '-static --verbose' -package unix -package minisat -package msat -I src src/ast_modal.cmx src/InToHyLoParser.cmx src/InToHyLoLexer.cmx src/ast_fo.cmx src/ast_proof.cmx src/pprinter.cmx src/convertisseur.cmx src/sign.cmx src/decide.cmx src/direct.cmx src/pparser.cmx src/plexer.cmx src/smtminisat.cmx src/smtmsat.cmx src/z3_parser.cmx src/z3_lexer.cmx src/smtz3.cmx src/solve.cmx src/moloss.cmx -o src/moloss.native
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/4.8/lto-wrapper
Target: x86_64-linux-gnu

Configured with: ../src/configure -v --with-pkgversion='Ubuntu 4.8.4-2ubuntu1~14.04.3' --with-bugurl=file:///usr/share/doc/gcc-4.8/README.Bugs --enable-languages=c,c++,java,go,d,fortran,objc,obj-c++ --prefix=/usr --program-suffix=-4.8 --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --with-gxx-include-dir=/usr/include/c++/4.8 --libdir=/usr/lib --enable-nls --with-sysroot=/ --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --enable-gnu-unique-object --disable-libmudflap --enable-plugin --with-system-zlib --disable-browser-plugin --enable-java-awt=gtk --enable-gtk-cairo --with-java-home=/usr/lib/jvm/java-1.5.0-gcj-4.8-amd64/jre --enable-java-home --with-jvm-root-dir=/usr/lib/jvm/java-1.5.0-gcj-4.8-amd64 --with-jvm-jar-dir=/usr/lib/jvm-exports/java-1.5.0-gcj-4.8-amd64 --with-arch-directory=amd64 --with-ecj-jar=/usr/share/java/eclipse-ecj.jar --enable-objc-gc --enable-multiarch --disable-werror --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --with-tune=generic --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix

gcc version 4.8.4 (Ubuntu 4.8.4-2ubuntu1~14.04.3) 

COMPILER_PATH=/usr/lib/gcc/x86_64-linux-gnu/4.8/:/usr/lib/gcc/x86_64-linux-gnu/4.8/:/usr/lib/gcc/x86_64-linux-gnu/:/usr/lib/gcc/x86_64-linux-gnu/4.8/:/usr/lib/gcc/x86_64-linux-gnu/
LIBRARY_PATH=/usr/lib/gcc/x86_64-linux-gnu/4.8/:/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/:/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../../lib/:/lib/x86_64-linux-gnu/:/lib/../lib/:/usr/lib/x86_64-linux-gnu/:/usr/lib/../lib/:/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../:/lib/:/usr/lib/

COLLECT_GCC_OPTIONS='-std=gnu99' '-O2' '-fno-strict-aliasing' '-fwrapv' '-fno-builtin-memcmp' '-Wall' '-fno-tree-vrp' '-D' '_FILE_OFFSET_BITS=64' '-D' '_REENTRANT' '-D' 'CAML_NAME_SPACE' '-o' 'src/moloss.native' '-Lsrc' '-L/home/valentinmontmirail/.opam/system/lib/minisat' '-L/home/valentinmontmirail/.opam/system/lib/msat' '-L/usr/local/lib/ocaml' '-static' '-v' '-mtune=generic' '-march=x86-64'
 /usr/lib/gcc/x86_64-linux-gnu/4.8/collect2 --sysroot=/ --build-id -m elf_x86_64 --hash-style=gnu --as-needed -static -z relro -o src/moloss.native /usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crt1.o /usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crti.o /usr/lib/gcc/x86_64-linux-gnu/4.8/crtbeginT.o -Lsrc -L/home/valentinmontmirail/.opam/system/lib/minisat -L/home/valentinmontmirail/.opam/system/lib/msat -L/usr/local/lib/ocaml -L/usr/lib/gcc/x86_64-linux-gnu/4.8 -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../../lib -L/lib/x86_64-linux-gnu -L/lib/../lib -L/usr/lib/x86_64-linux-gnu -L/usr/lib/../lib -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../.. -E /tmp/camlstartup839b78.o /usr/local/lib/ocaml/std_exit.o src/moloss.o src/solve.o src/smtz3.o src/z3_lexer.o src/z3_parser.o src/smtmsat.o src/smtminisat.o src/plexer.o src/pparser.o src/direct.o src/decide.o src/sign.o src/convertisseur.o src/pprinter.o src/ast_proof.o src/ast_fo.o src/InToHyLoLexer.o src/InToHyLoParser.o src/ast_modal.o /home/valentinmontmirail/.opam/system/lib/msat/msat.a /home/valentinmontmirail/.opam/system/lib/minisat/minisat.a /usr/local/lib/ocaml/unix.a /usr/local/lib/ocaml/stdlib.a -lminisat_stubs -lunix /usr/local/lib/ocaml/libasmrun.a -lm -ldl --start-group -lgcc -lgcc_eh -lc --end-group /usr/lib/gcc/x86_64-linux-gnu/4.8/crtend.o /usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crtn.o

/usr/local/lib/ocaml/libasmrun.a(unix.o): In function `caml_dlopen':
/home/valentinmontmirail/Téléchargements/ocaml-4.06.0/asmrun/unix.c:273: warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(initgroups.o): In function `unix_initgroups':
initgroups.c:(.text+0x1f): warning: Using 'initgroups' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getgr.o): In function `unix_getgrgid':
getgr.c:(.text+0x128): warning: Using 'getgrgid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getgr.o): In function `unix_getgrnam':
getgr.c:(.text+0x101): warning: Using 'getgrnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getpw.o): In function `unix_getpwnam':
getpw.c:(.text+0x151): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getpw.o): In function `unix_getpwuid':
getpw.c:(.text+0x178): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getaddrinfo.o): In function `unix_getaddrinfo':
getaddrinfo.c:(.text+0x224): warning: Using 'getaddrinfo' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(gethost.o): In function `unix_gethostbyaddr':
gethost.c:(.text+0x209): warning: Using 'gethostbyaddr_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(gethost.o): In function `unix_gethostbyname':
gethost.c:(.text+0x2b9): warning: Using 'gethostbyname_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getproto.o): In function `unix_getprotobynumber':
getproto.c:(.text+0xe8): warning: Using 'getprotobynumber' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getproto.o): In function `unix_getprotobyname':
getproto.c:(.text+0xc1): warning: Using 'getprotobyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getserv.o): In function `unix_getservbyname':
getserv.c:(.text+0x108): warning: Using 'getservbyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/local/lib/ocaml/libunix.a(getserv.o): In function `unix_getservbyport':
getserv.c:(.text+0x159): warning: Using 'getservbyport' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

/usr/bin/ld: dynamic STT_GNU_IFUNC symbol `tan' with pointer equality in `/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/libm.a(s_tan.o)' can not be used when making an executable; recompile with -fPIE and relink with -pie
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
Command exited with code 2.

Compilation unsuccessful after building 70 targets (69 cached) in 00:00:00.
make: *** [static] Error 10

So if I understand correctly what Ocaml is trying to say, we need to add the -fPIE flag during the compilation and -pie during the linking :) And I forget to answer your previous question, the final target is:

CentOS release 6.4 (Final)
Linux version 2.6.32-358.23.2.el6.x86_64 (mockbuild@c6b9.bsys.dev.centos.org) (gcc version 4.4.7 20120313 (Red Hat 4.4.7-3) (GCC) ) #1 SMP Wed Oct 16 18:37:12 UTC 2013

So I try to compile statically on a Ubuntu 14.04 (which is my virtual machine) to then run the executable on the super-calculator :)

[tofgarion]

Ouch, CentOS 6.4 is pretty old. And I thought our servers were not up-to-date :)

Install version 4.05.0 of OCaml and compilation should be fine:

opam switch install 4.05.0
eval `opam config env`
opam install minisat msat menhir

I do not know why it does not compile with OCaml 4.06.0. Something more to investigate...

[Mystelven]

Alright that's perfect now :) it can run on the Cluster :). Now I have an additional question.

Should we use it in a scientific article, quoting the paper of P.Fontaine for the idea and giving credits to Giet et al. for the development of it ?

You are probably more aware of the performance, I will run it on the super-computer to see it by myself, so it is up to you guys if you want it to appear on cactus-plot :)

In any case I will cite it in my thesis, it is too much work for being just on GitHub and not having credits for it ;)

[tofgarion]

Cool. Yes I think that you should use it in an article. Even if performance comparison will not be to our advantage, I am interested in the results of your benchmarks :) You should cite Carlos, Pascal and Stephan paper for the idea and Giet et al. for the development.

Static compilation is now enabled in the master branch, I will delete the static branch.

Best,

Christophe