[isabelle-dev] JinjaThreads

[Florian Haftmann]

Hi all,

it seems indeed that JinjaThreads since recently runs out of memory even
on macbroy2 with parallelism, c.f. last afp isatest log:

> Running HOL-Word-JinjaThreads ...
> poly(19058,0xa00a0540) malloc: *** mmap(size=16777216) failed (error code=12)
> *** error: can't allocate region
> *** set a breakpoint in malloc_error_break to debug
> poly(19058,0xa00a0540) malloc: *** mmap(size=2097152) failed (error code=12)
> *** error: can't allocate region
> *** set a breakpoint in malloc_error_break to debug
> terminate called after throwing an instance of 'St9bad_alloc'
>   what():  std::bad_alloc
> /mnt/nfsbroy/home/isabelle/Isabelle2009-2/lib/scripts/run-polyml: line 74: 19058 Abort trap              "$POLY" -q $ML_OPTIONS
> HOL-Word-JinjaThreads FAILED
> (see also /home/isatest/.isabelle/heaps/Isabelle2009-2/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads)
> 
> ### TC0.ty P ?E ?e == THE T. P,?E \<turnstile>1 ?e :: T
> ### Ignoring duplicate introduction (intro)
> ### [| ?P ?a; !!x. ?P x ==> x = ?a |] ==> (THE x. ?P x) = ?a
> ### Rule already declared as introduction (intro)
> ### ?P ?x ==> EX x. ?P x
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Ignoring duplicate rewrite rule:
> ### pcs (shift ?n1 ?xt1) == op + ?n1 ` pcs ?xt1
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> ### Trying linear arithmetic...
> 
> make: *** [/home/isatest/.isabelle/heaps/Isabelle2009-2/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads.gz] Error 134

Also another test on a considerably smaller machine without parallelism
does not run through any longer:

http://www4.in.tum.de/~haftmann/cgi-bin/testboard.cgi/AFP/report/9eaa8a4c3b0745dd95acafb8477968f6

I would say we have broken through our current the sonic barrier and
guess that this is due to the recent extension of JinjaThreads:

http://www4.in.tum.de/~haftmann/cgi-bin/testboard.cgi/AFP/rev/1f41c1842f5a

So, I would suggest to set JINJATHREADS_OPTIONS='-M 1 -q 0' on macbroy2
and give it again a try.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101220/6728e2b0/attachment.sig>