Re: [isabelle] Threads tab in Monitor panel (Isabelle2018-RC0)



Hello Makarius,


The following seems to be reproducible (both on my mac and on a Linux-Server):

isabelle console -r
Poly/ML> fun f n = if n = 0 then () else ignore (Thread.Thread.fork (fn () => OS.Process.sleep (Time.fromSeconds 10), []));
val f = fn: int -> unit
Poly/ML> f 5;
val it = (): unit
Poly/ML> f 5;
val it = (): unit
Poly/ML> f 5;
val it = (): unit

Then I waited 30s and got:


Poly/ML> PolyML.Statistics.getLocalStats ();
val it =
   {gcFullGCs = 0, gcPartialGCs = 0, sizeAllocation = 4194304,
    sizeAllocationFree = 1725432, sizeHeap = 4194304,
    sizeHeapFreeLastFullGC = 0, sizeHeapFreeLastGC = 0, threadsInML = 2,
    threadsTotal = ~1, threadsWaitCondVar = 0, threadsWaitIO = 0,
    threadsWaitMutex = 0, threadsWaitSignal = 1, timeGCSystem = 0.000,
    timeGCUser = 0.000, timeNonGCSystem = 0.085, timeNonGCUser = 0.057,
    userCounters = fromList[0, 0, 0, 0, 0, 0, 0, 0]}:
   {gcFullGCs: int,
     gcPartialGCs: int,
     sizeAllocation: int,
     sizeAllocationFree: int,
     sizeHeap: int,
     sizeHeapFreeLastFullGC: int,
     sizeHeapFreeLastGC: int,
     threadsInML: int,
     threadsTotal: int,
     threadsWaitCondVar: int,
     threadsWaitIO: int,
     threadsWaitMutex: int,
     threadsWaitSignal: int,
     timeGCSystem: Time.time,
     timeGCUser: Time.time,
     timeNonGCSystem: Time.time,
     timeNonGCUser: Time.time, userCounters: int vector}


More iterations of the loop (calling f three times, then waiting) lead to lower values of the "threadsTotal".



Best,
Mathias

> On 21. Jun 2018, at 11:23, Makarius <makarius at sketis.net> wrote:
> 
> On 15/06/18 22:11, Eugene W. Stark wrote:
>> I'm not doing any funny stuff with system debugging -- just using Isabelle2018-RC0
>> "out of the box".
>> 
>> I just tried the "isabelle console" thing you suggested, and the output from PolyML
>> appears reasonable.  I have attached that, as well as the Monitor window from
>> JEdit, which does not appear reasonable.  I tried forking a thread and the
>> stats reported by PolyML changed as expected.  So does not look like a PolyML
>> issue.
> 
> I cannot follow that conclusion.
> 
> The statistics are produced by the Poly/ML runtime system, and
> Isabelle/ML + Isabelle/Scala merely pass-on the values to the GUI panel.
> 
> I have studied the sources once again, and don't see how a negative
> value can emerged. There is probably something wrong at the very bottom
> of it.
> 
> 
>> On 06/15/2018 03:51 PM, Makarius wrote:
>>> 
>>> If you feel like it, you may also rebuild the bundled Poly/ML version
>>> from sources, and experiment with the resulting poly executable:
>>> 
>>>  $ cd Isabelle2018-RC0/contrib/polyml-5.7.1-5/src
>>>  $ ./configure && make compiler && make compiler
>>>  $ ./poly
>>>> PolyML.print_depth 100;
>>>> PolyML.Statistics.getLocalStats ();
>>> 
>>> Note that this gives you x86_64-linux by default: it can be compared
>>> directly with Isabelle2018-RC0/contrib/polyml-5.7.1-5/x86_64-linux/poly
>>> -- the Isabelle default is normally the x86-linux version, provided you
>>> have the package lib32stdc++6 installed, but building it requires more
>>> packages and options.
>>> 
>>> Anyway, if there is a deeper problem behind it, we should move this to
>>> the Poly/ML mailing list.
> 
> Can you try building Poly/ML from the bundled sources? Thus we could
> rule out odd effects from the rather old build environment (Ubuntu
> 12.04) of the official binaries.
> 
> You need to test the in the same Isabelle/PIDE environment as before.
> Apparently the raw console is not sufficient to see the effect.
> 
> 
> 	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.