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



On 21/06/2018 11:11, Makarius wrote:
On 21/06/18 12:06, Mathias Fleury wrote:

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".
OK, I've now seen it too. It is definitely somewhere at the bottom of
Poly/ML, not in Isabelle/ML.

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





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