[isabelle-dev] Circular reasoning via multithreading seems too easy
lammich at in.tum.de
Sun Dec 4 22:52:30 CET 2016
On So, 2016-12-04 at 22:30 +0100, Makarius wrote:
> On 04/12/16 11:14, Lars Hupel wrote:
> > >
> > > Where did you see these lots of Unsynchronized.ref (or better
> > > Synchronized.var) in Isabelle Tools?
> > There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools",
> > 181
> > in "~~/src/HOL", and some more in the AFP (many of which appear to
> > be in
> > generated code).
> So what is wrong here?
I find it a bit scary that my first(!) naive attempt to trick Isabelle
in presence of multithreading worked out immediately. I do not think
that it is a desirable state that Isabelle's soundness depends on
correct use of multithreading by the user/tools, and, at the same time,
tools are using more and more multithreading.
Btw: I do not believe that the error that I found depends on a (low-
level) datarace, it should (not yet tried) also work out if using
proper synchronization to make the tactic wait for the theorem.
> Tending global state (normally via Synchronized.var and not the raw
> Unsynchronized.ref) has been part of the normal routine of Isabelle
> maintenance in the last 10 years. At the beginning almost nothing
> worked, but around 2008/2009 it became routine. Today we have a
> robust system, with lots of user tools that are mostly thread-safe.
> The "implementation" manual (sections 0.7.9 and 0.8) has some brief
> explanations for users of Isabelle/ML.
More information about the isabelle-dev