Email Gateway (Aug 22 2022 at 17:23): Email Gateway (Aug 22 2022 at 17:23):From: Makarius <makarius@sketis.net>
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
$ ./polyPolyML.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
signature.asc
Email Gateway (Aug 22 2022 at 17:23):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello Makarius and Eugene,
I have the same effect (except with a different values).
My Computer:
MacBook Pro (Retina, 15-inch, Mid 2015)
2,5 GHz Intel Core i7
16 GB 1600 MHz DDR3
High Sierra 10.13.4
Isabelle version (more-or-less RC0):
$ hg id
4e27f5c361d2 tip
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.
I managed to get a negative total number of threads:
isabelle console -r
Poly/ML> fun f n = if n = 0 then () else ignore (Thread.Thread.fork (fn () => OS.Process.sleep (Time.fromSeconds 10), []));
After calling f with various numerical arguments (it requires a dozen of calls [I used values between 10 and 100, so it should be more that the number of threads required by Isabelle]; it also seems that different values must be used, but I have not found a reproducible way)
val it =
{gcFullGCs = 0, gcPartialGCs = 0, sizeAllocation = 123731968,
sizeAllocationFree = 2708352, sizeHeap = 123731968,
sizeHeapFreeLastFullGC = 0, sizeHeapFreeLastGC = 0, threadsInML = 15,
threadsTotal = ~1, threadsWaitCondVar = 0, threadsWaitIO = 13,
threadsWaitMutex = 0, threadsWaitSignal = 1, timeGCSystem = 0.000,
timeGCUser = 0.000, timeNonGCSystem = 1.243, timeNonGCUser = 0.517,
userCounters = fromList[0, 0, 0, 0, 0, 0, 0, 0]}:
val it =
{gcFullGCs = 0, gcPartialGCs = 0, sizeAllocation = 140509184,
sizeAllocationFree = 1910304, sizeHeap = 140509184,
sizeHeapFreeLastFullGC = 0, sizeHeapFreeLastGC = 0, threadsInML = 2,
threadsTotal = ~29, threadsWaitCondVar = 0, threadsWaitIO = 1,
threadsWaitMutex = 0, threadsWaitSignal = 1, timeGCSystem = 0.000,
timeGCUser = 0.000, timeNonGCSystem = 1.791, timeNonGCUser = 0.670,
userCounters = fromList[0, 0, 0, 0, 0, 0, 0, 0]}
Best,
Mathias
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
$ ./polyPolyML.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
Email Gateway (Aug 22 2022 at 17:23):From: Mathias Fleury <mathias.fleury12@gmail.com>
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
Email Gateway (Aug 22 2022 at 17:23):From: Makarius <makarius@sketis.net>
OK, I've now seen it too. It is definitely somewhere at the bottom of
Poly/ML, not in Isabelle/ML.
Makarius
Email Gateway (Aug 22 2022 at 17:25):From: David Matthews <dm@prolingua.co.uk>
The threads count was being decremented twice. This was a consequence
of a change in the way thread exit is handled. I've committed a fix to
this to Poly/ML master along with another fix that corrects
"threadsInML". I'll port these to the fixes-5.7.1 branch if they look
all right. Thanks for reducing it to a manageable example.
David
Email Gateway (Aug 22 2022 at 17:34):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I happened to be perusing the tabs in the Monitor panel in Isabelle2018-RC0
and noticed that one of the values (threads total? displayed as some kind of
red line on my system) has a bizarre value of about -375. The auto-scaling
adjusts for this, making the overall graph pretty useless.
This is on Ubuntu 16.04 LTS:
Linux 4.4.0-124-generic #148-Ubuntu SMP Wed May 2 13:00:18 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux
CPU: Intel(R) Core(TM) i5-4670K CPU @ 3.40GHz
Email Gateway (Aug 22 2022 at 17:37):From: Makarius <makarius@sketis.net>
I haven't seen anything like this myself, but I remember that you have
used Linux with special system debugging options before: that might
somehow confuse the built-in system statistics of the Poly/ML 5.7.1
runtime system (in Isabelle2017 that was Poly/ML 5.6).
This is how to access that data without anything of Isabelle/ML system
infrastructure getting in between:
$ isabelle console -r
Poly/ML> PolyML.Statistics.getLocalStats ();
You can also fork a few threads and then inspect the statistics again:
Poly/ML> Thread.Thread.fork (fn () => OS.Process.sleep
(Time.fromSeconds 10), []);
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.
Makarius
Email Gateway (Aug 22 2022 at 17:41):From: Makarius <makarius@sketis.net>
This appears to be on master dd7f37b157035614295d53aa14db27dfc06b1598 +
af7995530c13f13ae3e36438c7e1c6b5b44054d9, but I only see the "inML"
change on fixes-5.7.1 (3f75961b36601451a464b2eb22fb54d4a10ee24c).
Consequently, it is still possible in Isabelle2018-RC2 to get negative
threadsTotal as above.
Makarius
Email Gateway (Aug 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
I have updated to Poly/ML fixes-5.7.1 b3d1ff33a4b4 for the next release
candidate, see
https://isabelle.sketis.net/repos/isabelle-release/rev/8ef8905629ba
Makarius
Last updated: Apr 23 2024 at 20:15 UTC