[SMT-COMP] SMT-COMP 2016: Application Track Testing

[Armin Biere]

I thought I check this for our cluster set-up too.   On default Ubuntu
(14.04 and 16.04)
the stack default limit is 8192.  On our cluster which runs 14.04 the
master also has
this but the jobs submitted through sun-grid-engine have unlimited.  So I
wrote the
following script which checks stack overflow.  On the master and other
Ubuntu machines
calling this script gives very fast a stack overflow (as it should be) and
then runs
forever eating up all the (virtual) memory before getting a stack
overflow.  On the
cluster (under grid-engine control) it is unlimited from the beginning and
then eats
up the full memory (16 GB virtual 8 GB actual memory) before it runs into
the stack
overflow.  So to make it short, in 'unlimited' both on Ubuntu 14.04 and
16.04 as well
as when submitted on our cluster through Sun-Grid-Engine will really be
unlimited.
So I can not confirm what Mate wrote (in my environment).  BTW, I did have
exactly
this issue with the IIMC model checker in the HWMCC and reran their tool
with much
larger stack limit.  I think I got a specific error message which did only
appear
for that tool on a specific set of benchmarks deterministically.  So I
thought it is
fair to rerun.  But I understand that this might be more difficult here (in
particular
somebody could have checked the stack size and depending on that enable
disable, or limit certain optimizations / rewrites, but Boolector does not
do that).

Here is the the script:


!/bin/sh
set -x
cat << EOF > /tmp/stack-overflow.c
#include <stdio.h>
void f (int i) { printf ("%d\n", i); fflush (stdout); f (i+1); }
int main () { f (0); }
EOF
ulimit -s
gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
time -f %E /tmp/stack-overflow|tail -1
ulimit -s unlimited
ulimit -s
time -f %E /tmp/stack-overflow|tail -1


On a standard ubuntu installation it gives:

+ ulimit -s
8192
+ gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
+ time -f %E /tmp/stack-overflow
+ tail -1
Command terminated by signal 11
0:00.30
261874
+ ulimit -s unlimited
+ ulimit -s
unlimited
+ time -f %E /tmp/stack-overflow
+ tail -1
...
(then I pressed control-c)


So you can do 261,874 recursive invocations by default
(so never implement unlimited recursion on data structures
like a list which might have a million elements).


On the cluster nodes the output is split in stderr and stdout:

stdout:

unlimited
518808577
unlimited
518813922


stderr:


+ cat
+ ulimit -s
+ gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
+ time -f %E /tmp/stack-overflow
+ tail -1
Command terminated by signal 11
9:23.40
+ ulimit -s unlimited
+ ulimit -s
+ tail -1
+ time -f %E /tmp/stack-overflow
Command terminated by signal 11
9:11.67

So it takes more than 9 minutes to eat up that virtual
memory of 16GB (8GB real).  Note that I did not use
'runlim' or something similar to limit memory.



Maybe on StarExec there is a different behaviour?


Armin

On Sun, Jun 12, 2016 at 4:22 AM, Aaron Stump <aaron-stump at uiowa.edu> wrote:

> Hello, Mate.
>
> On 06/11/2016 07:59 AM, Mate Soos wrote:
>
>> Hi Aaron,
>>
>> First of all, thanks for getting back to me!
>>
> Sure, I am happy to discuss this matter with you.
>
>>
>> On 06/10/2016 09:11 PM, Aaron Stump wrote:
>>
>>> I am sorry you ran into a problem with stack size.  We are actually not
>>> setting the stack limit explicitly in our jobscript.  What are you
>>> seeing that makes you think it is lower than what is shown with "ulimit
>>> -s" (namely, 8192KB)?  This value should have been something one could
>>> see with the VM instance (though we are due to update that in the next
>>> week or so, but I don't expect major changes).
>>>
>>> Certainly one could ask for a higher stack limit than 8MB, and I would
>>> be happy to have us raise this or make it configurable.
>>>
>> I think the stack limit was about 2MB -- and I think it might have been
>> because it was set to:
>>
>> ulimit -s unlimited
>>
> Out of curiosity: what are you seeing that makes you think that we are
> setting "ulimit -s unlimited"?
>
>>
>> Yep -- unlimited stack is actually more limiting for whatever reason. I
>> have default 8MB (Ubuntu/Debian default), RedHat Linux default has 10MB.
>> Can you please create an example run with the system that ran the SMT
>> Competition that simply runs
>>
>> ulimit -a
>>
>> please? That would clear things up :)
>>
> I agree that this would help clear up this issue.  Here is the output from
> a single job pair that just calls ulimit -a
> (the job is
> https://www.starexec.org/starexec/secure/details/job.jsp?id=16269):
>
> 0.00/0.00       core file size          (blocks, -c) unlimited
> 0.00/0.00       data seg size           (kbytes, -d) unlimited
> 0.00/0.00       scheduling priority             (-e) 0
> 0.00/0.00       file size               (blocks, -f) 629145600
> 0.00/0.00       pending signals                 (-i) 1030922
> 0.00/0.00       max locked memory       (kbytes, -l) 64
> 0.00/0.00       max memory size         (kbytes, -m) unlimited
> 0.00/0.00       open files                      (-n) 1024
> 0.00/0.00       pipe size            (512 bytes, -p) 8
> 0.00/0.00       POSIX message queues     (bytes, -q) 819200
> 0.00/0.00       real-time priority              (-r) 0
> 0.00/0.00       stack size              (kbytes, -s) unlimited
> 0.00/0.00       cpu time               (seconds, -t) 90
> 0.00/0.00       max user processes              (-u) 4096
> 0.00/0.00       virtual memory          (kbytes, -v) 1099776
> 0.00/0.00       file locks                      (-x) unlimited
>
>
> So indeed, the stack size is unlimited.  Our code does not seem to be
> setting this explicitly, so I am not sure where it is getting set.
>
> I was not aware that ulimit -s unlimited would actually impose a default
> limit.  Do you mind sharing a reference for that?  This ulimit
> is different from what I see when I log in to a compute node and run
> "ulimit -a" (there, the stack size is set to 8MB).  So it is getting
> set somehow differently in the system when job pairs are getting run on
> the compute nodes.
>
> This stack size limit is something we will surely want to change, though I
> would like additional confirmation that ulimit -s unlimited on linux will
> actually (and quite counterintuitively) impose this low default limit.
>
> Cheers, and thanks for your investigation,
> Aaron
>
>>
>> Thanks a lot in advance,
>>
>> Mate
>>
>>
>>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>