Running Verifyta in docker containers.

[linem-davton]

I have been trying to run the model verification inside a docker container, and I keep getting Segmentation Fault (SIGSEGV).

./uppaal/bin/verifyta trafficlights.xml

On deeper inspection, I see that the fault occurs inside libc in function _strlen_avx2().
Here is the backtrace from gdb.

Program received signal SIGSEGV, Segmentation fault.
__strlen_avx2 () at ../sysdeps/x86_64/multiarch/strlen-avx2.S:76
warning: 76     ../sysdeps/x86_64/multiarch/strlen-avx2.S: No such file or directory
(gdb) bt full
#0  __strlen_avx2 () at ../sysdeps/x86_64/multiarch/strlen-avx2.S:76
No locals.
#1  0x000064b90f9b9b47 in ?? ()
No symbol table info available.
#2  0x000064b90f9abdf1 in ?? ()
No symbol table info available.
#3  0x000064b90f893f51 in ?? ()
No symbol table info available.
#4  0x00007eacd48391ca in __libc_start_call_main (main=main@entry=0x64b90f8939f0, argc=argc@entry=2, argv=argv@entry=0x7fff5bfc9668) at ../sysdeps/nptl/libc_start_call_main.h:58
        self = <optimized out>
        result = <optimized out>
        unwind_buf = {cancel_jmp_buf = {{jmp_buf = {140734736668264, 785554781903899411, 2, 0, 110745998935824, 139280776130560, 785554781914385171, 594975529371683603}, mask_was_saved = 0}}, priv = {pad = {0x0, 0x0, 0x2, 0x0}, data = {prev = 0x0, 
              cleanup = 0x0, canceltype = 2}}}
        not_first_call = <optimized out>
#5  0x00007eacd483928b in __libc_start_main_impl (main=0x64b90f8939f0, argc=2, argv=0x7fff5bfc9668, init=<optimized out>, fini=<optimized out>, rtld_fini=<optimized out>, stack_end=0x7fff5bfc9658) at ../csu/libc-start.c:360
No locals.
#6  0x000064b90f89ac15 in ?? ()
No symbol table info available.

The container I am using is based on Ubuntu:24.04 with Dockerfile that looks something like this -

FROM ubuntu:24.04                        
# Install dependencies              
RUN apt-get update && \                                   
     apt-get install -y default-jre&& \
    apt-get install -y wget unzip && \
    apt-get clean && \
    rm -rf /var/lib/apt/lists/*                                                                                                                                                                                                                         
 ... # other stuff

Note that on the host machine (outside of the Docker container), I have no problem executing the verifyta command, and things work as expected.

How do I successfully run the model verification inside the container?

[mikucionisaau]

Looks like you've got conflicting versions of libc. Please try verifyta.sh wrapper script which forces to use the shipped version of libc.

For more diagnostics you could try checking the libc versions:
libc.so --version
verifyta.sh --stdc-version

Ideally, both versions should match. Glibc tries very hard to preserve backward compatibility (old Uppaal should be able to run on newer OS with newer libc), but that does not always work out.

[linem-davton]

Thanks, so I did try a few things, here are my findings.

GLIBC

$ gcc  --print-file-name=libc.so.6
/usr/lib/gcc/x86_64-linux-gnu/13/../../../x86_64-linux-gnu/libc.so.6

$ usr/lib/gcc/x86_64-linux-gnu/13/../../../x86_64-linux-gnu/libc.so.6 --version
    GNU C Library (Ubuntu GLIBC 2.39-0ubuntu8.3) stable release version 2.39.
    Copyright (C) 2024 Free Software Foundation, Inc.
    This is free software; see the source for copying conditions.
    There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
    PARTICULAR PURPOSE.
    Compiled by GNU CC version 13.2.0.
    libc ABIs: UNIQUE IFUNC ABSOLUTE
    Minimum supported kernel: 3.2.0
    
$ verifyta.sh --stdc-version
GLIBC 2.35

verifyta comes with 2.35, the container has version 2.39.

verifyta.sh

$ verifyta.sh trafficlights.xml 
Segmentation fault (core dumped)

To further investigate, I modified the script as such
exec -a verifyta gdb --args "$HERE/lib/ld-linux.so" --library-path "$HERE:$HERE/lib" "$HERE/verifyta" "$@"

$ verifyta.sh trafficlights.xml 

Reading symbols from /root/uppaal/bin/lib/ld-linux.so...
(No debugging symbols found in /root/uppaal/bin/lib/ld-linux.so)
(gdb) run
Starting program: /root/uppaal/bin/lib/ld-linux.so --library-path /root/uppaal/bin:/root/uppaal/bin/lib /root/uppaal/bin/verifyta trafficlights.xml
warning: Error disabling address space randomization: Operation not permitted
warning: Unable to find libthread_db matching inferior's thread library, thread debugging will not be available.

Program received signal SIGSEGV, Segmentation fault.
0x00007ec40f63797d in ?? () from /root/uppaal/bin/lib/libc.so.6
(gdb) bt full
#0  0x00007ec40f63797d in ?? () from /root/uppaal/bin/lib/libc.so.6
No symbol table info available.
#1  0x00007ec4100fcb47 in ?? ()
No symbol table info available.
#2  0x0000555555a60c50 in ?? ()
No symbol table info available.
#3  0x00007ffc85823a70 in ?? ()
No symbol table info available.
#4  0x0000555555a4a0a0 in ?? ()
No symbol table info available.
#5  0x00007ffc85823b10 in ?? ()
No symbol table info available.
#6  0x0000555555a4aeb0 in ?? ()
No symbol table info available.
#7  0x00007ffc85823a68 in ?? ()
No symbol table info available.
#8  0x00007ec40f903660 in ?? () from /root/uppaal/bin/lib/libstdc++.so.6
No symbol table info available.
#9  0x00007ec40f903688 in ?? () from /root/uppaal/bin/lib/libstdc++.so.6
No symbol table info available.
#10 0x0000100210641040 in ?? ()
No symbol table info available.
#11 0x00007ec41063f600 in ?? ()
No symbol table info available.
#12 0x00007ffc85823ae0 in ?? ()
No symbol table info available.
#13 0x00007ffc85823b00 in ?? ()
No symbol table info available.
#14 0x0000000200000001 in ?? ()
No symbol table info available.
#15 0x0000000000000000 in ?? ()
No symbol table info available.

[mikucionisaau]

I just tried it now and I see that verifyta -v from UPPAAL-5.0 indeed crashes, but only at the very end, so it's not a libc issue.

Now I remembered that there was an issue with UPPAAL-5.0 in docker environment where $USER variable is not defined (used to locate the path for UPPAAL settings), because docker runs everything under root by default.

As a workaround please set USER variable, for example:

FROM ubuntu:24.04

RUN apt-get -qq update && apt-get -qq upgrade
# RUN useradd -rm -d /home/ubuntu -s /bin/bash -g root -G sudo -u 1001 ubuntu # ubuntu is already there
USER ubuntu # change to user ubuntu instead of root
ENV USER=ubuntu # set the environment variable
ADD . /home/ubuntu/uppaal # copy UPPAAL installation

WORKDIR /home/ubuntu/uppaal
ENTRYPOINT /home/ubuntu/uppaal/bin/socketserver

The issue has been fixed in UPPAAL-5.1 (at least 5.1.0-beta5 does not have it).
Please report back how it goes.

[linem-davton]

Thank you.
This works, with the $USER variable set and running from the home dir, things work as intended.