Email Gateway (Aug 22 2022 at 18:24): Email Gateway (Aug 22 2022 at 18:24):From: Michael.Norrish@data61.csiro.au
Why is the increment amount 2? (Or 3 in those setups where Thread_Data.is_virtual = true.)
Michael
Email Gateway (Aug 22 2022 at 18:25):From: Makarius <makarius@sketis.net>
To understand the Isabelle sources, you need to look at the history.
I have actually changed the above recently, because it was not as
planned (but did not notice because it was not strictly relevant so far).
See http://isabelle.in.tum.de/repos/isabelle/rev/cbde6e3b132b
Makarius
Email Gateway (Aug 22 2022 at 18:25):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
Makarius wrote:
I have trouble reading between the lines. Is this something that can
cause problems (i.e., duplicate "unique" ids) in the Isabelle2018
release, which predates cbde6e3b132b?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 18:25):From: Makarius <makarius@sketis.net>
Reading between the lines of sources is not required, if you actually
follow the history.
The rev cbde6e3b132b above points to a5853334c179 from 09-Apr-2016,
where I introduced the idea of disjoint physical/virtual counters, but
they were not disjoint, and not really required to be disjoint.
To avoid this confusion, I have recently made them disjoint. At some
later stage this might be actually required.
Makarius
Email Gateway (Aug 22 2022 at 18:26):From: Michael.Norrish@data61.csiro.au
Thanks for the discussion. My summary is that the increments were used to ensure that numbers emitted by different sorts of counter would be kept in disjoint sets. The later commit, updating the code I looked at, actually ensures this by using odd and even numbers (rather than multiples of 2 and 3).
Michael
Email Gateway (Aug 22 2022 at 18:27):From: Makarius <makarius@sketis.net>
The implicit context of this thread is actually HOL4, which is in the
process to adopt more and more parallel functional programming
facilities from Isabelle/ML. I generally welcome this.
Poly/ML is a great platform, and it is good to see HOL4 make more use of
its potential. I also recommend to give up the obsolete Moscow ML
support eventually: this will loosen further brakes.
When copying around sources, it requires the usual care to avoid odd
clones and old copies from outdated Isabelle modules. Things are
gradually changing over the years. For example, just a few days ago, I
have again reconsidered old questions about the interaction of
interrupts, parallel evaluation and lazy evaluation, although I am still
not finished with it. BTW, your Susp module in HOL4 is still for
sequential programming only, without interrupts.
There are also subtle side-conditions about the overall ML runtime
environment, e.g. default thread parameters for interrupts, and the
avoidance of certain "standard" I/O operations that are not thread-safe.
The "implementation" manual explains some of this from the perspective
of Isabelle/ML users. If there are questions about the implementation
and design decisions behind that, it is better done in the proper
context, i.e. the HOL mailing list; or the isabelle-dev mailing list if
it is about ongoing changes on the Isabelle repository.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC